Model #

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[implicit_reducible]

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.

source

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

Structure.Eq ℒₒᵣ M

source

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

Structure.Zero ℒₒᵣ M

source

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

Structure.One ℒₒᵣ M

source

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

Structure.Add ℒₒᵣ M

source

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

Structure.Mul ℒₒᵣ M

source

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

Structure.Eq ℒₒᵣ M

source

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

Structure.LT ℒₒᵣ M

source

@[implicit_reducible]

instance LO.FirstOrder.Arith.instORingORing :

ℒₒᵣ.ORing

Equations

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

source

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

source

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

source

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

source

@[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

source

@[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 ε) φ

source

@[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

source

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

M ⊧ₘ* 𝐏𝐀⁻

source

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

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

source

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

M ⊧ₘ* 𝐏𝐀⁻

Imported declaration from the Incompleteness formalization.

source

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

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

Imported declaration from the Incompleteness formalization.

source

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

M ⊧ₘ* 𝐏𝐀⁻

source

instance LO.FirstOrder.Arith.Standard.models_CobhamR0 :

ℕ ⊧ₘ* 𝐑₀

source

instance LO.FirstOrder.Arith.Standard.models_PeanoMinus :

ℕ ⊧ₘ* 𝐏𝐀⁻

source

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

ℕ ⊧ₘ succInd φ

source

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

ℕ ⊧ₘ* 𝐈𝐍𝐃Γ k

source

instance LO.FirstOrder.Arith.Standard.models_iSigmaZero :

ℕ ⊧ₘ* 𝐈Sg0

source

instance LO.FirstOrder.Arith.Standard.models_iSigmaOne :

ℕ ⊧ₘ* 𝐈Sg1

source

instance LO.FirstOrder.Arith.Standard.models_peano :

ℕ ⊧ₘ* 𝐏𝐀

source

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

Type w

Imported declaration from the Incompleteness formalization.

domain : Set M
Imported declaration from the Incompleteness formalization.
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

source

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

Type w

Imported declaration from the Incompleteness formalization.

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

source

@[reducible, inline]

abbrev LO.FirstOrder.Arith.Theory.TrueArith :

Theory ℒₒᵣ

Imported declaration from the Incompleteness formalization.

Equations

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

Instances For

source

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

Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

Instances For

source

instance LO.FirstOrder.Arith.Standard.models_trueArith :

ℕ ⊧ₘ* 𝐓𝐀

source

theorem LO.FirstOrder.Arith.trueArith_provable_iff {φ : SyntacticFormula ℒₒᵣ} :

𝐓𝐀 ⊢! φ ↔ ℕ ⊧ₘ φ

source

instance LO.FirstOrder.Arith.instWeakerThanSyntacticFormulaORingTheoryTrueArithOfModelsTheoryNat (T : Theory ℒₒᵣ) [ℕ ⊧ₘ* T] :

T wkn 𝐓𝐀

source

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

T ⊨ φ

source

theorem LO.FirstOrder.Arith.oRing_weakerThan_of (T S : Theory ℒₒᵣ) [𝐄𝐐 wkn S] (H : ∀ (M : Type u_1) [inst : ORingStruc M] [M ⊧ₘ* S], M ⊧ₘ* T) :

T wkn S

source

instance LO.FirstOrder.Theory.CobhamR0.consistent :

Entailment.Consistent 𝐑₀

source

instance LO.FirstOrder.Theory.Peano.consistent :

Entailment.Consistent 𝐏𝐀

source

instance LO.FirstOrder.Theory.TrueArith.consistent :

Entailment.Consistent 𝐓𝐀

Documentation

LeanPool.Incompleteness.Foundation.FirstOrder.Arith.Model

Model #