Documentation

Foundation.FirstOrder.Arithmetic.Basic.Model

@[instance_reducible]

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

Tarski.Structure ℒₒᵣ M

Equations

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

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

Tarski.Structure.Eq ℒₒᵣ M

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

Tarski.Structure.Zero ℒₒᵣ M

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

Tarski.Structure.One ℒₒᵣ M

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

Tarski.Structure.Add ℒₒᵣ M

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

Tarski.Structure.Mul ℒₒᵣ M

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

Tarski.Structure.Eq ℒₒᵣ M

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

Tarski.Structure.LT ℒₒᵣ M

@[instance_reducible]

instance FFL.FirstOrder.Arithmetic.instORingORing :

ℒₒᵣ.ORing

Equations

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

theorem FFL.FirstOrder.Arithmetic.standardModel_unique' (M : Type u_1) [ORingStructure M] (s : Tarski.Structure ℒₒᵣ M) (hZero : Tarski.Structure.Zero ℒₒᵣ M) (hOne : Tarski.Structure.One ℒₒᵣ M) (hAdd : Tarski.Structure.Add ℒₒᵣ M) (hMul : Tarski.Structure.Mul ℒₒᵣ M) (hEq : Tarski.Structure.Eq ℒₒᵣ M) (hLT : Tarski.Structure.LT ℒₒᵣ M) :

s = standardModel M

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

s = standardModel M

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

T ⊢ φ

provable_of_models

theorem FFL.FirstOrder.Arithmetic.provable_iff_of_models_iff {T : ArithmeticTheory} [𝗘𝗤 ℒₒᵣ ⪯ T] {n : ℕ} {φ ψ : ArithmeticSemisentence n} (h : ∀ (V : Type u_1) [inst : ORingStructure V] [V↓[ℒₒᵣ ] ⊧* T] (e : Fin n → V), (Semiformula.Evalb e) φ ↔ (Semiformula.Evalb e) ψ) :

T ⊢ ∀¹* (φ 🡘 ψ)

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

T ⪯ S

theorem FFL.FirstOrder.Arithmetic.equiv_of_models {T S : ArithmeticTheory} [𝗘𝗤 ℒₒᵣ ⪯ S] [𝗘𝗤 ℒₒᵣ ⪯ T] (hTS : ∀ (M : Type u_1) [inst : ORingStructure M] [M↓[ℒₒᵣ ] ⊧* S], M↓[ℒₒᵣ ] ⊧* T) (hST : ∀ (M : Type u_2) [inst : ORingStructure M] [M↓[ℒₒᵣ ] ⊧* T], M↓[ℒₒᵣ ] ⊧* S) :

T ≊ S

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

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

Instances

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

theorem FFL.FirstOrder.ArithmeticTheory.SoundOn.of_weakerThan (F : ArithmeticSentence → Prop) (T U : ArithmeticTheory) [U ⪯ T] [T.SoundOn F] :

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

Entailment.Consistent T