Documentation

LeanPool.Incompleteness.Arith.FormalizedArithmetic

Formalized Theory $\mathsf{R_0}$ #

@[implicit_reducible]

noncomputable def LO.Arith.instDecidableEqOfClassical (α : Sort u_2) :

Local classical decidable equality instance used by imported proofs.

Equations

LO.Arith.instDecidableEqOfClassical α = Classical.decEq α

Instances For

@[reducible, inline]

abbrev LO.Arith.Formalized.LOR.Theory (V : Type u_1) [ORingStruc V] :

Type u_1

Imported declaration from the Incompleteness formalization.

Equations

LO.Arith.Formalized.LOR.Theory V = ⌜ℒₒᵣ⌝.Theory

Instances For

@[simp]

theorem LO.Arith.Formalized.two_lt_three {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] :

2 < 1 + 1 + 1

TODO: move

@[simp]

theorem LO.Arith.Formalized.two_lt_four {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] :

2 < 1 + 1 + 1 + 1

@[simp]

theorem LO.Arith.Formalized.three_lt_four {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] :

3 < 1 + 1 + 1 + 1

@[simp]

theorem LO.Arith.Formalized.two_sub_one_eq_one {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] :

2 - 1 = 1

@[simp]

theorem LO.Arith.Formalized.three_sub_one_eq_two {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] :

3 - 1 = 2

class LO.Arith.Formalized.R₀Theory {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (T : ⌜ℒₒᵣ⌝.TTheory) :

Type u_1

Imported declaration from the Incompleteness formalization.

refl : T ⊢ ((bv 0 ⋯).equals (bv 0 ⋯)).all
Imported declaration from the Incompleteness formalization.
replace (φ : ⌜ℒₒᵣ⌝.Semiformula (0 + 1)) : T ⊢ ((bv 1 ⋯).equals (bv 0 ⋯) ==> φ^/[(bv 1 ⋯).sing] ==> φ^/[(bv 0 ⋯).sing]).all.all
Imported declaration from the Incompleteness formalization.
add (n m : V) : T ⊢ (typedNumeral 0 n + typedNumeral 0 m).equals (typedNumeral 0 (n + m))
Imported declaration from the Incompleteness formalization.
mul (n m : V) : T ⊢ (typedNumeral 0 n * typedNumeral 0 m).equals (typedNumeral 0 (n * m))
Imported declaration from the Incompleteness formalization.
ne {n m : V} : n ≠ m → T ⊢ (typedNumeral 0 n).notEquals (typedNumeral 0 m)
Imported declaration from the Incompleteness formalization.
ltNumeral (n : V) : T ⊢ ((bv 0 ⋯).lessThan (typedNumeral (0 + 1) n) <=> (tSubstItr (bv 0 ⋯).sing ((bv 1 ⋯).equals (bv 0 ⋯)) n).disj).all
Imported declaration from the Incompleteness formalization.

Instances

@[reducible, inline]

noncomputable abbrev LO.Arith.Formalized.oneAbbrev {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {n : V} :

⌜ℒₒᵣ⌝.Semiterm n

Imported declaration from the Incompleteness formalization.

Equations

LO.Arith.Formalized.oneAbbrev = LO.Arith.Formalized.typedNumeral n 1

Instances For

def LO.Arith.Formalized.«term^1» :

Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

LO.Arith.Formalized.«term^1» = Lean.ParserDescr.node `LO.Arith.Formalized.«term^1» 1024 (Lean.ParserDescr.symbol "^1")

Instances For

noncomputable def LO.Arith.Formalized.TProof.eqRefl {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (t : ⌜ℒₒᵣ⌝.Term) :

T ⊢ Language.Semiterm.equals t t

Imported declaration from the Incompleteness formalization.

Equations

LO.Arith.Formalized.TProof.eqRefl T t = ⋯.mp (LO.Arith.Language.Theory.TProof.specialize LO.Arith.Formalized.R₀Theory.refl t)

Instances For

theorem LO.Arith.Formalized.TProof.eq_refl! {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (t : ⌜ℒₒᵣ⌝.Term) :

T ⊢! Language.Semiterm.equals t t

noncomputable def LO.Arith.Formalized.TProof.replace {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (φ : ⌜ℒₒᵣ⌝.Semiformula (0 + 1)) (t u : ⌜ℒₒᵣ⌝.Term) :

T ⊢ Language.Semiterm.equals t u ==> φ^/[Language.Semiterm.sing t] ==> φ^/[Language.Semiterm.sing u]

Imported declaration from the Incompleteness formalization.

Equations

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

Instances For

theorem LO.Arith.Formalized.TProof.replace! {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (φ : ⌜ℒₒᵣ⌝.Semiformula (0 + 1)) (t u : ⌜ℒₒᵣ⌝.Term) :

T ⊢! Language.Semiterm.equals t u ==> φ^/[Language.Semiterm.sing t] ==> φ^/[Language.Semiterm.sing u]

noncomputable def LO.Arith.Formalized.TProof.eqSymm {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (t₁ t₂ : ⌜ℒₒᵣ⌝.Term) :

T ⊢ Language.Semiterm.equals t₁ t₂ ==> Language.Semiterm.equals t₂ t₁

Imported declaration from the Incompleteness formalization.

Equations

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

Instances For

theorem LO.Arith.Formalized.TProof.eq_symm! {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (t₁ t₂ : ⌜ℒₒᵣ⌝.Term) :

T ⊢! Language.Semiterm.equals t₁ t₂ ==> Language.Semiterm.equals t₂ t₁

theorem LO.Arith.Formalized.TProof.eq_symm'! {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] {t₁ t₂ : ⌜ℒₒᵣ⌝.Term} (h : T ⊢! Language.Semiterm.equals t₁ t₂) :

T ⊢! Language.Semiterm.equals t₂ t₁

noncomputable def LO.Arith.Formalized.TProof.eqTrans {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (t₁ t₂ t₃ : ⌜ℒₒᵣ⌝.Term) :

T ⊢ Language.Semiterm.equals t₁ t₂ ==> Language.Semiterm.equals t₂ t₃ ==> Language.Semiterm.equals t₁ t₃

Imported declaration from the Incompleteness formalization.

Equations

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

Instances For

theorem LO.Arith.Formalized.TProof.eq_trans! {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (t₁ t₂ t₃ : ⌜ℒₒᵣ⌝.Term) :

T ⊢! Language.Semiterm.equals t₁ t₂ ==> Language.Semiterm.equals t₂ t₃ ==> Language.Semiterm.equals t₁ t₃

noncomputable def LO.Arith.Formalized.TProof.addExt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) :

T ⊢ Language.Semiterm.equals t₁ t₂ ==> Language.Semiterm.equals u₁ u₂ ==> Language.Semiterm.equals (t₁ + u₁) (t₂ + u₂)

Imported declaration from the Incompleteness formalization.

Equations

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

Instances For

theorem LO.Arith.Formalized.TProof.add_ext! {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) :

T ⊢! Language.Semiterm.equals t₁ t₂ ==> Language.Semiterm.equals u₁ u₂ ==> Language.Semiterm.equals (t₁ + u₁) (t₂ + u₂)

noncomputable def LO.Arith.Formalized.TProof.mulExt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) :

T ⊢ Language.Semiterm.equals t₁ t₂ ==> Language.Semiterm.equals u₁ u₂ ==> Language.Semiterm.equals (t₁ * u₁) (t₂ * u₂)

Imported declaration from the Incompleteness formalization.

Equations

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

Instances For

theorem LO.Arith.Formalized.TProof.mul_ext! {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) :

T ⊢! Language.Semiterm.equals t₁ t₂ ==> Language.Semiterm.equals u₁ u₂ ==> Language.Semiterm.equals (t₁ * u₁) (t₂ * u₂)

noncomputable def LO.Arith.Formalized.TProof.eqExt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) :

T ⊢ Language.Semiterm.equals t₁ t₂ ==> Language.Semiterm.equals u₁ u₂ ==> Language.Semiterm.equals t₁ u₁ ==> Language.Semiterm.equals t₂ u₂

Imported declaration from the Incompleteness formalization.

Equations

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

Instances For

theorem LO.Arith.Formalized.TProof.eq_ext {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) :

T ⊢! Language.Semiterm.equals t₁ t₂ ==> Language.Semiterm.equals u₁ u₂ ==> Language.Semiterm.equals t₁ u₁ ==> Language.Semiterm.equals t₂ u₂

noncomputable def LO.Arith.Formalized.TProof.neExt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) :

T ⊢ Language.Semiterm.equals t₁ t₂ ==> Language.Semiterm.equals u₁ u₂ ==> Language.Semiterm.notEquals t₁ u₁ ==> Language.Semiterm.notEquals t₂ u₂

Imported declaration from the Incompleteness formalization.

Equations

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

Instances For

theorem LO.Arith.Formalized.TProof.ne_ext {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) :

T ⊢! Language.Semiterm.equals t₁ t₂ ==> Language.Semiterm.equals u₁ u₂ ==> Language.Semiterm.notEquals t₁ u₁ ==> Language.Semiterm.notEquals t₂ u₂

noncomputable def LO.Arith.Formalized.TProof.ltExt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) :

T ⊢ Language.Semiterm.equals t₁ t₂ ==> Language.Semiterm.equals u₁ u₂ ==> Language.Semiterm.lessThan t₁ u₁ ==> Language.Semiterm.lessThan t₂ u₂

Imported declaration from the Incompleteness formalization.

Equations

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

Instances For

theorem LO.Arith.Formalized.TProof.lt_ext! {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) :

T ⊢! Language.Semiterm.equals t₁ t₂ ==> Language.Semiterm.equals u₁ u₂ ==> Language.Semiterm.lessThan t₁ u₁ ==> Language.Semiterm.lessThan t₂ u₂

noncomputable def LO.Arith.Formalized.TProof.nltExt {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) :

T ⊢ Language.Semiterm.equals t₁ t₂ ==> Language.Semiterm.equals u₁ u₂ ==> Language.Semiterm.notLessThan t₁ u₁ ==> Language.Semiterm.notLessThan t₂ u₂

Imported declaration from the Incompleteness formalization.

Equations

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

Instances For

theorem LO.Arith.Formalized.TProof.nlt_ext {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Term) :

T ⊢! Language.Semiterm.equals t₁ t₂ ==> Language.Semiterm.equals u₁ u₂ ==> Language.Semiterm.notLessThan t₁ u₁ ==> Language.Semiterm.notLessThan t₂ u₂

noncomputable def LO.Arith.Formalized.TProof.ballReplace {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (φ : ⌜ℒₒᵣ⌝.Semiformula (0 + 1)) (t u : ⌜ℒₒᵣ⌝.Term) :

T ⊢ Language.Semiterm.equals t u ==> Language.Semiformula.ball t φ ==> Language.Semiformula.ball u φ

Imported declaration from the Incompleteness formalization.

Equations

LO.Arith.Formalized.TProof.ballReplace T φ t u = ⋯.mp (LO.Arith.Formalized.TProof.replace T (LO.Arith.Language.Semiformula.ball (LO.Arith.bv 0 ⋯) (φ^/[(LO.Arith.bv 0 ⋯).sing])) t u)

Instances For

theorem LO.Arith.Formalized.TProof.ball_replace! {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (φ : ⌜ℒₒᵣ⌝.Semiformula (0 + 1)) (t u : ⌜ℒₒᵣ⌝.Term) :

T ⊢! Language.Semiterm.equals t u ==> Language.Semiformula.ball t φ ==> Language.Semiformula.ball u φ

noncomputable def LO.Arith.Formalized.TProof.bexReplace {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (φ : ⌜ℒₒᵣ⌝.Semiformula (0 + 1)) (t u : ⌜ℒₒᵣ⌝.Term) :

T ⊢ Language.Semiterm.equals t u ==> Language.Semiformula.bex t φ ==> Language.Semiformula.bex u φ

Imported declaration from the Incompleteness formalization.

Equations

LO.Arith.Formalized.TProof.bexReplace T φ t u = ⋯.mp (LO.Arith.Formalized.TProof.replace T (LO.Arith.Language.Semiformula.bex (LO.Arith.bv 0 ⋯) (φ^/[(LO.Arith.bv 0 ⋯).sing])) t u)

Instances For

theorem LO.Arith.Formalized.TProof.bex_replace! {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (φ : ⌜ℒₒᵣ⌝.Semiformula (0 + 1)) (t u : ⌜ℒₒᵣ⌝.Term) :

T ⊢! Language.Semiterm.equals t u ==> Language.Semiformula.bex t φ ==> Language.Semiformula.bex u φ

noncomputable def LO.Arith.Formalized.TProof.eqComplete {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] {n m : V} (h : n = m) :

T ⊢ (typedNumeral 0 n).equals (typedNumeral 0 m)

Imported declaration from the Incompleteness formalization.

Equations

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

Instances For

theorem LO.Arith.Formalized.TProof.eq_complete! {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] {n m : V} (h : n = m) :

T ⊢! (typedNumeral 0 n).equals (typedNumeral 0 m)

def LO.Arith.Formalized.TProof.addComplete {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (n m : V) :

T ⊢ (typedNumeral 0 n + typedNumeral 0 m).equals (typedNumeral 0 (n + m))

Imported declaration from the Incompleteness formalization.

Equations

LO.Arith.Formalized.TProof.addComplete T n m = LO.Arith.Formalized.R₀Theory.add n m

Instances For

theorem LO.Arith.Formalized.TProof.add_complete! {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (n m : V) :

T ⊢! (typedNumeral 0 n + typedNumeral 0 m).equals (typedNumeral 0 (n + m))

def LO.Arith.Formalized.TProof.mulComplete {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (n m : V) :

T ⊢ (typedNumeral 0 n * typedNumeral 0 m).equals (typedNumeral 0 (n * m))

Imported declaration from the Incompleteness formalization.

Equations

LO.Arith.Formalized.TProof.mulComplete T n m = LO.Arith.Formalized.R₀Theory.mul n m

Instances For

theorem LO.Arith.Formalized.TProof.mul_complete! {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (n m : V) :

T ⊢! (typedNumeral 0 n * typedNumeral 0 m).equals (typedNumeral 0 (n * m))

def LO.Arith.Formalized.TProof.neComplete {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] {n m : V} (h : n ≠ m) :

T ⊢ (typedNumeral 0 n).notEquals (typedNumeral 0 m)

Imported declaration from the Incompleteness formalization.

Equations

LO.Arith.Formalized.TProof.neComplete T h = LO.Arith.Formalized.R₀Theory.ne h

Instances For

theorem LO.Arith.Formalized.TProof.ne_complete! {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] {n m : V} (h : n ≠ m) :

T ⊢! (typedNumeral 0 n).notEquals (typedNumeral 0 m)

noncomputable def LO.Arith.Formalized.TProof.ltNumeral {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (t : ⌜ℒₒᵣ⌝.Term) (n : V) :

T ⊢ Language.Semiterm.lessThan t (typedNumeral 0 n) <=> (tSubstItr (Language.Semiterm.sing t) ((bv 1 ⋯).equals (bv 0 ⋯)) n).disj

Imported declaration from the Incompleteness formalization.

Equations

LO.Arith.Formalized.TProof.ltNumeral T t n = ⋯.mp (LO.Arith.Language.Theory.TProof.specialize (LO.Arith.Formalized.R₀Theory.ltNumeral n) t)

Instances For

noncomputable def LO.Arith.Formalized.TProof.nltNumeral {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (t : ⌜ℒₒᵣ⌝.Term) (n : V) :

T ⊢ Language.Semiterm.notLessThan t (typedNumeral 0 n) <=> (tSubstItr (Language.Semiterm.sing t) ((bv 1 ⋯).notEquals (bv 0 ⋯)) n).conj

Imported declaration from the Incompleteness formalization.

Equations

LO.Arith.Formalized.TProof.nltNumeral T t n = ⋯.mp (LO.Entailment.negReplaceIff' (LO.Arith.Formalized.TProof.ltNumeral T t n))

Instances For

noncomputable def LO.Arith.Formalized.TProof.ltComplete {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] {n m : V} (h : n < m) :

T ⊢ (typedNumeral 0 n).lessThan (typedNumeral 0 m)

Imported declaration from the Incompleteness formalization.

Equations

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

Instances For

theorem LO.Arith.Formalized.TProof.lt_complete! {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] {n m : V} (h : n < m) :

T ⊢! (typedNumeral 0 n).lessThan (typedNumeral 0 m)

noncomputable def LO.Arith.Formalized.TProof.nltComplete {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] {n m : V} (h : m ≤ n) :

T ⊢ (typedNumeral 0 n).notLessThan (typedNumeral 0 m)

Imported declaration from the Incompleteness formalization.

Equations

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

Instances For

theorem LO.Arith.Formalized.TProof.nlt_complete {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] {n m : V} (h : m ≤ n) :

T ⊢! (typedNumeral 0 n).notLessThan (typedNumeral 0 m)

noncomputable def LO.Arith.Formalized.TProof.ballIntro {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (φ : ⌜ℒₒᵣ⌝.Semiformula (0 + 1)) (n : V) (bs : (i : V) → i < n → T ⊢ φ^/[(typedNumeral 0 i).sing]) :

T ⊢ Language.Semiformula.ball (typedNumeral 0 n) φ

Imported declaration from the Incompleteness formalization.

Equations

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

Instances For

theorem LO.Arith.Formalized.TProof.ball_intro! {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (φ : ⌜ℒₒᵣ⌝.Semiformula (0 + 1)) (n : V) (bs : ∀ i < n, T ⊢! φ^/[(typedNumeral 0 i).sing]) :

T ⊢! Language.Semiformula.ball (typedNumeral 0 n) φ

noncomputable def LO.Arith.Formalized.TProof.bexIntro {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (φ : ⌜ℒₒᵣ⌝.Semiformula (0 + 1)) (n : V) {i : V} (hi : i < n) (b : T ⊢ φ^/[(typedNumeral 0 i).sing]) :

T ⊢ Language.Semiformula.bex (typedNumeral 0 n) φ

Imported declaration from the Incompleteness formalization.

Equations

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

Instances For

theorem LO.Arith.Formalized.TProof.bex_intro! {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (T : ⌜ℒₒᵣ⌝.TTheory) [R₀Theory T] (φ : ⌜ℒₒᵣ⌝.Semiformula (0 + 1)) (n : V) {i : V} (hi : i < n) (b : T ⊢! φ^/[(typedNumeral 0 i).sing]) :

T ⊢! Language.Semiformula.bex (typedNumeral 0 n) φ