Documentation

Foundation.FirstOrder.Arithmetic.Basic.Model

@[implicit_reducible]

instance LO.FirstOrder.Arithmetic.standardModel (M : Type u_1) [ORingStructure M] :

Structure ℒₒᵣ M

Equations

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

instance LO.FirstOrder.Arithmetic.instEqORing (M : Type u_1) [ORingStructure M] :

Structure.Eq ℒₒᵣ M

instance LO.FirstOrder.Arithmetic.instZeroORing (M : Type u_1) [ORingStructure M] :

Structure.Zero ℒₒᵣ M

instance LO.FirstOrder.Arithmetic.instOneORing (M : Type u_1) [ORingStructure M] :

Structure.One ℒₒᵣ M

instance LO.FirstOrder.Arithmetic.instAddORing (M : Type u_1) [ORingStructure M] :

Structure.Add ℒₒᵣ M

instance LO.FirstOrder.Arithmetic.instMulORing (M : Type u_1) [ORingStructure M] :

Structure.Mul ℒₒᵣ M

instance LO.FirstOrder.Arithmetic.instEqORing_1 (M : Type u_1) [ORingStructure M] :

Structure.Eq ℒₒᵣ M

instance LO.FirstOrder.Arithmetic.instLTORing (M : Type u_1) [ORingStructure M] :

Structure.LT ℒₒᵣ M

@[implicit_reducible]

instance LO.FirstOrder.Arithmetic.instORingORing :

ℒₒᵣ.ORing

Equations

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

theorem LO.FirstOrder.Arithmetic.standardModel_unique' (M : Type u_1) [ORingStructure 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.Arithmetic.standardModel_unique (M : Type u_1) [ORingStructure 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.Arithmetic.complete (T : ArithmeticTheory) [𝗘𝗤 ℒₒᵣ ⪯ T] (φ : ArithmeticSentence) (H : ∀ (M : Type u_1) [inst : ORingStructure M] [M↓[ℒₒᵣ ] ⊧* T], M↓[ℒₒᵣ ] ⊧ φ) :

T ⊢ φ

provable_of_models

theorem LO.FirstOrder.Arithmetic.weakerThan_of_models (T S : ArithmeticTheory) [𝗘𝗤 ℒₒᵣ ⪯ S] (H : ∀ (M : Type u_1) [inst : ORingStructure M] [M↓[ℒₒᵣ ] ⊧* S], M↓[ℒₒᵣ ] ⊧* T) :

T ⪯ S

class LO.FirstOrder.ArithmeticTheory.SoundOn (T : ArithmeticTheory) (F : ArithmeticSentence → Prop) :

sound {σ : Sentence ℒₒᵣ} : T ⊢ σ → F σ → ℕ ↓[ℒₒᵣ ] ⊧ σ

Instances

instance LO.FirstOrder.ArithmeticTheory.instSoundOnOfModelsSetStrucORingSentenceStrNat (T : ArithmeticTheory) (F : ArithmeticSentence → Prop) [ℕ ↓[ℒₒᵣ ] ⊧* T] :

theorem LO.FirstOrder.ArithmeticTheory.consistent_of_sound (T : ArithmeticTheory) (F : ArithmeticSentence → Prop) [T.SoundOn F] (hF : F ⊥) :

Entailment.Consistent T