Documentation

Foundation.FirstOrder.Arith.Model

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

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

Structure ℒₒᵣ M

Equations

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

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

Structure.Eq ℒₒᵣ M

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

Structure.Zero ℒₒᵣ M

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

Structure.One ℒₒᵣ M

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

Structure.Add ℒₒᵣ M

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

Structure.Mul ℒₒᵣ M

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

Structure.Eq ℒₒᵣ M

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

Structure.LT ℒₒᵣ M

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) [ORingStruc M] (s : Structure ℒₒᵣ M) (hZero : Structure.Zero ℒₒᵣ M) (hOne : Structure.One ℒₒᵣ M) (hAdd : Structure.Add ℒₒᵣ M) (hMul : Structure.Mul ℒₒᵣ M) (hEq : Structure.Eq ℒₒᵣ M) (hLT : Structure.LT ℒₒᵣ M) :

s = standardModel M

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

s = standardModel M

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

Structure.lMap Language.oringEmb s = standardModel M

@[simp]

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

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

@[simp]

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

(Semiformula.Evalm M e ε) ((Semiformula.lMap Language.oringEmb) φ) ↔ (Semiformula.Evalm M e ε) φ

@[simp]

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

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

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

M ⊧ₘ* 𝐏𝐀⁻

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

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

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

M ⊧ₘ* 𝐏𝐀⁻

Equations

⋯ = ⋯

Instances For

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

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

Equations

⋯ = ⋯

Instances For

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

M ⊧ₘ* 𝐏𝐀⁻

instance LO.FirstOrder.Arith.Standard.models_CobhamR0 :

ℕ ⊧ₘ* 𝐑₀

instance LO.FirstOrder.Arith.Standard.models_PAMinus :

ℕ ⊧ₘ* 𝐏𝐀⁻

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

ℕ ⊧ₘ succInd φ

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

ℕ ⊧ₘ* 𝐈𝐍𝐃Γ k

instance LO.FirstOrder.Arith.Standard.models_iSigmaZero :

ℕ ⊧ₘ* 𝐈𝚺₀

instance LO.FirstOrder.Arith.Standard.models_iSigmaOne :

ℕ ⊧ₘ* 𝐈𝚺₁

instance LO.FirstOrder.Arith.Standard.models_peano :

ℕ ⊧ₘ* 𝐏𝐀

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

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

Instances For

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

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

Instances For

@[reducible, inline]

abbrev LO.FirstOrder.Arith.Theory.TrueArith :

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 :

ℕ ⊧ₘ* 𝐓𝐀

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

T ⊨ φ

instance LO.FirstOrder.Theory.CobhamR0.consistent :

System.Consistent 𝐑₀

instance LO.FirstOrder.Theory.Peano.consistent :

System.Consistent 𝐏𝐀