Documentation

Foundation.FirstOrder.Arith.Model

@[simp]

theorem LO.FirstOrder.Arith.oringEmb_operator_zero_val {L : LO.FirstOrder.Language} [L.ORing] :

LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb op(0).term = op(0).term

@[simp]

theorem LO.FirstOrder.Arith.oringEmb_operator_one_val {L : LO.FirstOrder.Language} [L.ORing] :

LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb op(1).term = op(1).term

@[simp]

theorem LO.FirstOrder.Arith.oringEmb_operator_add_val {L : LO.FirstOrder.Language} [L.ORing] :

LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb op(+).term = op(+).term

@[simp]

theorem LO.FirstOrder.Arith.oringEmb_operator_mul_val {L : LO.FirstOrder.Language} [L.ORing] :

LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb op(*).term = op(*).term

@[simp]

theorem LO.FirstOrder.Arith.oringEmb_operator_eq_val {L : LO.FirstOrder.Language} [L.ORing] :

(LO.FirstOrder.Semiformula.lMap LO.FirstOrder.Language.oringEmb) op(=).sentence = op(=).sentence

@[simp]

theorem LO.FirstOrder.Arith.oringEmb_operator_lt_val {L : LO.FirstOrder.Language} [L.ORing] :

(LO.FirstOrder.Semiformula.lMap LO.FirstOrder.Language.oringEmb) op(<).sentence = op(<).sentence

instance LO.FirstOrder.Arith.standardModel (M : Type u_1) [LO.ORingStruc M] :

LO.FirstOrder.Structure ℒₒᵣ M

Equations

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

instance LO.FirstOrder.Arith.instEqORing (M : Type u_1) [LO.ORingStruc M] :

LO.FirstOrder.Structure.Eq ℒₒᵣ M

Equations

⋯ = ⋯

instance LO.FirstOrder.Arith.instZeroORing (M : Type u_1) [LO.ORingStruc M] :

LO.FirstOrder.Structure.Zero ℒₒᵣ M

Equations

⋯ = ⋯

instance LO.FirstOrder.Arith.instOneORing (M : Type u_1) [LO.ORingStruc M] :

LO.FirstOrder.Structure.One ℒₒᵣ M

Equations

⋯ = ⋯

instance LO.FirstOrder.Arith.instAddORing (M : Type u_1) [LO.ORingStruc M] :

LO.FirstOrder.Structure.Add ℒₒᵣ M

Equations

⋯ = ⋯

instance LO.FirstOrder.Arith.instMulORing (M : Type u_1) [LO.ORingStruc M] :

LO.FirstOrder.Structure.Mul ℒₒᵣ M

Equations

⋯ = ⋯

instance LO.FirstOrder.Arith.instEqORing_1 (M : Type u_1) [LO.ORingStruc M] :

LO.FirstOrder.Structure.Eq ℒₒᵣ M

Equations

⋯ = ⋯

instance LO.FirstOrder.Arith.instLTORing (M : Type u_1) [LO.ORingStruc M] :

LO.FirstOrder.Structure.LT ℒₒᵣ M

Equations

⋯ = ⋯

instance LO.FirstOrder.Arith.instORingORing :

ℒₒᵣ.ORing

Equations

LO.FirstOrder.Arith.instORingORing = LO.FirstOrder.Language.ORing.mk

theorem LO.FirstOrder.Arith.standardModel_unique' (M : Type u_1) [LO.ORingStruc M] (s : LO.FirstOrder.Structure ℒₒᵣ M) (hZero : LO.FirstOrder.Structure.Zero ℒₒᵣ M) (hOne : LO.FirstOrder.Structure.One ℒₒᵣ M) (hAdd : LO.FirstOrder.Structure.Add ℒₒᵣ M) (hMul : LO.FirstOrder.Structure.Mul ℒₒᵣ M) (hEq : LO.FirstOrder.Structure.Eq ℒₒᵣ M) (hLT : LO.FirstOrder.Structure.LT ℒₒᵣ M) :

s = LO.FirstOrder.Arith.standardModel M

theorem LO.FirstOrder.Arith.standardModel_unique (M : Type u_1) [LO.ORingStruc M] (s : LO.FirstOrder.Structure ℒₒᵣ M) [hZero : LO.FirstOrder.Structure.Zero ℒₒᵣ M] [hOne : LO.FirstOrder.Structure.One ℒₒᵣ M] [hAdd : LO.FirstOrder.Structure.Add ℒₒᵣ M] [hMul : LO.FirstOrder.Structure.Mul ℒₒᵣ M] [hEq : LO.FirstOrder.Structure.Eq ℒₒᵣ M] [hLT : LO.FirstOrder.Structure.LT ℒₒᵣ M] :

s = LO.FirstOrder.Arith.standardModel M

theorem LO.FirstOrder.Arith.standardModel_lMap_oringEmb_eq_standardModel (M : Type u_1) [LO.ORingStruc M] {L : LO.FirstOrder.Language} [L.ORing] [s : LO.FirstOrder.Structure L M] [LO.FirstOrder.Structure.Zero L M] [LO.FirstOrder.Structure.One L M] [LO.FirstOrder.Structure.Add L M] [LO.FirstOrder.Structure.Mul L M] [LO.FirstOrder.Structure.Eq L M] [LO.FirstOrder.Structure.LT L M] :

LO.FirstOrder.Structure.lMap LO.FirstOrder.Language.oringEmb s = LO.FirstOrder.Arith.standardModel M

@[simp]

theorem LO.FirstOrder.Arith.val_lMap_oringEmb {n : ℕ} {ξ : Type u_2} {M : Type u_1} [LO.ORingStruc M] {L : LO.FirstOrder.Language} [L.ORing] [s : LO.FirstOrder.Structure L M] [LO.FirstOrder.Structure.Zero L M] [LO.FirstOrder.Structure.One L M] [LO.FirstOrder.Structure.Add L M] [LO.FirstOrder.Structure.Mul L M] [LO.FirstOrder.Structure.Eq L M] [LO.FirstOrder.Structure.LT L M] {e : Fin n → M} {ε : ξ → M} {t : LO.FirstOrder.Semiterm ℒₒᵣ ξ n} :

LO.FirstOrder.Semiterm.valm M e ε (LO.FirstOrder.Semiterm.lMap LO.FirstOrder.Language.oringEmb t) = LO.FirstOrder.Semiterm.valm M e ε t

@[simp]

theorem LO.FirstOrder.Arith.eval_lMap_oringEmb {n : ℕ} {ξ : Type u_2} {M : Type u_1} [LO.ORingStruc M] {L : LO.FirstOrder.Language} [L.ORing] [s : LO.FirstOrder.Structure L M] [LO.FirstOrder.Structure.Zero L M] [LO.FirstOrder.Structure.One L M] [LO.FirstOrder.Structure.Add L M] [LO.FirstOrder.Structure.Mul L M] [LO.FirstOrder.Structure.Eq L M] [LO.FirstOrder.Structure.LT L M] {e : Fin n → M} {ε : ξ → M} {p : LO.FirstOrder.Semiformula ℒₒᵣ ξ n} :

(LO.FirstOrder.Semiformula.Evalm M e ε) ((LO.FirstOrder.Semiformula.lMap LO.FirstOrder.Language.oringEmb) p) ↔ (LO.FirstOrder.Semiformula.Evalm M e ε) p

@[simp]

theorem LO.FirstOrder.Arith.modelsTheory_lMap_oringEmb {L : LO.FirstOrder.Language} [L.ORing] {M : Type u_1} [LO.ORingStruc M] [s : LO.FirstOrder.Structure L M] [LO.FirstOrder.Structure.Zero L M] [LO.FirstOrder.Structure.One L M] [LO.FirstOrder.Structure.Add L M] [LO.FirstOrder.Structure.Mul L M] [LO.FirstOrder.Structure.Eq L M] [LO.FirstOrder.Structure.LT L M] (T : LO.FirstOrder.Theory ℒₒᵣ) :

M ⊧ₘ* LO.FirstOrder.Theory.lMap LO.FirstOrder.Language.oringEmb T ↔ M ⊧ₘ* T

instance LO.FirstOrder.Arith.instModelsTheoryPAMinusOfIOpen {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐈open] :

M ⊧ₘ* 𝐏𝐀⁻

Equations

⋯ = ⋯

instance LO.FirstOrder.Arith.instModelsTheoryIndSchemeORingOpenNatOfIOpen {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐈open] :

M ⊧ₘ* LO.FirstOrder.Theory.indScheme ℒₒᵣ LO.FirstOrder.Semiformula.Open

Equations

⋯ = ⋯

def LO.FirstOrder.Arith.models_PAMinus_of_models_indH {M : Type u_1} [LO.ORingStruc M] (Γ : LO.Polarity) (n : ℕ) [M ⊧ₘ* 𝐈𝐍𝐃Γ n] :

M ⊧ₘ* 𝐏𝐀⁻

Equations

⋯ = ⋯

Instances For

def LO.FirstOrder.Arith.models_indScheme_of_models_indH {M : Type u_1} [LO.ORingStruc M] (Γ : LO.Polarity) (n : ℕ) [M ⊧ₘ* 𝐈𝐍𝐃Γ n] :

M ⊧ₘ* LO.FirstOrder.Theory.indScheme ℒₒᵣ (LO.FirstOrder.Arith.Hierarchy Γ n)

Equations

⋯ = ⋯

Instances For

instance LO.FirstOrder.Arith.models_PAMinus_of_models_peano {M : Type u_1} [LO.ORingStruc M] [M ⊧ₘ* 𝐏𝐀] :

M ⊧ₘ* 𝐏𝐀⁻

Equations

⋯ = ⋯

instance LO.FirstOrder.Arith.Standard.models_CobhamR0 :

ℕ ⊧ₘ* 𝐑₀

Equations

LO.FirstOrder.Arith.Standard.models_CobhamR0 = ⋯

instance LO.FirstOrder.Arith.Standard.models_PAMinus :

ℕ ⊧ₘ* 𝐏𝐀⁻

Equations

LO.FirstOrder.Arith.Standard.models_PAMinus = ⋯

theorem LO.FirstOrder.Arith.Standard.models_succInd (p : LO.FirstOrder.Semiformula ℒₒᵣ ℕ 1) :

ℕ ⊧ₘ LO.FirstOrder.succInd p

instance LO.FirstOrder.Arith.Standard.models_iSigma (Γ : LO.Polarity) (k : ℕ) :

ℕ ⊧ₘ* 𝐈𝐍𝐃Γ k

Equations

⋯ = ⋯

instance LO.FirstOrder.Arith.Standard.models_iSigmaZero :

ℕ ⊧ₘ* 𝐈𝚺₀

Equations

LO.FirstOrder.Arith.Standard.models_iSigmaZero = ⋯

instance LO.FirstOrder.Arith.Standard.models_iSigmaOne :

ℕ ⊧ₘ* 𝐈𝚺₁

Equations

LO.FirstOrder.Arith.Standard.models_iSigmaOne = ⋯

instance LO.FirstOrder.Arith.Standard.models_peano :

ℕ ⊧ₘ* 𝐏𝐀

Equations

LO.FirstOrder.Arith.Standard.models_peano = ⋯

structure LO.FirstOrder.Arith.Cut (L : LO.FirstOrder.Language) [L.ORing] (M : Type w) [s : LO.FirstOrder.Structure L M] :

domain : Set M
closedSucc : ∀ x ∈ self.domain, LO.FirstOrder.Semiterm.valb s ![x] (‘(!!(LO.FirstOrder.Semiterm.bvar 0) + 1)’) ∈ self.domain
closedLt : ∀ (x y : M), (LO.FirstOrder.Semiformula.Evalb s ![x, y]) (“!!(LO.FirstOrder.Semiterm.bvar 0) < !!(LO.FirstOrder.Semiterm.bvar 1)”) → y ∈ self.domain → x ∈ self.domain

Instances For

theorem LO.FirstOrder.Arith.Cut.closedSucc {L : LO.FirstOrder.Language} [L.ORing] {M : Type w} [s : LO.FirstOrder.Structure L M] (self : LO.FirstOrder.Arith.Cut L M) (x : M) :

x ∈ self.domain → LO.FirstOrder.Semiterm.valb s ![x] (‘(!!(LO.FirstOrder.Semiterm.bvar 0) + 1)’) ∈ self.domain

theorem LO.FirstOrder.Arith.Cut.closedLt {L : LO.FirstOrder.Language} [L.ORing] {M : Type w} [s : LO.FirstOrder.Structure L M] (self : LO.FirstOrder.Arith.Cut L M) (x : M) (y : M) :

(LO.FirstOrder.Semiformula.Evalb s ![x, y]) (“!!(LO.FirstOrder.Semiterm.bvar 0) < !!(LO.FirstOrder.Semiterm.bvar 1)”) → y ∈ self.domain → x ∈ self.domain

structure LO.FirstOrder.Arith.ClosedCut (L : LO.FirstOrder.Language) [L.ORing] (M : Type w) [s : LO.FirstOrder.Structure L M] extends LO.FirstOrder.Structure.ClosedSubset :

domain : Set M
domain_closed : ∀ {k : ℕ} (f : L.Func k) {v : Fin k → M}, (∀ (i : Fin k), v i ∈ self.domain) → LO.FirstOrder.Structure.func f v ∈ self.domain
closedLt : ∀ (x y : M), (LO.FirstOrder.Semiformula.Evalb s ![x, y]) (“!!(LO.FirstOrder.Semiterm.bvar 0) < !!(LO.FirstOrder.Semiterm.bvar 1)”) → y ∈ self.domain → x ∈ self.domain

Instances For

theorem LO.FirstOrder.Arith.ClosedCut.closedLt {L : LO.FirstOrder.Language} [L.ORing] {M : Type w} [s : LO.FirstOrder.Structure L M] (self : LO.FirstOrder.Arith.ClosedCut L M) (x : M) (y : M) :

(LO.FirstOrder.Semiformula.Evalb s ![x, y]) (“!!(LO.FirstOrder.Semiterm.bvar 0) < !!(LO.FirstOrder.Semiterm.bvar 1)”) → y ∈ self.domain → x ∈ self.domain

@[reducible, inline]

abbrev LO.FirstOrder.Arith.Theory.TrueArith :

LO.FirstOrder.Theory ℒₒᵣ

Equations

𝐓𝐀 = LO.FirstOrder.Structure.theory ℒₒᵣ ℕ

Instances For

def LO.FirstOrder.Arith.«term𝐓𝐀» :

Lean.ParserDescr

Equations

LO.FirstOrder.Arith.«term𝐓𝐀» = Lean.ParserDescr.node `LO.FirstOrder.Arith.term𝐓𝐀 1024 (Lean.ParserDescr.symbol "𝐓𝐀")

Instances For

instance LO.FirstOrder.Arith.Standard.models_trueArith :

ℕ ⊧ₘ* 𝐓𝐀

Equations

LO.FirstOrder.Arith.Standard.models_trueArith = ⋯

theorem LO.FirstOrder.Arith.oRing_consequence_of (T : LO.FirstOrder.Theory ℒₒᵣ) [𝐄𝐐 ≼ T] (p : LO.FirstOrder.SyntacticFormula ℒₒᵣ) (H : ∀ (M : Type u_1) [inst : LO.ORingStruc M] [inst_1 : M ⊧ₘ* T], M ⊧ₘ p) :

T ⊨ p

instance LO.FirstOrder.Theory.CobhamR0.consistent :

LO.System.Consistent 𝐑₀

Equations

LO.FirstOrder.Theory.CobhamR0.consistent = ⋯

instance LO.FirstOrder.Theory.Peano.consistent :

LO.System.Consistent 𝐏𝐀

Equations

LO.FirstOrder.Theory.Peano.consistent = ⋯