Theory of first-order arithmetic #

This file formalizes Peano arithmetic and Robinson's Q, two first-order theories of arithmetic. The goal is to prove Gödel's first incompleteness theorem under Q and second incompleteness theorem under PA.

source

inductive FirstOrder.Language.peanoFunc :

ℕ → Type

zero : peanoFunc 0
succ : peanoFunc 1
add : peanoFunc 2
mul : peanoFunc 2

Instances For

source

def FirstOrder.Language.peano :

Language

The language of first-order arithmetic.

Equations

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

Instances For

source

def FirstOrder.Language.peano.succ {n : ℕ} (t : peano.Term n) :

peano.Term n

Equations

FirstOrder.Language.peano.succ t = FirstOrder.Language.peanoFunc.succ ⬝ᶠ [t]ᵥ

Instances For

source

def FirstOrder.Language.peano.termS :

Lean.ParserDescr

Equations

FirstOrder.Language.peano.termS = Lean.ParserDescr.node `FirstOrder.Language.peano.termS 1024 (Lean.ParserDescr.symbol "S")

Instances For

source

instance FirstOrder.Language.peano.instZeroTerm {n : ℕ} :

Zero (peano.Term n)

Equations

FirstOrder.Language.peano.instZeroTerm = { zero := FirstOrder.Language.peanoFunc.zero ⬝ᶠ []ᵥ }

source

instance FirstOrder.Language.peano.instOneTerm {n : ℕ} :

One (peano.Term n)

Equations

FirstOrder.Language.peano.instOneTerm = { one := FirstOrder.Language.peano.succ 0 }

source

instance FirstOrder.Language.peano.instAddTerm {n : ℕ} :

Add (peano.Term n)

Equations

FirstOrder.Language.peano.instAddTerm = { add := fun (x1 x2 : FirstOrder.Language.peano.Term n) => FirstOrder.Language.peanoFunc.add ⬝ᶠ [x1, x2]ᵥ }

source

instance FirstOrder.Language.peano.instMulTerm {n : ℕ} :

Mul (peano.Term n)

Equations

FirstOrder.Language.peano.instMulTerm = { mul := fun (x1 x2 : FirstOrder.Language.peano.Term n) => FirstOrder.Language.peanoFunc.mul ⬝ᶠ [x1, x2]ᵥ }

source

def FirstOrder.Language.peano.ofNat {n : ℕ} :

ℕ → peano.Term n

Equations

Instances For

source

instance FirstOrder.Language.peano.instCoeNatTerm {m : ℕ} :

Coe ℕ (peano.Term m)

Equations

FirstOrder.Language.peano.instCoeNatTerm = { coe := FirstOrder.Language.peano.ofNat }

source

def FirstOrder.Language.peano.ofEncode {n : ℕ} {α : Type u_1} [Encodable α] (a : α) :

peano.Term n

Equations

FirstOrder.Language.peano.ofEncode a = FirstOrder.Language.peano.ofNat (Encodable.encode a)

Instances For

source

def FirstOrder.Language.peano.«term⌜_⌝» :

Lean.ParserDescr

Equations

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

Instances For

source

@[simp]

theorem FirstOrder.Language.peano.zero_eq {n : ℕ} :

peanoFunc.zero ⬝ᶠ []ᵥ = 0

source

@[simp]

theorem FirstOrder.Language.peano.succ_eq {n : ℕ} {t₁ : peano.Term n} :

peanoFunc.succ ⬝ᶠ [t₁]ᵥ = succ t₁

source

@[simp]

theorem FirstOrder.Language.peano.add_eq {n : ℕ} {t₁ t₂ : peano.Term n} :

peanoFunc.add ⬝ᶠ [t₁, t₂]ᵥ = t₁ + t₂

source

@[simp]

theorem FirstOrder.Language.peano.mul_eq {n : ℕ} {t₁ t₂ : peano.Term n} :

peanoFunc.mul ⬝ᶠ [t₁, t₂]ᵥ = t₁ * t₂

source

theorem FirstOrder.Language.peano.ofNat_zero {n : ℕ} :

ofNat 0 = 0

source

theorem FirstOrder.Language.peano.ofNat_succ {n a : ℕ} :

ofNat (a + 1) = succ (ofNat a)

source

theorem FirstOrder.Language.peano.one_def {n : ℕ} :

1 = succ 0

source

@[simp]

theorem FirstOrder.Language.peano.ofNat_one {n : ℕ} :

ofNat 1 = 1

source

@[simp]

theorem FirstOrder.Language.peano.subst_zero {n m✝ : ℕ} {σ : peano.Subst n m✝} :

0[σ]ₜ = 0

source

@[simp]

theorem FirstOrder.Language.peano.subst_succ {n : ℕ} {t : peano.Term n} {m✝ : ℕ} {σ : peano.Subst n m✝} :

(succ t)[σ]ₜ = succ t[σ]ₜ

source

@[simp]

theorem FirstOrder.Language.peano.subst_one {n m✝ : ℕ} {σ : peano.Subst n m✝} :

1[σ]ₜ = 1

source

@[simp]

theorem FirstOrder.Language.peano.subst_add {n : ℕ} {t₁ t₂ : peano.Term n} {m✝ : ℕ} {σ : peano.Subst n m✝} :

(t₁ + t₂)[σ]ₜ = t₁[σ]ₜ + t₂[σ]ₜ

source

@[simp]

theorem FirstOrder.Language.peano.subst_mul {n : ℕ} {t₁ t₂ : peano.Term n} {m✝ : ℕ} {σ : peano.Subst n m✝} :

(t₁ * t₂)[σ]ₜ = t₁[σ]ₜ * t₂[σ]ₜ

source

@[simp]

theorem FirstOrder.Language.peano.subst_ofNat {n n✝ m✝ : ℕ} {σ : peano.Subst n✝ m✝} :

(ofNat n)[σ]ₜ = ofNat n

source

@[simp]

theorem FirstOrder.Language.peano.subst_ofEncode {α : Type u_1} {n✝ m✝ : ℕ} {σ : peano.Subst n✝ m✝} [Encodable α] {a : α} :

(ofEncode a)[σ]ₜ = ofEncode a

source

instance FirstOrder.Language.peano.instOrder :

peano.Order

Equations

FirstOrder.Language.peano.instOrder = { leDef := ∃' (#0 + #1 ≐ #2), ltDef := ∃' (#0 + FirstOrder.Language.peano.succ #1 ≐ #2) }

source

theorem FirstOrder.Language.peano.le_def {n : ℕ} {t₁ t₂ : peano.Term n} :

t₁ ⪯ t₂ = ∃' (#0 + ↑ₜt₁ ≐ ↑ₜt₂)

source

theorem FirstOrder.Language.peano.lt_def {n : ℕ} {t₁ t₂ : peano.Term n} :

t₁ ≺ t₂ = succ t₁ ⪯ t₂

source

theorem FirstOrder.Language.peano.eq_congr_succ {n : ℕ} {t₁ t₂ : peano.Term n} {Γ : peano.FormulaSet n} :

Γ ⊢ t₁ ≐ t₂ ⇒ succ t₁ ≐ succ t₂

source

theorem FirstOrder.Language.peano.eq_congr_add {n : ℕ} {t₁ t₂ : peano.Term n} {Γ : peano.FormulaSet n} {t₁' t₂' : peano.Term n} :

Γ ⊢ t₁ ≐ t₁' ⇒ t₂ ≐ t₂' ⇒ t₁ + t₂ ≐ t₁' + t₂'

source

theorem FirstOrder.Language.peano.eq_congr_mul {n : ℕ} {t₁ t₂ : peano.Term n} {Γ : peano.FormulaSet n} {t₁' t₂' : peano.Term n} :

Γ ⊢ t₁ ≐ t₁' ⇒ t₂ ≐ t₂' ⇒ t₁ * t₂ ≐ t₁' * t₂'

source

instance FirstOrder.Language.peano.instRepr :

peano.Repr

Equations

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

source

inductive FirstOrder.Language.Theory.Q :

peano.Theory

Robinson's Q.

ax_succ_ne_zero : Q (∀' (~ peano.succ #0 ≐ 0))
ax_succ_inj : Q (∀' ∀' (peano.succ #1 ≐ peano.succ #0 ⇒ #1 ≐ #0))
ax_add_zero : Q (∀' (#0 + 0 ≐ #0))
ax_add_succ : Q (∀' ∀' (#1 + peano.succ #0 ≐ peano.succ (#1 + #0)))
ax_mul_zero : Q (∀' (#0 * 0 ≐ 0))
ax_mul_succ : Q (∀' ∀' (#1 * peano.succ #0 ≐ #1 * #0 + #1))
ax_zero_or_succ : Q (∀' (#0 ≐ 0 ⩒ ∃' (#1 ≐ peano.succ #0)))

Instances For

source

theorem FirstOrder.Language.Theory.Q.succ_ne_zero {n : ℕ} (t : peano.Term n) :

↑ᵀ^[n] Q ⊢ ~ peano.succ t ≐ 0

source

theorem FirstOrder.Language.Theory.Q.succ_inj {n : ℕ} {t₁ t₂ : peano.Term n} :

↑ᵀ^[n] Q ⊢ peano.succ t₁ ≐ peano.succ t₂ ⇒ t₁ ≐ t₂

source

theorem FirstOrder.Language.Theory.Q.add_zero {n : ℕ} (t : peano.Term n) :

↑ᵀ^[n] Q ⊢ t + 0 ≐ t

source

theorem FirstOrder.Language.Theory.Q.add_succ {n : ℕ} (t₁ t₂ : peano.Term n) :

↑ᵀ^[n] Q ⊢ t₁ + peano.succ t₂ ≐ peano.succ (t₁ + t₂)

source

theorem FirstOrder.Language.Theory.Q.add_one {n : ℕ} (t : peano.Term n) :

↑ᵀ^[n] Q ⊢ t + 1 ≐ peano.succ t

source

theorem FirstOrder.Language.Theory.Q.mul_zero {n : ℕ} (t : peano.Term n) :

↑ᵀ^[n] Q ⊢ t * 0 ≐ 0

source

theorem FirstOrder.Language.Theory.Q.mul_succ {n : ℕ} (t₁ t₂ : peano.Term n) :

↑ᵀ^[n] Q ⊢ t₁ * peano.succ t₂ ≐ t₁ * t₂ + t₁

source

theorem FirstOrder.Language.Theory.Q.zero_or_succ {n : ℕ} (t : peano.Term n) :

↑ᵀ^[n] Q ⊢ t ≐ 0 ⩒ ∃' (↑ₜt ≐ peano.succ #0)

source

theorem FirstOrder.Language.Theory.Q.succ_inj_iff {n : ℕ} {t₁ t₂ : peano.Term n} :

↑ᵀ^[n] Q ⊢ peano.succ t₁ ≐ peano.succ t₂ ⇔ t₁ ≐ t₂

source

theorem FirstOrder.Language.Theory.Q.add_eq_zero_iff {n : ℕ} {t₁ t₂ : peano.Term n} :

↑ᵀ^[n] Q ⊢ t₁ + t₂ ≐ 0 ⇔ t₁ ≐ 0 ⩑ t₂ ≐ 0

source

theorem FirstOrder.Language.Theory.Q.le_of_add_eq {n : ℕ} {t₁ t₂ t₃ : peano.Term n} :

↑ᵀ^[n] Q ⊢ t₁ + t₂ ≐ t₃ ⇒ t₂ ⪯ t₃

source

theorem FirstOrder.Language.Theory.Q.zero_le {n : ℕ} {t : peano.Term n} :

↑ᵀ^[n] Q ⊢ 0 ⪯ t

source

theorem FirstOrder.Language.Theory.Q.succ_not_le_zero {n : ℕ} {t : peano.Term n} :

↑ᵀ^[n] Q ⊢ ~ peano.succ t ⪯ 0

source

theorem FirstOrder.Language.Theory.Q.le_zero_iff_eq_zero {n : ℕ} {t : peano.Term n} :

↑ᵀ^[n] Q ⊢ t ⪯ 0 ⇔ t ≐ 0

source

theorem FirstOrder.Language.Theory.Q.succ_le_iff_lt {n : ℕ} {t₁ t₂ : peano.Term n} :

↑ᵀ^[n] Q ⊢ peano.succ t₁ ⪯ t₂ ⇔ t₁ ≺ t₂

source

theorem FirstOrder.Language.Theory.Q.one_le_iff_zero_lt {n : ℕ} {t : peano.Term n} :

↑ᵀ^[n] Q ⊢ 1 ⪯ t ⇔ 0 ≺ t

source

theorem FirstOrder.Language.Theory.Q.succ_le_succ_iff {n : ℕ} {t₁ t₂ : peano.Term n} :

↑ᵀ^[n] Q ⊢ peano.succ t₁ ⪯ peano.succ t₂ ⇔ t₁ ⪯ t₂

source

theorem FirstOrder.Language.Theory.Q.not_lt_zero {n : ℕ} {t : peano.Term n} :

↑ᵀ^[n] Q ⊢ ~ t ≺ 0

source

theorem FirstOrder.Language.Theory.Q.lt_succ_iff_le {n : ℕ} {t₁ t₂ : peano.Term n} :

↑ᵀ^[n] Q ⊢ t₁ ≺ peano.succ t₂ ⇔ t₁ ⪯ t₂

source

theorem FirstOrder.Language.Theory.Q.succ_lt_succ_iff {n : ℕ} {t₁ t₂ : peano.Term n} :

↑ᵀ^[n] Q ⊢ peano.succ t₁ ≺ peano.succ t₂ ⇔ t₁ ≺ t₂

source

theorem FirstOrder.Language.Theory.Q.zero_lt_succ {n : ℕ} {t : peano.Term n} :

↑ᵀ^[n] Q ⊢ 0 ≺ peano.succ t

source

theorem FirstOrder.Language.Theory.Q.add_ofNat {n a b : ℕ} :

↑ᵀ^[n] Q ⊢ peano.ofNat a + peano.ofNat b ≐ peano.ofNat (a + b)

source

theorem FirstOrder.Language.Theory.Q.mul_ofNat {n a b : ℕ} :

↑ᵀ^[n] Q ⊢ peano.ofNat a * peano.ofNat b ≐ peano.ofNat (a * b)

source

theorem FirstOrder.Language.Theory.Q.add_assoc_ofNat {n : ℕ} {t₁ t₂ : peano.Term n} {a : ℕ} :

↑ᵀ^[n] Q ⊢ t₁ + t₂ + peano.ofNat a ≐ t₁ + (t₂ + peano.ofNat a)

source

theorem FirstOrder.Language.Theory.Q.add_ofNat_cancel {n : ℕ} {t₁ t₂ : peano.Term n} {a : ℕ} :

↑ᵀ^[n] Q ⊢ t₁ + peano.ofNat a ≐ t₂ + peano.ofNat a ⇒ t₁ ≐ t₂

source

theorem FirstOrder.Language.Theory.Q.ne_ofNat {n a b : ℕ} (h : a ≠ b) :

↑ᵀ^[n] Q ⊢ ~ peano.ofNat a ≐ peano.ofNat b

source

theorem FirstOrder.Language.Theory.Q.le_ofNat {n a b : ℕ} (h : a ≤ b) :

↑ᵀ^[n] Q ⊢ peano.ofNat a ⪯ peano.ofNat b

source

theorem FirstOrder.Language.Theory.Q.lt_ofNat {n a b : ℕ} (h : a < b) :

↑ᵀ^[n] Q ⊢ peano.ofNat a ≺ peano.ofNat b

source

theorem FirstOrder.Language.Theory.Q.not_le_ofNat {n a b : ℕ} (h : b < a) :

↑ᵀ^[n] Q ⊢ ~ peano.ofNat a ⪯ peano.ofNat b

source

theorem FirstOrder.Language.Theory.Q.not_lt_ofNat {n a b : ℕ} (h : b ≤ a) :

↑ᵀ^[n] Q ⊢ ~ peano.ofNat a ≺ peano.ofNat b

source

theorem FirstOrder.Language.Theory.Q.add_le_add_ofNat_iff {n : ℕ} {t₁ t₂ : peano.Term n} {a : ℕ} :

↑ᵀ^[n] Q ⊢ t₁ + peano.ofNat a ⪯ t₂ + peano.ofNat a ⇔ t₁ ⪯ t₂

source

theorem FirstOrder.Language.Theory.Q.add_lt_add_ofNat_iff {n : ℕ} {t₁ t₂ : peano.Term n} {a : ℕ} :

↑ᵀ^[n] Q ⊢ t₁ + peano.ofNat a ≺ t₂ + peano.ofNat a ⇔ t₁ ≺ t₂

source

theorem FirstOrder.Language.Theory.Q.eq_or_ge_ofNat {n : ℕ} (t : peano.Term n) (a : ℕ) :

↑ᵀ^[n] Q ⊢ (⋁ (i : Fin a), t ≐ peano.ofNat ↑i) ⩒ peano.ofNat a ⪯ t

source

theorem FirstOrder.Language.Theory.Q.lt_or_ge_ofNat {n : ℕ} (t : peano.Term n) (a : ℕ) :

↑ᵀ^[n] Q ⊢ t ≺ peano.ofNat a ⩒ peano.ofNat a ⪯ t

source

theorem FirstOrder.Language.Theory.Q.le_or_gt_ofNat {n : ℕ} (t : peano.Term n) (a : ℕ) :

↑ᵀ^[n] Q ⊢ t ⪯ peano.ofNat a ⩒ peano.ofNat a ≺ t

source

theorem FirstOrder.Language.Theory.Q.lt_ofNat_iff {n : ℕ} {t : peano.Term n} {a : ℕ} :

↑ᵀ^[n] Q ⊢ t ≺ peano.ofNat a ⇔ ⋁ (i : Fin a), t ≐ peano.ofNat ↑i

source

theorem FirstOrder.Language.Theory.Q.le_ofNat_iff {n : ℕ} {t : peano.Term n} {a : ℕ} :

↑ᵀ^[n] Q ⊢ t ⪯ peano.ofNat a ⇔ ⋁ (i : Fin (a + 1)), t ≐ peano.ofNat ↑i

source

theorem FirstOrder.Language.Theory.Q.not_lt_ofNat_iff {n : ℕ} {t : peano.Term n} {a : ℕ} :

↑ᵀ^[n] Q ⊢ ~ t ≺ peano.ofNat a ⇔ peano.ofNat a ⪯ t

source

theorem FirstOrder.Language.Theory.Q.not_le_ofNat_iff {n : ℕ} {t : peano.Term n} {a : ℕ} :

↑ᵀ^[n] Q ⊢ ~ t ⪯ peano.ofNat a ⇔ peano.ofNat a ≺ t

source

theorem FirstOrder.Language.Theory.Q.ne_ofNat_iff {n : ℕ} {t : peano.Term n} {a : ℕ} :

↑ᵀ^[n] Q ⊢ ~ t ≐ peano.ofNat a ⇔ t ≺ peano.ofNat a ⩒ peano.ofNat a ≺ t

source

theorem FirstOrder.Language.Theory.Q.not_ge_ofNat_iff {n : ℕ} {t : peano.Term n} {a : ℕ} :

↑ᵀ^[n] Q ⊢ ~ peano.ofNat a ⪯ t ⇔ t ≺ peano.ofNat a

source

theorem FirstOrder.Language.Theory.Q.not_gt_ofNat_iff {n : ℕ} {t : peano.Term n} {a : ℕ} :

↑ᵀ^[n] Q ⊢ ~ peano.ofNat a ≺ t ⇔ t ⪯ peano.ofNat a

source

theorem FirstOrder.Language.Theory.Q.bdall_ofNat_iff {n a : ℕ} {p : peano.Formula (n + 1)} :

↑ᵀ^[n] Q ⊢ ∀[≺ peano.ofNat a] p ⇔ ⋀ (i : Fin a), p[↦ₛ peano.ofNat ↑i]ₚ

source

theorem FirstOrder.Language.Theory.Q.bdex_ofNat_iff {n a : ℕ} {p : peano.Formula (n + 1)} :

↑ᵀ^[n] Q ⊢ ∃[≺ peano.ofNat a] p ⇔ ⋁ (i : Fin a), p[↦ₛ peano.ofNat ↑i]ₚ

source

inductive FirstOrder.Language.Theory.PA :

peano.Theory

Peano arithmetic.

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 {n : ℕ} {p : peano.Formula (n + 1)} : PA (∀* (p[↦ₛ 0]ₚ ⇒ ∀' (p ⇒ p[≔ₛ peano.succ #0]ₚ) ⇒ ∀' p))

Instances For

source

theorem FirstOrder.Language.Theory.PA.ind {n : ℕ} {p : peano.Formula (n + 1)} :

↑ᵀ^[n] PA ⊢ p[↦ₛ 0]ₚ ⇒ ∀' (p ⇒ p[≔ₛ peano.succ #0]ₚ) ⇒ ∀' p

source

theorem FirstOrder.Language.Theory.PA.zero_or_succ {n : ℕ} (t : peano.Term n) :

↑ᵀ^[n] PA ⊢ t ≐ 0 ⩒ ∃' (↑ₜt ≐ peano.succ #0)

source

instance FirstOrder.Language.Theory.PA.instSubtheoryQ :

Q ⊆ᵀ PA

source

instance FirstOrder.Language.Theory.PA.instSubtheoryQ_1 {T : peano.FormulaSet 0} [h : PA ⊆ᵀ T] :

Q ⊆ᵀ T

source

theorem FirstOrder.Language.Theory.PA.zero_add {n : ℕ} (t : peano.Term n) :

↑ᵀ^[n] PA ⊢ 0 + t ≐ t

source

theorem FirstOrder.Language.Theory.PA.succ_add {n : ℕ} (t₁ t₂ : peano.Term n) :

↑ᵀ^[n] PA ⊢ peano.succ t₁ + t₂ ≐ peano.succ (t₁ + t₂)

source

theorem FirstOrder.Language.Theory.PA.add_comm {n : ℕ} (t₁ t₂ : peano.Term n) :

↑ᵀ^[n] PA ⊢ t₁ + t₂ ≐ t₂ + t₁

source

theorem FirstOrder.Language.Theory.PA.one_add {n : ℕ} (t : peano.Term n) :

↑ᵀ^[n] PA ⊢ 1 + t ≐ peano.succ t

source

theorem FirstOrder.Language.Theory.PA.add_assoc {n : ℕ} (t₁ t₂ t₃ : peano.Term n) :

↑ᵀ^[n] PA ⊢ t₁ + t₂ + t₃ ≐ t₁ + (t₂ + t₃)

source

theorem FirstOrder.Language.Theory.PA.add_right_comm {n : ℕ} (t₁ t₂ t₃ : peano.Term n) :

↑ᵀ^[n] PA ⊢ t₁ + t₂ + t₃ ≐ t₁ + t₃ + t₂

source

theorem FirstOrder.Language.Theory.PA.add_right_cancel {n : ℕ} {t₁ t₂ : peano.Term n} (t : peano.Term n) :

↑ᵀ^[n] PA ⊢ t₁ + t ≐ t₂ + t ⇒ t₁ ≐ t₂

source

theorem FirstOrder.Language.Theory.PA.add_left_cancel {n : ℕ} {t₁ t₂ : peano.Term n} (t : peano.Term n) :

↑ᵀ^[n] PA ⊢ t + t₁ ≐ t + t₂ ⇒ t₁ ≐ t₂

source

theorem FirstOrder.Language.Theory.PA.zero_mul {n : ℕ} (t : peano.Term n) :

↑ᵀ^[n] PA ⊢ 0 * t ≐ 0

source

theorem FirstOrder.Language.Theory.PA.succ_mul {n : ℕ} (t₁ t₂ : peano.Term n) :

↑ᵀ^[n] PA ⊢ peano.succ t₁ * t₂ ≐ t₁ * t₂ + t₂

source

theorem FirstOrder.Language.Theory.PA.mul_comm {n : ℕ} (t₁ t₂ : peano.Term n) :

↑ᵀ^[n] PA ⊢ t₁ * t₂ ≐ t₂ * t₁

source

theorem FirstOrder.Language.Theory.PA.right_distrib {n : ℕ} (t₁ t₂ t₃ : peano.Term n) :

↑ᵀ^[n] PA ⊢ (t₁ + t₂) * t₃ ≐ t₁ * t₃ + t₂ * t₃

source

theorem FirstOrder.Language.Theory.PA.left_distrib {n : ℕ} (t₁ t₂ t₃ : peano.Term n) :

↑ᵀ^[n] PA ⊢ t₁ * (t₂ + t₃) ≐ t₁ * t₂ + t₁ * t₃

source

theorem FirstOrder.Language.Theory.PA.mul_assoc {n : ℕ} (t₁ t₂ t₃ : peano.Term n) :

↑ᵀ^[n] PA ⊢ t₁ * t₂ * t₃ ≐ t₁ * (t₂ * t₃)

source

theorem FirstOrder.Language.Theory.PA.mul_right_comm {n : ℕ} {t₁ t₂ t₃ : peano.Term n} :

↑ᵀ^[n] PA ⊢ t₁ * t₂ * t₃ ≐ t₁ * t₃ * t₂

source

theorem FirstOrder.Language.Theory.PA.mul_one {n : ℕ} (t : peano.Term n) :

↑ᵀ^[n] PA ⊢ t * 1 ≐ t

source

theorem FirstOrder.Language.Theory.PA.one_mul {n : ℕ} (t : peano.Term n) :

↑ᵀ^[n] PA ⊢ 1 * t ≐ t

source

theorem FirstOrder.Language.Theory.PA.mul_eq_zero_iff {n : ℕ} {t₁ t₂ : peano.Term n} :

↑ᵀ^[n] PA ⊢ t₁ * t₂ ≐ 0 ⇔ t₁ ≐ 0 ⩒ t₂ ≐ 0

source

theorem FirstOrder.Language.Theory.PA.mul_eq_one_iff {n : ℕ} {t₁ t₂ : peano.Term n} :

↑ᵀ^[n] PA ⊢ t₁ * t₂ ≐ 1 ⇔ t₁ ≐ 1 ⩑ t₂ ≐ 1

source

theorem FirstOrder.Language.Theory.PA.le_refl {n : ℕ} {t : peano.Term n} :

↑ᵀ^[n] PA ⊢ t ⪯ t

source

theorem FirstOrder.Language.Theory.PA.le_antisymm {n : ℕ} {t₁ t₂ : peano.Term n} :

↑ᵀ^[n] PA ⊢ t₁ ⪯ t₂ ⇒ t₂ ⪯ t₁ ⇒ t₁ ≐ t₂

source

theorem FirstOrder.Language.Theory.PA.le_trans {n : ℕ} {t₁ t₂ t₃ : peano.Term n} :

↑ᵀ^[n] PA ⊢ t₁ ⪯ t₂ ⇒ t₂ ⪯ t₃ ⇒ t₁ ⪯ t₃

source

theorem FirstOrder.Language.Theory.PA.lt_iff_le_not_ge {n : ℕ} {t₁ t₂ : peano.Term n} :

↑ᵀ^[n] PA ⊢ t₁ ≺ t₂ ⇔ t₁ ⪯ t₂ ⩑ ~ t₂ ⪯ t₁

source

theorem FirstOrder.Language.Theory.PA.lt_succ_self {n : ℕ} {t : peano.Term n} :

↑ᵀ^[n] PA ⊢ t ≺ peano.succ t

source

theorem FirstOrder.Language.Theory.PA.le_succ_self {n : ℕ} {t : peano.Term n} :

↑ᵀ^[n] PA ⊢ t ⪯ peano.succ t

source

theorem FirstOrder.Language.Theory.PA.le_total {n : ℕ} {t₁ t₂ : peano.Term n} :

↑ᵀ^[n] PA ⊢ t₁ ⪯ t₂ ⩒ t₂ ⪯ t₁

source

instance FirstOrder.Language.Theory.PA.instSubtheoryLO :

LO ⊆ᵀ PA

source

theorem FirstOrder.Language.Theory.PA.le_succ_of_le {n : ℕ} {t₁ t₂ : peano.Term n} :

↑ᵀ^[n] PA ⊢ t₁ ⪯ t₂ ⇒ t₁ ⪯ peano.succ t₂

source

theorem FirstOrder.Language.Theory.PA.lt_succ_of_lt {n : ℕ} {t₁ t₂ : peano.Term n} :

↑ᵀ^[n] PA ⊢ t₁ ≺ t₂ ⇒ t₁ ≺ peano.succ t₂

source

theorem FirstOrder.Language.Theory.PA.lt_succ_iff_lt_or_eq {n : ℕ} {t₁ t₂ : peano.Term n} :

↑ᵀ^[n] PA ⊢ t₁ ≺ peano.succ t₂ ⇔ t₁ ≺ t₂ ⩒ t₁ ≐ t₂

source

theorem FirstOrder.Language.Theory.PA.succ_not_le_self {n : ℕ} {t : peano.Term n} :

↑ᵀ^[n] PA ⊢ ~ peano.succ t ⪯ t

source

theorem FirstOrder.Language.Theory.PA.succ_ne_self {n : ℕ} {t : peano.Term n} :

↑ᵀ^[n] PA ⊢ ~ peano.succ t ≐ t

source

theorem FirstOrder.Language.Theory.PA.pos_of_lt {n : ℕ} {t₁ t₂ : peano.Term n} :

↑ᵀ^[n] PA ⊢ t₁ ≺ t₂ ⇒ 0 ≺ t₂

source

theorem FirstOrder.Language.Theory.PA.zero_or_pos {n : ℕ} (t : peano.Term n) :

↑ᵀ^[n] PA ⊢ t ≐ 0 ⩒ 0 ≺ t

source

theorem FirstOrder.Language.Theory.PA.add_le_add {n : ℕ} {t₁ t₂ t₃ t₄ : peano.Term n} :

↑ᵀ^[n] PA ⊢ t₁ ⪯ t₂ ⇒ t₃ ⪯ t₄ ⇒ t₁ + t₃ ⪯ t₂ + t₄

source

theorem FirstOrder.Language.Theory.PA.add_le_add_iff_left {n : ℕ} {t t₁ t₂ : peano.Term n} :

↑ᵀ^[n] PA ⊢ t + t₁ ⪯ t + t₂ ⇔ t₁ ⪯ t₂

source

theorem FirstOrder.Language.Theory.PA.add_le_add_iff_right {n : ℕ} {t t₁ t₂ : peano.Term n} :

↑ᵀ^[n] PA ⊢ t₁ + t ⪯ t₂ + t ⇔ t₁ ⪯ t₂

source

theorem FirstOrder.Language.Theory.PA.le_add_of_le_left {n : ℕ} {t t₁ t₂ : peano.Term n} :

↑ᵀ^[n] PA ⊢ t₁ ⪯ t₂ ⇒ t₁ ⪯ t + t₂

source

theorem FirstOrder.Language.Theory.PA.le_add_of_le_right {n : ℕ} {t t₁ t₂ : peano.Term n} :

↑ᵀ^[n] PA ⊢ t₁ ⪯ t₂ ⇒ t₁ ⪯ t₂ + t

source

theorem FirstOrder.Language.Theory.PA.le_add_left {n : ℕ} {t₁ t₂ : peano.Term n} :

↑ᵀ^[n] PA ⊢ t₁ ⪯ t₂ + t₁

source

theorem FirstOrder.Language.Theory.PA.le_add_right {n : ℕ} {t₁ t₂ : peano.Term n} :

↑ᵀ^[n] PA ⊢ t₁ ⪯ t₁ + t₂

source

theorem FirstOrder.Language.Theory.PA.add_lt_add_of_le_of_lt {n : ℕ} {t₁ t₂ t₃ t₄ : peano.Term n} :

↑ᵀ^[n] PA ⊢ t₁ ⪯ t₂ ⇒ t₃ ≺ t₄ ⇒ t₁ + t₃ ≺ t₂ + t₄

source

theorem FirstOrder.Language.Theory.PA.add_lt_add_of_lt_of_le {n : ℕ} {t₁ t₂ t₃ t₄ : peano.Term n} :

↑ᵀ^[n] PA ⊢ t₁ ≺ t₂ ⇒ t₃ ⪯ t₄ ⇒ t₁ + t₃ ≺ t₂ + t₄

source

theorem FirstOrder.Language.Theory.PA.add_lt_add_iff_left {n : ℕ} {t t₁ t₂ : peano.Term n} :

↑ᵀ^[n] PA ⊢ t + t₁ ≺ t + t₂ ⇔ t₁ ≺ t₂

source

theorem FirstOrder.Language.Theory.PA.add_lt_add_iff_right {n : ℕ} {t t₁ t₂ : peano.Term n} :

↑ᵀ^[n] PA ⊢ t₁ + t ≺ t₂ + t ⇔ t₁ ≺ t₂

source

theorem FirstOrder.Language.Theory.PA.lt_add_of_lt_left {n : ℕ} {t t₁ t₂ : peano.Term n} :

↑ᵀ^[n] PA ⊢ t₁ ≺ t₂ ⇒ t₁ ≺ t + t₂

source

theorem FirstOrder.Language.Theory.PA.lt_add_of_lt_right {n : ℕ} {t t₁ t₂ : peano.Term n} :

↑ᵀ^[n] PA ⊢ t₁ ≺ t₂ ⇒ t₁ ≺ t₂ + t

source

theorem FirstOrder.Language.Theory.PA.lt_add_of_pos_left {n : ℕ} {t t₁ : peano.Term n} :

↑ᵀ^[n] PA ⊢ 0 ≺ t ⇒ t₁ ≺ t + t₁

source

theorem FirstOrder.Language.Theory.PA.lt_add_of_pos_right {n : ℕ} {t t₁ : peano.Term n} :

↑ᵀ^[n] PA ⊢ 0 ≺ t ⇒ t₁ ≺ t₁ + t

source

theorem FirstOrder.Language.Theory.PA.mul_le_mul {n : ℕ} {t₁ t₂ t₃ t₄ : peano.Term n} :

↑ᵀ^[n] PA ⊢ t₁ ⪯ t₂ ⇒ t₃ ⪯ t₄ ⇒ t₁ * t₃ ⪯ t₂ * t₄

source

theorem FirstOrder.Language.Theory.PA.mul_le_mul_left {n : ℕ} {t t₁ t₂ : peano.Term n} :

↑ᵀ^[n] PA ⊢ t₁ ⪯ t₂ ⇒ t * t₁ ⪯ t * t₂

source

theorem FirstOrder.Language.Theory.PA.mul_le_mul_right {n : ℕ} {t t₁ t₂ : peano.Term n} :

↑ᵀ^[n] PA ⊢ t₁ ⪯ t₂ ⇒ t₁ * t ⪯ t₂ * t

source

theorem FirstOrder.Language.Theory.PA.le_mul_of_le_left {n : ℕ} {t t₁ t₂ : peano.Term n} :

↑ᵀ^[n] PA ⊢ 0 ≺ t ⇒ t₁ ⪯ t₂ ⇒ t₁ ⪯ t * t₂

source

theorem FirstOrder.Language.Theory.PA.le_mul_of_le_right {n : ℕ} {t t₁ t₂ : peano.Term n} :

↑ᵀ^[n] PA ⊢ 0 ≺ t ⇒ t₁ ⪯ t₂ ⇒ t₁ ⪯ t₂ * t

source

theorem FirstOrder.Language.Theory.PA.le_mul_left {n : ℕ} {t₁ t₂ : peano.Term n} :

↑ᵀ^[n] PA ⊢ 0 ≺ t₂ ⇒ t₁ ⪯ t₂ * t₁

source

theorem FirstOrder.Language.Theory.PA.le_mul_right {n : ℕ} {t₁ t₂ : peano.Term n} :

↑ᵀ^[n] PA ⊢ 0 ≺ t₂ ⇒ t₁ ⪯ t₁ * t₂

source

theorem FirstOrder.Language.Theory.PA.mul_lt_mul_left {n : ℕ} {t t₁ t₂ : peano.Term n} :

↑ᵀ^[n] PA ⊢ 0 ≺ t ⇒ t₁ ≺ t₂ ⇒ t * t₁ ≺ t * t₂

source

theorem FirstOrder.Language.Theory.PA.mul_lt_mul_right {n : ℕ} {t t₁ t₂ : peano.Term n} :

↑ᵀ^[n] PA ⊢ 0 ≺ t ⇒ t₁ ≺ t₂ ⇒ t₁ * t ≺ t₂ * t

source

theorem FirstOrder.Language.Theory.PA.lt_mul_left {n : ℕ} {t₁ t₂ : peano.Term n} :

↑ᵀ^[n] PA ⊢ 0 ≺ t₁ ⇒ 1 ≺ t₂ ⇒ t₁ ≺ t₂ * t₁

source

theorem FirstOrder.Language.Theory.PA.lt_mul_right {n : ℕ} {t₁ t₂ : peano.Term n} :

↑ᵀ^[n] PA ⊢ 0 ≺ t₁ ⇒ 1 ≺ t₂ ⇒ t₁ ≺ t₁ * t₂

source

theorem FirstOrder.Language.Theory.PA.mul_le_mul_iff_left {n : ℕ} {t t₁ t₂ : peano.Term n} :

↑ᵀ^[n] PA ⊢ 0 ≺ t ⇒ t * t₁ ⪯ t * t₂ ⇔ t₁ ⪯ t₂

source

theorem FirstOrder.Language.Theory.PA.mul_le_mul_iff_right {n : ℕ} {t t₁ t₂ : peano.Term n} :

↑ᵀ^[n] PA ⊢ 0 ≺ t ⇒ t₁ * t ⪯ t₂ * t ⇔ t₁ ⪯ t₂

source

theorem FirstOrder.Language.Theory.PA.mul_pos_iff {n : ℕ} {t₁ t₂ : peano.Term n} :

↑ᵀ^[n] PA ⊢ 0 ≺ t₁ * t₂ ⇔ 0 ≺ t₁ ⩑ 0 ≺ t₂

source

theorem FirstOrder.Language.Theory.PA.strong_ind {n : ℕ} {p : peano.Formula (n + 1)} :

↑ᵀ^[n] PA ⊢ ∀' (∀[≺ #0] p[#0 ∷ᵥ Subst.shift 2]ₚ ⇒ p) ⇒ ∀' p

Strong induction principle formalized in PA.

source

theorem FirstOrder.Language.Theory.PA.exists_min {n : ℕ} {p : peano.Formula (n + 1)} :

↑ᵀ^[n] PA ⊢ ∃' p ⇒ ∃' (p ⩑ ∀[≺ #0] (~ p[#0 ∷ᵥ Subst.shift 2]ₚ))

Least number principle formalized in PA.

Documentation

MathematicalLogic.FirstOrder.Theories.Peano.Theory

Theory of first-order arithmetic #