NameTheTrait 2.0

This article is intended to be an improvement on the original (logically invalid) NameTheTrait argument. It is possible to correct the NTT argument and preserve its persuasive force by adding a premise that rejects double standards and by changing the first premise to require human moral value (or some other moral consideration) to be based on a trait. This makes NTT valid, and allows it to be presented in the same way as it was intended.

NTT 2.0 In English

In the following x has R means; we are moral required to not consume the products of x for food, in order to prevent harm to x.

(This could be substituted for moral value or the right to equal consideration of interests etc.)

(P1) There exists a trait, such that, if an individual is a human then the individual has R if and only if they possess the trait

(humans who possess a certain trait have R (this may or may not include all humans))

(P2) If humans have R if and only if they possess a certain trait, then all beings have R if an only if they possess the certain trait.

(rejection of double standards)

(P3) If an individual is a sentient nonhuman animal, then there is no trait absent in the individual, which if absent in a human, would cause the human to not have R.

or equivalently

(P3) If an individual is a sentient nonhuman animal, then the trait that grants humans R is present in the individual.

(sentient nonhuman animals possess this certain trait)

Therefore

(C) Sentient nonhuman animals have R

(we are morally required to go vegan)

Defense of Premises

P1 - All that is necessary here is to convince the opponent that humans who have R, have R in virtue of some trait that they have, it is not necessary to specify which trait. But examples may include example sentience, capacity for sentience, moral agency etc. Furthermore all humans may or may not possess this trait.

P2 - Most people would reject moral double standards, it is unlikely that one would face much resistance on this premise.

P3 - If one can convince an opponent that the sentience, capacity for sentience or similar then they must accept the premise. People will be unlikely to say the trait which grants humans R is moral agency, intelligence, or similar, as this would imply that infants or disabled humans would not have R.

In First Order Logic

Definitions

H(x) means 'x is a human'

SNA(x) means 'x is a sentient non-human animal'

R(x) means 'we are morally required to seek to exclude—as far as is possible and practicable (AFAPP)—all forms of exploitation of, and : cruelty to, x'

T(x) means 'x is a trait'

P(x,y) means 'x has y'

In First Order Logic

(P1) ∃t ( Tt ∧ ∀x ( Hx ⇒ ( Rx ⇔ Pxt ) ) )

(P2) ∀t ( Tt ∧ ( ∀x ( Hx ⇒ ( Rx ⇔ Pxt ) ) ⇒ ∀x ( Rx ⇔ Pxt ) ) )

(P3) ∀x( SNAx ⇒ ¬∃t ( Tt ∧ ¬Pxt ∧ ∀y ( Hy ⇒ ( ¬Pyt ⇒ ¬Ry ) ) ) )

or equivalently

(P3) ∀x( SNAx ⇒ ∀t ( Tt ∧ ∀y ( Hy ⇒ ( Ry ⇒ Pyt ) ) ⇒ Pxt ) )

Therefore (C) ∀x ( SNAx ⇒ Rx )

Direct Translation

(P1) there exists t, such that t is a trait, and for all x, if x is a human, then x has R, if and only if x has t

(P2) for all t, t is a trait, and if for all x, if x is a human, then x has R if and only if x has t, then for all x, x has R if and only if x has t

(P3) for all x, if x is a sentient nonhuman animal, then there does not exist t, such that, t is a trait and, x lacks t, and for all y, if y is a human, then if y lacks t, then y does not have R

or equivalently

(P3) for all x, if x is a sentient non-human animal, then for all t, if t is a trait, and, for all y, if y is a sentient human, then, if y has R then y has t, then x has t

Therefore (C) for all x, if x is a sentient nonhuman animal then x has R

Proof of Validity

Logical Proof Generator

We can show this is valid argument by using a logical proof generator, to prove the formula

P1 ∧ P2 ∧ P3 ⇒ C

with the input

(P1) \existst ( Tt \land \forallx (Hx \to ( Rx \leftrightarrow Pxt ) ) )

(P2) \forallt (Tt \land ( \forallx (Hx \to ( Rx \leftrightarrow Pxt ) ) \to \forallx ( Rx \leftrightarrow Pxt ) ) )

(P3) \forallx ( Ax \to \neg \existst ( Tt \land \negPxt \land( \forally (Hy \to ( \negPyt \to \negRy ) ) ) ) )

or equivalently

(P3) \forallx( Ax \to \forallt ( Tt \land \forally ( Hy \to ( Ry \to Pyt ) ) \to Pxt ) )

(C) \forallx ( Ax \to Rx )

Or all together (P1 ∧ P2 ∧ P3 ⇒ C)

\existst ( Tt \land \forallx (Hx \to (Rx \leftrightarrow Pxt ) ) ) \land \forallt ( Tt \land ( \forallx (Hx \to ( Rx \leftrightarrow Pxt)) \to \forallx (Rx \leftrightarrow Pxt))) \land \forallx (Ax \to \neg \existst (Tt \land \negPxt \land (\forally (Hy \to ( \negPyt \to \negRy))))) \to \forallx ( Ax \to Rx )

which yields valid

Note that without the modification of premise 1 to require human moral value to be based on trait, and the addition of the premise to forbid double standards, the argument would not be even close to valid, which is the case for the original NTT formulation.

Natural Deduction

First we will prove the following to make our proof simpler:

∀x( SNAx ⇒ ¬∃t ( Tt ∧ ¬Pxt ∧ ∀y ( Hy ⇒ ( ¬Pyt ⇒ ¬Ry ) ) ) ) ⇔ ∀x( SNAx ⇒ ∀t ( Tt ∧ ∀y ( Hy ⇒ ( Ry ⇒ Pyt ) ) ⇒ Pxt ) )

Starting with the left-hand-side (LHS)

LHS	⇔ ∀x( SNAx ⇒ ¬∃t ( Tt ∧ ¬Pxt ∧ ∀y ( Hy ⇒ ( ¬Pyt ⇒ ¬Ry ) ) ) )
	⇔ ∀x( SNAx ⇒ ∀t ¬( Tt ∧ ¬Pxt ∧ ∀y ( Hy ⇒ ( ¬Pyt ⇒ ¬Ry ) ) ) )	(¬∃x Px) ⇔ (∀x ¬Px)
	⇔ ∀x( SNAx ⇒ ∀t( Tt ∧ ¬Pxt ⇒ ¬∀y ( Hy ⇒ ( ¬Pyt ⇒ ¬Ry ) ) ) )	¬(p∧q) ⇔ (p⇒¬q)
	⇔ ∀x( SNAx ⇒ ∀t( Tt ∧ ¬Pxt ⇒ ¬∀y ( Hy ⇒ ( Ry ⇒ Pyt ) ) ) )	(p⇒q) ⇔ (¬q⇒¬p)
	⇔ ∀x( SNAx ⇒ ∀t( Tt ∧ ∀y ( Hy ⇒ ( Ry ⇒ Pyt ) ) ⇒ Pxt) )	(p⇒q) ⇔ (¬q⇒¬p)
	⇔ RHS

Hence we have shown the equivalency.

Now we can prove the validity of the argument using natural deduction.

Natural Deduction Proof of Validity

1	∃t ( Tt ∧ ∀x ( Hx ⇒ ( Rx ⇔ Pxt ) ) )	assumption (P1)
2	∀t ( Tt ∧ ( ∀x ( Hx ⇒ ( Rx ⇔ Pxt ) ) ⇒ ∀x ( Rx ⇔ Pxt ) ) )	assumption (P2)
3	∀x( SNAx ⇒ ∀t ( Tt ∧ ∀y ( Hy ⇒ ( Ry ⇒ Pyt ) ) ⇒ Pxt ) )	assumption (P3)
4	Ts ∧ ∀x ( Hx ⇒ ( Rx ⇔ Pxs ) )	existential elimination	1
5	Ts ∧ ( Ha ⇒ ( Ra ⇔ Pas ) )	universal elimination	4
6	Ts ∧ ( ( Ha ⇒ ( Ra ⇔ Pas ) ) ⇒ ( Rb ⇔ Pbs ) )	universal elimination	2
7	SNAb ⇒ ( Ts ∧ ( Ha ⇒ ( Ra ⇒ Pas ) ) ⇒ Pbs )	universal elimination	3
8	¬ ( SNAb ∧ ¬ ( Ts ∧ ( Ha ⇒ ( Ra ⇒ Pas ) ) ⇒ Pbs ) )	( p ⇒ q ) ⇔ ¬( p ∧ ¬q )	7
9	¬ ( SNAb ∧ ¬ ¬( Ts ∧ ( Ha ⇒ ( Ra ⇒ Pas ) ) ∧ ¬ Pbs ) )	(p ⇒ q) ⇔ ¬(p ∧ ¬q)	8
10	¬ ( SNAb ∧ ( Ts ∧ ( Ha ⇒ ( Ra ⇒ Pas ) ) ∧ ¬ Pbs ) )	negation elimination	9
11	¬ ( SNAb ∧ ¬ Pbs ∧ ( Ts ∧ ( Ha ⇒ ( Ra ⇒ Pas ) ) ) )	∧ commutivity	10
12	SNAb ∧ ¬ Pbs ⇒ ¬ ( Ts ∧ ( Ha ⇒ ( Ra ⇒ Pas ) ) )	¬( p ∧ q) = (p ⇒ ¬q)	11
13	¬ (SNAb ⇒ Pbs) ⇒ ¬ ( Ts ∧ ( Ha ⇒ ( Ra ⇒ Pas ) ) )	¬(p ⇒ q) ⇔ (p ∧ ¬q)	12
14	( Ts ∧ ( Ha ⇒ ( Ra ⇒ Pas ) ) ) ⇒ (SNAb ⇒ Pbs)	(¬p ⇒ ¬q) ⇔ (q ⇒ p)	13
15	Ts ∧ ¬( Ha ∧ ¬ ( Ra ⇔ Pas ) )	(p⇒q) ⇔ ¬(p∧¬q)	5
16	Ts ∧ ¬( Ha ∧ ¬ ( (Ra ⇒ Pas) ∧ (Pas ⇒ Ra) ) )	biconditional elimination	15
17	Ts ∧ ¬ ( Ha ∧ (¬ (Ra ⇒ Pas) ∨ ¬(Pas ⇒ Ra) ) )	¬(p ∧ q) = ¬p ∨ ¬q	16
18	Ts ∧ ¬ ( (Ha ∧ ¬ (Ra ⇒ Pas) ) ∨ (Ha ∧ ¬( Pas ⇒ Ra ) ) )	p ∧ (q ∨ r ) = (p ∧ q) ∨ (p ∧ r)	17
19	Ts ∧ ¬ (Ha ∧ ¬ (Ra ⇒ Pas) ) ∧ ¬ (Ha ∧ ¬( Pas ⇒ Ra ) )	¬ (p ∨ q) = (¬p ∧ ¬q)	18
20	Ts ∧ (Ha ⇒ (Ra ⇒ Pas)) ∧ (Ha ⇒ (Pas ⇒ Ra) )	( p ⇒ q ) ⇔ ¬ ( p ∧ ¬q )	19
21	Ts ∧ (Ha ⇒ (Ra ⇒ Pas))	∧ elimination	20
22	SNAb ⇒ Pbs	Modus Ponens	14, 21
23	Rb ⇔ Pbs	Modus Ponens	6, 5
24	(Rb ⇒ Pbs) ∧ (Pbs ⇒ Rb)	biconditional elimination	23
25	Pbs ⇒ Rb	∧ elimination	24
26	SNAb ⇒ Rb	transitivity	22, 25
27	∀x (SNAx ⇒ Rx)	universal introduction (C)	26