Documentation

MathematicalLogic.SecondOrder.Theories.Peano

def SecondOrder.Language.peano :

Equations

SecondOrder.Language.peano = { Func := SecondOrder.Language.peano.Func✝, Rel := fun (x : ℕ) => Empty }

Instances For

instance SecondOrder.Language.peano.instZeroTerm {l : List Ty} :

Zero (peano.Term l)

Equations

SecondOrder.Language.peano.instZeroTerm = { zero := SecondOrder.Language.peano.Func.zero✝ ⬝ᶠ []ᵥ }

instance SecondOrder.Language.peano.instAddTerm {l : List Ty} :

Add (peano.Term l)

Equations

SecondOrder.Language.peano.instAddTerm = { add := fun (x1 x2 : SecondOrder.Language.peano.Term l) => SecondOrder.Language.peano.Func.add✝ ⬝ᶠ [x1, x2]ᵥ }

instance SecondOrder.Language.peano.instMulTerm {l : List Ty} :

Mul (peano.Term l)

Equations

SecondOrder.Language.peano.instMulTerm = { mul := fun (x1 x2 : SecondOrder.Language.peano.Term l) => SecondOrder.Language.peano.Func.mul✝ ⬝ᶠ [x1, x2]ᵥ }

def SecondOrder.Language.peano.succ {l : List Ty} (t : peano.Term l) :

Equations

SecondOrder.Language.peano.succ t = SecondOrder.Language.peano.Func.succ✝ ⬝ᶠ [t]ᵥ

Instances For

def SecondOrder.Language.peano.termS_ :

Lean.ParserDescr

Equations

One or more equations did not get rendered due to their size.

Instances For

instance SecondOrder.Language.peano.Nat :

peano.HasStructure ℕ

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem SecondOrder.Language.peano.Nat.interp_zero {l : List Ty} {ρ : Assignment ℕ l} :

⟦ 0 ⟧ₜ ℕ , ρ = 0

@[simp]

theorem SecondOrder.Language.peano.Nat.interp_succ {l : List Ty} {t : peano.Term l} {ρ : Assignment ℕ l} :

⟦ succ t ⟧ₜ ℕ , ρ = (⟦ t ⟧ₜ ℕ , ρ) + 1

@[simp]

theorem SecondOrder.Language.peano.Nat.interp_add {l : List Ty} {t₁ t₂ : peano.Term l} {ρ : Assignment ℕ l} :

⟦ t₁ + t₂ ⟧ₜ ℕ , ρ = (⟦ t₁ ⟧ₜ ℕ , ρ) + (⟦ t₂ ⟧ₜ ℕ , ρ)

@[simp]

theorem SecondOrder.Language.peano.Nat.interp_mul {l : List Ty} {t₁ t₂ : peano.Term l} {ρ : Assignment ℕ l} :

⟦ t₁ * t₂ ⟧ₜ ℕ , ρ = (⟦ t₁ ⟧ₜ ℕ , ρ) * (⟦ t₂ ⟧ₜ ℕ , ρ)

inductive SecondOrder.Language.Theory.PA₂ :

ax_succ_ne_zero : PA₂ (∀' (~ peano.succ #0 ≐ 0))
ax_succ_inj : PA₂ (∀' ∀' (peano.succ #1 ≐ peano.succ #0 ⇒ #1 ≐ #0))
ax_add_zero : PA₂ (∀' (#0 + 0 ≐ #0))
ax_add_succ : PA₂ (∀' ∀' (#1 + peano.succ #0 ≐ peano.succ (#1 + #0)))
ax_mul_zero : PA₂ (∀' (#0 * 0 ≐ 0))
ax_mul_succ : PA₂ (∀' ∀' (#1 * peano.succ #0 ≐ #1 * #0 + #1))
ax_ind : PA₂ (∀ʳ[1](0 ⬝ʳᵛ [0]ᵥ ⇒ ∀' (1 ⬝ʳᵛ [#0]ᵥ ⇒ 1 ⬝ʳᵛ [peano.succ #0]ᵥ) ⇒ ∀' (1 ⬝ʳᵛ [#0]ᵥ)))

Instances For

instance SecondOrder.Language.Theory.PA₂.instIsModelNat :

PA₂.IsModel ℕ

instance SecondOrder.Language.Theory.PA₂.instZeroDom {M : PA₂.Model} :

Equations

SecondOrder.Language.Theory.PA₂.instZeroDom = { zero := M.interpFunc SecondOrder.Language.peano.Func.zero✝ []ᵥ }

instance SecondOrder.Language.Theory.PA₂.instAddDom {M : PA₂.Model} :

Equations

SecondOrder.Language.Theory.PA₂.instAddDom = { add := fun (x1 x2 : M.Dom) => M.interpFunc SecondOrder.Language.peano.Func.add✝ [x1, x2]ᵥ }

instance SecondOrder.Language.Theory.PA₂.instMulDom {M : PA₂.Model} :

Equations

SecondOrder.Language.Theory.PA₂.instMulDom = { mul := fun (x1 x2 : M.Dom) => M.interpFunc SecondOrder.Language.peano.Func.mul✝ [x1, x2]ᵥ }

def SecondOrder.Language.Theory.PA₂.succ {M : PA₂.Model} (u : M.Dom) :

Equations

SecondOrder.Language.Theory.PA₂.succ u = M.interpFunc SecondOrder.Language.peano.Func.succ✝ [u]ᵥ

Instances For

@[simp]

theorem SecondOrder.Language.Theory.PA₂.interp_zero {l : List Ty} {M : PA₂.Model} {ρ : Assignment M.Dom l} :

⟦ 0 ⟧ₜ M.Dom, ρ = 0

@[simp]

theorem SecondOrder.Language.Theory.PA₂.interp_succ {l : List Ty} {M : PA₂.Model} {t : peano.Term l} {ρ : Assignment M.Dom l} :

⟦ peano.succ t ⟧ₜ M.Dom, ρ = succ (⟦ t ⟧ₜ M.Dom, ρ)

@[simp]

theorem SecondOrder.Language.Theory.PA₂.interp_add {l : List Ty} {M : PA₂.Model} {t₁ t₂ : peano.Term l} {ρ : Assignment M.Dom l} :

⟦ t₁ + t₂ ⟧ₜ M.Dom, ρ = (⟦ t₁ ⟧ₜ M.Dom, ρ) + (⟦ t₂ ⟧ₜ M.Dom, ρ)

@[simp]

theorem SecondOrder.Language.Theory.PA₂.interp_mul {l : List Ty} {M : PA₂.Model} {t₁ t₂ : peano.Term l} {ρ : Assignment M.Dom l} :

⟦ t₁ * t₂ ⟧ₜ M.Dom, ρ = (⟦ t₁ ⟧ₜ M.Dom, ρ) * (⟦ t₂ ⟧ₜ M.Dom, ρ)

def SecondOrder.Language.Theory.PA₂.ofNat {M : PA₂.Model} :

ℕ → M.Dom

Equations

Instances For

theorem SecondOrder.Language.Theory.PA₂.ofNat_injective {M : PA₂.Model} :

Function.Injective ofNat

theorem SecondOrder.Language.Theory.PA₂.ofNat_surjective {M : PA₂.Model} :

Function.Surjective ofNat

theorem SecondOrder.Language.Theory.PA₂.ofNat_add {M : PA₂.Model} {n m : ℕ} :

ofNat (n + m) = ofNat n + ofNat m

theorem SecondOrder.Language.Theory.PA₂.ofNat_mul {M : PA₂.Model} {n m : ℕ} :

ofNat (n * m) = ofNat n * ofNat m

theorem SecondOrder.Language.Theory.PA₂.iso_Nat (M : PA₂.Model) :

Nonempty (M.toStructure ≃ᴹ Structure.of ℕ)

theorem SecondOrder.Language.Theory.PA₂.categorical :

PA₂.Categorical