The task is to show that the given sequence (line 2) is a consequence of a formula. The formula is a translation of the English sentence: There is one and only one God. The conclusion (the given sequence) reads: Something that is a God has property 'F' if and only if anything that is a God has property 'F'. Perhaps the most valuable hints here are that: a) the universal quantifier on line 6 can be instantiated again, to a constant (here 'a') on line 11, and b) that the universal quantifier can be instantiated to the same constant (here 'a' on line 24 and 25) as the existential quantifier. Then it is just a matter of assuming a = a, without any justification. There is no reason to worry about using the same constant again after line 22 because all previous assumptions have been discharged.
- (∃x)(y)(y = x ≡ Gy)
- ∴ (∃x)(Gx • Fx) ≡ (x)(Gx ⊃ Fx)
- * (∃x)(Gx • Fx) / ACP
- ** Gx / ACP
- ** Ga • Fa / 3EI x/a
- ** (y)(y = m ≡ Gy) / 1EI x/m
- ** x = m ≡ Gx / 6UI / y/x
- ** (x = m ⊃ Gx) • (Gx ⊃ x = m) / 7BE
- ** Gx ⊃ x = m / 8Simp
- ** x = m / 4,9MP
- ** a = m ≡ Ga / 6UI y/a
- ** (a = m ⊃ Ga) • (Ga ⊃ a = m) / 11BE
- ** Ga ⊃ a = m / 12Simp
- ** Ga / 5Simp
- ** a = m / 14,13MP
- ** m = a / 15Id
- ** x = a / 10,16Id
- ** Fa / 5Simp
- ** Fx / 17,18Id
- * Gx ⊃Fx / 4 - 19CP
- * (x)(Gx ⊃Fx) / 20UG
- (∃x)(Gx • Fx) ⊃(x)(Gx ⊃Fx) / 3 - 21CP
- * (x)(Gx ⊃Fx) / ACP
- * (y)(y = a ≡ Gy) / 1EI x/a
- * a = a ≡ Ga / 24UI y/a
- * (a = a ⊃Ga) • (Ga ⊃a = a) / 25BE
- * a = a ⊃Ga / 26Simp
- * a = a / Id
- * Ga / 27,28MP
- * Ga ⊃Fa / 23UI x/a
- * Fa / 29,30MP
- * Ga • Fa / 30,31Conj.
- * (∃x)(Gx • Fx) / 32EG
- (x)(Gx ⊃Fx) ⊃(∃x)(Gx • Fx) / 23 - 33CP
- [(∃x)(Gx • Fx) ⊃(x)(Gx ⊃Fx)] • [(x)(Gx ⊃Fx) ⊃(∃x)(Gx • Fx)] / 22,34Conj.
- (∃x)(Gx • Fx) ≡ (x)(Gx ⊃ Fx) / 35BE
No comments:
Post a Comment