Difference between revisions of "NameTheTrait 2.0"
(→Natural Deduction) |
(→Natural Deduction) |
||
Line 119: | Line 119: | ||
{| class="wikitable" | {| class="wikitable" | ||
|+Natural Deduction Proof of Validity | |+Natural Deduction Proof of Validity | ||
− | |1 || ∃t ( Tt ∧ ∀x ( Hx ⇒ ( Rx ⇔ Pxt ) ) ) || assumption '''(P1)''' | + | |1 || ∃t ( Tt ∧ ∀x ( Hx ⇒ ( Rx ⇔ Pxt ) ) ) || assumption '''(P1)''' || |
|- | |- | ||
− | |2 || ∀t ( Tt ∧ ( ∀x ( Hx ⇒ ( Rx ⇔ Pxt ) ) ⇒ ∀x ( Rx ⇔ Pxt ) ) ) || assumption '''(P2)''' | + | |2 || ∀t ( Tt ∧ ( ∀x ( Hx ⇒ ( Rx ⇔ Pxt ) ) ⇒ ∀x ( Rx ⇔ Pxt ) ) ) || assumption '''(P2)''' || |
|- | |- | ||
− | |3 || ∀x( SNAx ⇒ ∀t ( Tt ∧ ∀y ( Hy ⇒ ( Ry ⇒ Pyt ) ) ⇒ Pxt ) ) || assumption '''(P3)''' | + | |3 || ∀x( SNAx ⇒ ∀t ( Tt ∧ ∀y ( Hy ⇒ ( Ry ⇒ Pyt ) ) ⇒ Pxt ) ) || assumption '''(P3)''' || |
|- | |- | ||
− | |4 || Ts ∧ ∀x ( Hx ⇒ ( Rx ⇔ Pxs ) ) ||existential elimination on line 1 | + | |4 || Ts ∧ ∀x ( Hx ⇒ ( Rx ⇔ Pxs ) ) ||existential elimination || on line 1 |
|- | |- | ||
− | |5 || Ts ∧ ( Ha ⇒ ( Ra ⇔ Pas ) ) ||universal elimination on line 4 | + | |5 || Ts ∧ ( Ha ⇒ ( Ra ⇔ Pas ) ) ||universal elimination || on line 4 |
|- | |- | ||
− | |6 || Ts ∧ ( ( Ha ⇒ ( Ra ⇔ Pas ) ) ⇒ ( Rb ⇔ Pbs ) ) ||universal elimination on line 2 | + | |6 || Ts ∧ ( ( Ha ⇒ ( Ra ⇔ Pas ) ) ⇒ ( Rb ⇔ Pbs ) ) ||universal elimination || on line 2 |
|- | |- | ||
− | |7 || SNAb ⇒ ( Ts ∧ ( Ha ⇒ ( Ra ⇒ Pas ) ) ⇒ Pbs )|| universal elimination on line 3 | + | |7 || SNAb ⇒ ( Ts ∧ ( Ha ⇒ ( Ra ⇒ Pas ) ) ⇒ Pbs )|| universal elimination || on line 3 |
|- | |- | ||
− | |8 || ¬ ( SNAb ∧ ¬ ( Ts ∧ ( Ha ⇒ ( Ra ⇒ Pas ) ) ⇒ Pbs ) ) || (p⇒q) ⇔ ¬(p∧¬q) on line 7 | + | |8 || ¬ ( SNAb ∧ ¬ ( Ts ∧ ( Ha ⇒ ( Ra ⇒ Pas ) ) ⇒ Pbs ) ) || (p⇒q) ⇔ ¬(p∧¬q) || on line 7 |
|- | |- | ||
− | |9 || ¬ ( SNAb ∧ ¬ ¬( Ts ∧ ( Ha ⇒ ( Ra ⇒ Pas ) ) ∧ ¬ Pbs ) ) || (p⇒q) ⇔ ¬(p∧¬q) on line 8 | + | |9 || ¬ ( SNAb ∧ ¬ ¬( Ts ∧ ( Ha ⇒ ( Ra ⇒ Pas ) ) ∧ ¬ Pbs ) ) || (p⇒q) ⇔ ¬(p∧¬q) || on line 8 |
|- | |- | ||
− | |10 || ¬ ( SNAb ∧ ( Ts ∧ ( Ha ⇒ ( Ra ⇒ Pas ) ) ∧ ¬ Pbs ) ) || negation elimination on line 9 | + | |10 || ¬ ( SNAb ∧ ( Ts ∧ ( Ha ⇒ ( Ra ⇒ Pas ) ) ∧ ¬ Pbs ) ) || negation elimination || on line 9 |
|- | |- | ||
− | |11 || ¬ ( SNAb ∧ ¬ Pbs ∧ ( Ts ∧ ( Ha ⇒ ( Ra ⇒ Pas ) ) ) ) || ∧ commutivity on line 10 | + | |11 || ¬ ( SNAb ∧ ¬ Pbs ∧ ( Ts ∧ ( Ha ⇒ ( Ra ⇒ Pas ) ) ) ) || ∧ commutivity || on line 10 |
|- | |- | ||
− | |12 || SNAb ∧ ¬ Pbs ⇒ ¬ ( Ts ∧ ( Ha ⇒ ( Ra ⇒ Pas ) ) ) || ¬( p ∧ q) = (p ⇒ ¬q) on line 11 | + | |12 || SNAb ∧ ¬ Pbs ⇒ ¬ ( Ts ∧ ( Ha ⇒ ( Ra ⇒ Pas ) ) ) || ¬( p ∧ q) = (p ⇒ ¬q) || on line 11 |
|- | |- | ||
− | |13 || ¬ (SNAb ⇒ Pbs) ⇒ ¬ ( Ts ∧ ( Ha ⇒ ( Ra ⇒ Pas ) ) ) || ¬(p⇒q) ⇔ (p∧¬q) | + | |13 || ¬ (SNAb ⇒ Pbs) ⇒ ¬ ( Ts ∧ ( Ha ⇒ ( Ra ⇒ Pas ) ) ) || ¬(p⇒q) ⇔ (p∧¬q) || on line 12 |
+ | |- | ||
+ | |14 || ( Ts ∧ ( Ha ⇒ ( Ra ⇒ Pas ) ) ) ⇒ (SNAb ⇒ Pbs) || (~p -> ~q) ⇔ (q->p) || line 13 | ||
|- | |- | ||
− | | ||Ts ∧ ¬( Ha ∧ ¬ ( Ra ⇔ Pas ) ) || (p⇒q) ⇔ ¬(p∧¬q) on line 5 | + | |15 ||Ts ∧ ¬( Ha ∧ ¬ ( Ra ⇔ Pas ) ) || (p⇒q) ⇔ ¬(p∧¬q) || on line 5 |
|- | |- | ||
− | | ||Ts ∧ ¬( Ha ∧ ¬ ( (Ra ⇒ Pas) ∧ (Pas ⇒ Ra) ) ) || biconditional elimination | + | |16 ||Ts ∧ ¬( Ha ∧ ¬ ( (Ra ⇒ Pas) ∧ (Pas ⇒ Ra) ) ) || biconditional elimination || on line 14 |
|- | |- | ||
− | | ||Ts ∧ ¬ ( Ha ∧ ¬ (Ra ⇒ Pas) V ¬(Pas ⇒ Ra) ) ||¬(p∧q) = ¬pV¬q | + | |17 ||Ts ∧ ¬ ( Ha ∧ ¬ (Ra ⇒ Pas) V ¬(Pas ⇒ Ra) ) ||¬(p∧q) = ¬pV¬q || on line 15 |
|- | |- | ||
− | | || Ts ∧ ¬ (Ha ∧ ¬ (Ra ⇒ Pas))∧ ¬¬(Pas ⇒ Ra) || ¬(pVq) = ¬p ∧ ¬q | + | |18 || Ts ∧ ¬ (Ha ∧ ¬ (Ra ⇒ Pas))∧ ¬¬(Pas ⇒ Ra) || ¬(pVq) = ¬p ∧ ¬q || on line 16 |
|- | |- | ||
− | | ||Ts ∧ (Ha ⇒ (Ra ⇒ Pas)) ∧ (Pas ⇒ Ra) || (p⇒q) ⇔ ¬(p∧¬q) and negation elimination | + | |19 ||Ts ∧ (Ha ⇒ (Ra ⇒ Pas)) ∧ (Pas ⇒ Ra) || (p⇒q) ⇔ ¬(p∧¬q) || and negation elimination 17 |
|- | |- | ||
− | | ||Ts ∧ (Ha ⇒ (Ra ⇒ Pas)) || and elimination | + | |20 ||Ts ∧ (Ha ⇒ (Ra ⇒ Pas)) || and elimination || on line 18 |
|- | |- | ||
− | | | + | |21 || SNAb ⇒ Pbs || implication elimination || lines 14 and 20 |
|- | |- | ||
− | | | + | |22 || Rb ⇔ Pbs ||implication elimination || on lines 5 and 6 |
|- | |- | ||
− | | | + | |23 || SNAb ⇒ Rb || lines 14 and 15 || |
|- | |- | ||
− | | | + | |24 ||∀x (SNAx ⇒ Rx) ||universal introduction '''(C)'''|| |
|} | |} |
Revision as of 06:49, 14 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.
Contents
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 there exists a trait present in the individual, such that, humans that have R must possess the trait
- (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 be excluding from exploitation, as far as practical and possible.
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.
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 | on line 1 |
5 | Ts ∧ ( Ha ⇒ ( Ra ⇔ Pas ) ) | universal elimination | on line 4 |
6 | Ts ∧ ( ( Ha ⇒ ( Ra ⇔ Pas ) ) ⇒ ( Rb ⇔ Pbs ) ) | universal elimination | on line 2 |
7 | SNAb ⇒ ( Ts ∧ ( Ha ⇒ ( Ra ⇒ Pas ) ) ⇒ Pbs ) | universal elimination | on line 3 |
8 | ¬ ( SNAb ∧ ¬ ( Ts ∧ ( Ha ⇒ ( Ra ⇒ Pas ) ) ⇒ Pbs ) ) | (p⇒q) ⇔ ¬(p∧¬q) | on line 7 |
9 | ¬ ( SNAb ∧ ¬ ¬( Ts ∧ ( Ha ⇒ ( Ra ⇒ Pas ) ) ∧ ¬ Pbs ) ) | (p⇒q) ⇔ ¬(p∧¬q) | on line 8 |
10 | ¬ ( SNAb ∧ ( Ts ∧ ( Ha ⇒ ( Ra ⇒ Pas ) ) ∧ ¬ Pbs ) ) | negation elimination | on line 9 |
11 | ¬ ( SNAb ∧ ¬ Pbs ∧ ( Ts ∧ ( Ha ⇒ ( Ra ⇒ Pas ) ) ) ) | ∧ commutivity | on line 10 |
12 | SNAb ∧ ¬ Pbs ⇒ ¬ ( Ts ∧ ( Ha ⇒ ( Ra ⇒ Pas ) ) ) | ¬( p ∧ q) = (p ⇒ ¬q) | on line 11 |
13 | ¬ (SNAb ⇒ Pbs) ⇒ ¬ ( Ts ∧ ( Ha ⇒ ( Ra ⇒ Pas ) ) ) | ¬(p⇒q) ⇔ (p∧¬q) | on line 12 |
14 | ( Ts ∧ ( Ha ⇒ ( Ra ⇒ Pas ) ) ) ⇒ (SNAb ⇒ Pbs) | (~p -> ~q) ⇔ (q->p) | line 13 |
15 | Ts ∧ ¬( Ha ∧ ¬ ( Ra ⇔ Pas ) ) | (p⇒q) ⇔ ¬(p∧¬q) | on line 5 |
16 | Ts ∧ ¬( Ha ∧ ¬ ( (Ra ⇒ Pas) ∧ (Pas ⇒ Ra) ) ) | biconditional elimination | on line 14 |
17 | Ts ∧ ¬ ( Ha ∧ ¬ (Ra ⇒ Pas) V ¬(Pas ⇒ Ra) ) | ¬(p∧q) = ¬pV¬q | on line 15 |
18 | Ts ∧ ¬ (Ha ∧ ¬ (Ra ⇒ Pas))∧ ¬¬(Pas ⇒ Ra) | ¬(pVq) = ¬p ∧ ¬q | on line 16 |
19 | Ts ∧ (Ha ⇒ (Ra ⇒ Pas)) ∧ (Pas ⇒ Ra) | (p⇒q) ⇔ ¬(p∧¬q) | and negation elimination 17 |
20 | Ts ∧ (Ha ⇒ (Ra ⇒ Pas)) | and elimination | on line 18 |
21 | SNAb ⇒ Pbs | implication elimination | lines 14 and 20 |
22 | Rb ⇔ Pbs | implication elimination | on lines 5 and 6 |
23 | SNAb ⇒ Rb | lines 14 and 15 | |
24 | ∀x (SNAx ⇒ Rx) | universal introduction (C) |