24.400 Proseminar in philosophy I Fall 2003 Some Grundlagen easy-to-prove theorems (HP) ∀F∀G(#F = #G ↔ F ≈ G) Definitions ‘0’ is defined as ‘#[x: x≠x]’ (§74) ‘1’ is defined as ‘#[x: x=0]’ (§77) ⎡Snm⎤ (⎡n is the successor of m⎤) is defined as: ⎡∃F∃x(Fx & #F = n & #[y: Fy & y≠x] = m)⎤ ( §76) ⎡Zx⎤ (⎡x is a Number⎤) is defined as: ⎡∃F(#F = x)⎤ (§72) [⎡Nx⎤ (⎡x is a finite Number⎤) is defined as: ⎡∀F((∀x(Sx0 ⊃ Fx) & ∀y(Fy ⊃ ∀z(Szy ⊃ Fz)) ⊃ Fx) v x = 0⎤ ( §83)] Theorems 1. ∀F(#F = 0 ↔ ∀x~Fx) (§75) Proof. Suppose #F = 0, i.e. #F = #[x: x≠x]. By (HP), F ≈ [x: x≠x]. By the definition of ‘≈’: ∃R(∀x(Fx ⊃ ∃1y([x: x≠x]y & Rxy)) & ∀y([x: x≠x]y ⊃ ∃1x(Fx &Rxy))) Since ~∃y[x: x≠x]y, ~∃1y([x: x≠x]y & Rxy), for any R, x, so ∀x~Fx. Similarly for the other direction. 2. ∀xSx0 ⊃ x = 1 (§78, 1) 3. ∀F(#F = 1 ⊃ ∃xFx) (§78, 2) 4. ∀F(#F = 1 ⊃ ∀x∀y((Fx & Fy) ⊃ x = y) (§78, 3) 5. ∀F(∃xFx & ∀x∀y((Fx & Fy) ⊃ x = y) ⊃ #F = 1) (§78, 4)6. ∀x∀y∀x′∀y′Sxy & Sx′y′ ⊃ (x = x′ ↔ y = y′) (§78, 5) 7. ∀x(Zx & x ≠ 0 ⊃ ∃y(Zy & Sxy)) (§78,