Return to Answer

1. P(1) ∧ ∀m∈N[P(m) → P(m')] [OSC1]
2. ~∀m∈N[P(m)] [OSC2]
3. ∃m∈N[~P(m)] [2; QN]
4. n ∈N ∧ ~P(n) [3; EI]
5. ~P(n) [4; simplification 2]
6. n = 0⁽ⁿ⁾ [Df]
7. ~P(0⁽ⁿ⁾) [5,6; substitution]
8. P(0') [1; simplification 1]
9. If P(0') then P(0'') [1; UI]
10. P(0'') [8,9; MP X 1]
11. If P(0'') then P(0''') [1; UI]
12. P(0''') [10,11; MP X 2] ...
13. P(0⁽ⁿ⁾) [MP X n-1]
14. P(0⁽ⁿ⁾) ∧ ~P(0⁽ⁿ⁾) [13,7; conjunction]
15. If~∀m∈N[P(m)] then contradiction [2-15; CSC2]
16. ∀m∈N[P(m)] [15; RAA]
17. If P(1) ∧ ∀m∈N[P(m) → P(m')] then ∀m∈N[P(m)] [1-16; CSC1]

1. P(1) ∧ ∀m∈N[P(m) → P(m')] [OSC1]
2. ~∀m∈N[P(m)] [OSC2]
3. ∃m∈N[~P(m)] [2; QN]
4. n ∈N ∧ ~P(n) [3; EI]
5. ~P(n) [4; simplification 2]
6. n = 0⁽ⁿ⁾ [Df]
7. ~P(0⁽ⁿ⁾) [5,6; substitution]
8. P(0') [1; simplification 1]
9. If P(0') then P(0'') [1; UI]
10. P(0'') [8,9; MP X 1]
11. If P(0'') then P(0''') [1; UI]
12. P(0''') [10,11; MP X 2] ...
13. P(0⁽ⁿ⁾) [MP X n-1]
14. P(0⁽ⁿ⁾) ∧ ~P(0⁽ⁿ⁾) [13,7; conjunction]
15. If~∀m∈N[P(m)] then contradiction [2-14; CSC2]
16. ∀m∈N[P(m)] [15; RAA]
17. If P(1) ∧ ∀m∈N[P(m) → P(m')] then ∀m∈N[P(m)] [1-16; CSC1]

1. P(1) ∧ ∀m∈N[P(m) → P(m')] [OSC1]
2. ~∀m∈N[P(m)] [OSC2]
3. ∃m∈N[~P(m)] [2; QN]
4. n ∈N ∧ ~P(n) [3; EI]
5. ~P(n) [4; simplification 2]
6. n = 0⁽ⁿ⁾ [Df]
7. ~P(0⁽ⁿ⁾) [5,6; substitution]
8. P(0') [1; simplification 1]
9. If P(0') then P(0'') [1; UI]
10. P(0'') [8,9; MP X 1]
11. If P(0'') then P(0''') [1; UI]
12. P(0''') [10,11; MP X 2] ...
13. P(0⁽ⁿ⁾) [MP X n-1]
14. P(0⁽ⁿ⁾) ∧ ~P(0⁽ⁿ⁾) [13,7; conjunction]
15. If~∀m∈N[P(m)] then contradiction [2-15; CSC2]
16. ∀m∈N[P(m)]
17. If P(1) ∧ ∀m∈N[P(m) → P(m')] then ∀m∈N[P(m)] [1-16; CSC1]

1. P(1) ∧ ∀m∈N[P(m) → P(m')] [OSC1]
2. ~∀m∈N[P(m)] [OSC2]
3. ∃m∈N[~P(m)] [2; QN]
4. n ∈N ∧ ~P(n) [3; EI]
5. ~P(n) [4; simplification 2]
6. n = 0⁽ⁿ⁾ [Df]
7. ~P(0⁽ⁿ⁾) [5,6; substitution]
8. P(0') [1; simplification 1]
9. If P(0') then P(0'') [1; UI]
10. P(0'') [8,9; MP X 1]
11. If P(0'') then P(0''') [1; UI]
12. P(0''') [10,11; MP X 2] ...
13. P(0⁽ⁿ⁾) [MP X n-1]
14. P(0⁽ⁿ⁾) ∧ ~P(0⁽ⁿ⁾) [13,7; conjunction]
15. If~∀m∈N[P(m)] then contradiction [2-15; CSC2]
16. ∀m∈N[P(m)] [15; RAA]
17. If P(1) ∧ ∀m∈N[P(m) → P(m')] then ∀m∈N[P(m)] [1-16; CSC1]

A1 states "x=1 ∨ ∃y (x=y' ∧ y ∈ N)" is a sufficient condition for x to denote a natural number.

A4 states that condition is necessary for x to denote a natural number.