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

(only humans who possess a certain trait have R)

(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 - Most people will agree that humans have R if and only if have have a certain trait, and that this trait is the capacity for sentience, as we (society) do not grant R to brain-dead humans with no possibility of recovery.

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 capacity for sentience is what grants humans R, then they must agree with this premise.

Note that by defining R in the way we have, we avoid issues that would be present if R was instead, moral value or the right to non-exploitation, as many people would believe that insentient humans have moral value and the right to non-exploitation, which may lead them to reject P1.

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