Difference between revisions of "NameTheTrait 2.0"

From Philosophical Vegan Wiki
Jump to: navigation, search
(In English)
(In English)
Line 26: Line 26:
  
  
Where R refers to the right to life (or to not be killed), in the absence of mitigating circumstances, which under current western conditions, does not include for food or for fun
+
Where R refers to the right to life (or to not be killed), in the absence of mitigating circumstances, which under current western conditions, do not include for food or for fun
  
 
=Defense of Premises=
 
=Defense of Premises=

Revision as of 07:47, 16 December 2017

It is possible to correct the NTT argument and preserve persuasive force by adding a premise that rejects double standards and changing the first premise to require human moral value to be based on a trait. This makes NTT valid, and allows it to be presented in the same way as it was intended.

In English

(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

(P3) If an individual is a sentient nonhuman animal, then the trait that gives R to humans 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)


Where R refers to the right to life (or to not be killed), in the absence of mitigating circumstances, which under current western conditions, do not include for food or for fun

Defense of Premises

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
Therefore (C) for all x, if x is a sentient nonhuman animal then x has R

where R is the right to not be exploited AFAPP.

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