Documentation

Foundation.FirstOrder.Arithmetic.Basic.Model

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

@[instance_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.provable_iff_of_models_iff {T : ArithmeticTheory} [𝗘𝗤 ℒₒᵣ ⪯ T] {n : ℕ} {φ ψ : ArithmeticSemisentence n} (h : ∀ (V : Type) [inst : ORingStructure V] [V↓[ℒₒᵣ ] ⊧* T] (e : Fin n → V), (Semiformula.Evalb e) φ ↔ (Semiformula.Evalb e) ψ) :

T ⊢ ∀¹* (φ 🡘 ψ)

theorem LO.FirstOrder.Arithmetic.models_iff_of_provable_iff {T : ArithmeticTheory} [𝗘𝗤 ℒₒᵣ ⪯ T] {n : ℕ} {φ ψ : ArithmeticSemisentence n} (h : T ⊢ ∀¹* (φ 🡘 ψ)) (V : Type u_1) [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* T] (e : Fin n → V) :

(Semiformula.Evalb e) φ ↔ (Semiformula.Evalb e) ψ

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.SoundOn.of_weakerThan (F : ArithmeticSentence → Prop) (T U : ArithmeticTheory) [U ⪯ T] [T.SoundOn F] :

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

Entailment.Consistent T