Documentation

Logic.FirstOrder.Arith.EA.Basic

instance LO.FirstOrder.Arith.instORingORingExp :

ℒₒᵣ(exp).ORing

Equations

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

theorem LO.FirstOrder.Arith.consequence_of_exp {L : LO.FirstOrder.Language} [L.ORing] (T : LO.FirstOrder.Theory L) [𝐄𝐐 ≼ T] [L.Exp] (σ : LO.FirstOrder.Sentence L) (H : ∀ (M : Type u) [inst : Zero M] [inst_1 : One M] [inst_2 : Add M] [inst_3 : Mul M] [inst_4 : Exp M] [inst_5 : LT M] [inst_6 : LO.FirstOrder.Structure L M] [inst : LO.FirstOrder.Structure.ORing L M] [inst : LO.FirstOrder.Structure.Exp L M] [inst : M ⊧ₘ* T], M ⊧ₘ σ) :

T ⊨ σ

inductive LO.FirstOrder.Arith.Theory.Exponential :

LO.FirstOrder.Theory ℒₒᵣ(exp)

zero: 𝐄𝐗𝐏 (“!!(LO.FirstOrder.Semiterm.Operator.Exp.exp.operator ![‘0’]) = 1”)
succ: 𝐄𝐗𝐏 (“∀' !!(LO.FirstOrder.Semiterm.Operator.Exp.exp.operator ![‘(!!(LO.FirstOrder.Semiterm.bvar 0) + 1)’]) = (2 * !!(LO.FirstOrder.Semiterm.Operator.Exp.exp.operator ![LO.FirstOrder.Semiterm.bvar 0]))”)

Instances For

def LO.FirstOrder.Arith.Theory.«term𝐄𝐗𝐏» :

Lean.ParserDescr

Equations

LO.FirstOrder.Arith.Theory.«term𝐄𝐗𝐏» = Lean.ParserDescr.node `LO.FirstOrder.Arith.Theory.term𝐄𝐗𝐏 1024 (Lean.ParserDescr.symbol "𝐄𝐗𝐏")

Instances For

@[reducible, inline]

abbrev LO.FirstOrder.Arith.Theory.elementaryArithmetic :

LO.FirstOrder.Theory ℒₒᵣ(exp)

Equations

𝐄𝐀 = ⇑(LO.FirstOrder.Semiformula.lMap LO.FirstOrder.Language.oringEmb) '' 𝐏𝐀⁻ + 𝐄𝐗𝐏 + LO.FirstOrder.Arith.Theory.indScheme ℒₒᵣ(exp) (LO.FirstOrder.Arith.Hierarchy 𝚺 0)

Instances For

def LO.FirstOrder.Arith.Theory.«term𝐄𝐀» :

Lean.ParserDescr

Equations

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

Instances For

theorem LO.FirstOrder.Arith.Theory.iSigma₀_subset_EA :

⇑(LO.FirstOrder.Semiformula.lMap LO.FirstOrder.Language.oringEmb) '' 𝐈𝚺₀ ⊆ 𝐄𝐀

instance LO.FirstOrder.Arith.standardModelExp (M : Type u_1) [Zero M] [One M] [Add M] [Exp M] [Mul M] [LT M] :

LO.FirstOrder.Structure ℒₒᵣ(exp) M

Equations

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

instance LO.FirstOrder.Arith.instEqORingExp (M : Type u_1) [Zero M] [One M] [Add M] [Exp M] [Mul M] [LT M] :

LO.FirstOrder.Structure.Eq ℒₒᵣ(exp) M

Equations

⋯ = ⋯

instance LO.FirstOrder.Arith.instZeroORingExp (M : Type u_1) [Zero M] [One M] [Add M] [Exp M] [Mul M] [LT M] :

LO.FirstOrder.Structure.Zero ℒₒᵣ(exp) M

Equations

⋯ = ⋯

instance LO.FirstOrder.Arith.instOneORingExp (M : Type u_1) [Zero M] [One M] [Add M] [Exp M] [Mul M] [LT M] :

LO.FirstOrder.Structure.One ℒₒᵣ(exp) M

Equations

⋯ = ⋯

instance LO.FirstOrder.Arith.instAddORingExp (M : Type u_1) [Zero M] [One M] [Add M] [Exp M] [Mul M] [LT M] :

LO.FirstOrder.Structure.Add ℒₒᵣ(exp) M

Equations

⋯ = ⋯

instance LO.FirstOrder.Arith.instMulORingExp (M : Type u_1) [Zero M] [One M] [Add M] [Exp M] [Mul M] [LT M] :

LO.FirstOrder.Structure.Mul ℒₒᵣ(exp) M

Equations

⋯ = ⋯

instance LO.FirstOrder.Arith.instExpORingExp (M : Type u_1) [Zero M] [One M] [Add M] [Exp M] [Mul M] [LT M] :

LO.FirstOrder.Structure.Exp ℒₒᵣ(exp) M

Equations

⋯ = ⋯

instance LO.FirstOrder.Arith.instEqORingExp_1 (M : Type u_1) [Zero M] [One M] [Add M] [Exp M] [Mul M] [LT M] :

LO.FirstOrder.Structure.Eq ℒₒᵣ(exp) M

Equations

⋯ = ⋯

instance LO.FirstOrder.Arith.instLTORingExp (M : Type u_1) [Zero M] [One M] [Add M] [Exp M] [Mul M] [LT M] :

LO.FirstOrder.Structure.LT ℒₒᵣ(exp) M

Equations

⋯ = ⋯

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

s = LO.FirstOrder.Arith.standardModelExp M

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

s = LO.FirstOrder.Arith.standardModelExp M

def LO.FirstOrder.Arith.Standard.instExpNat :

Equations

LO.FirstOrder.Arith.Standard.instExpNat = { exp := fun (x : ℕ) => 2 ^ x }

Instances For

theorem LO.FirstOrder.Arith.Standard.Nat.exp_def (n : ℕ) :

exp n = 2 ^ n

@[simp]

theorem LO.FirstOrder.Arith.Standard.Nat.exp_zero :

exp 0 = 1

theorem LO.FirstOrder.Arith.Standard.Nat.exp_succ (n : ℕ) :

exp (n + 1) = 2 * exp n

instance LO.FirstOrder.Arith.Standard.models_exponential :

ℕ ⊧ₘ* 𝐄𝐗𝐏

Equations

LO.FirstOrder.Arith.Standard.models_exponential = ⋯

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

ℕ ⊧ₘ ∀ᶠ* LO.FirstOrder.Arith.succInd p

theorem LO.FirstOrder.Arith.Standard.modelsTheory_elementaryArithmetic :

ℕ ⊧ₘ* 𝐄𝐀

instance LO.Arith.models_peanoMinus_of_models_elementaryArithmetic (M : Type) [Zero M] [One M] [Add M] [Mul M] [Exp M] [LT M] [M ⊧ₘ* 𝐄𝐀] :

M ⊧ₘ* 𝐏𝐀⁻

Equations

⋯ = ⋯

instance LO.Arith.models_exponential_of_models_elementaryArithmetic (M : Type) [Zero M] [One M] [Add M] [Mul M] [Exp M] [LT M] [M ⊧ₘ* 𝐄𝐀] :

M ⊧ₘ* 𝐄𝐗𝐏

Equations

⋯ = ⋯

instance LO.Arith.models_indScheme_of_models_elementaryArithmetic (M : Type) [Zero M] [One M] [Add M] [Mul M] [Exp M] [LT M] [M ⊧ₘ* 𝐄𝐀] :

M ⊧ₘ* LO.FirstOrder.Arith.Theory.indScheme ℒₒᵣ(exp) (LO.FirstOrder.Arith.Hierarchy 𝚺 0)

Equations

⋯ = ⋯

instance LO.Arith.models_iSigmaZero_of_models_elementaryArithmetic (M : Type) [Zero M] [One M] [Add M] [Mul M] [Exp M] [LT M] [M ⊧ₘ* 𝐄𝐀] :

M ⊧ₘ* 𝐈𝚺₀

Equations

⋯ = ⋯