Difference between revisions of "NameTheTrait 2.0"
(→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, | + | 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.
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 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.
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 |