Documentation

LeanPool.PointwiseComposition.Foundation.FirstOrder.Arithmetic.Basic.Model

Supporting results for pointwise provable equality.

source
@[instance_reducible]
instance PointwiseComposition.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.
source
instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instEqORing (M : Type u_1) [ORingStructure M] :
Tarski.Structure.Eq ℒₒᵣ M
source
instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instZeroORing (M : Type u_1) [ORingStructure M] :
Tarski.Structure.Zero ℒₒᵣ M
source
instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instOneORing (M : Type u_1) [ORingStructure M] :
Tarski.Structure.One ℒₒᵣ M
source
instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instAddORing (M : Type u_1) [ORingStructure M] :
Tarski.Structure.Add ℒₒᵣ M
source
instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instMulORing (M : Type u_1) [ORingStructure M] :
Tarski.Structure.Mul ℒₒᵣ M
source
instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instEqORing_1 (M : Type u_1) [ORingStructure M] :
Tarski.Structure.Eq ℒₒᵣ M
source
instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instLTORing (M : Type u_1) [ORingStructure M] :
Tarski.Structure.LT ℒₒᵣ M
source
@[instance_reducible]
instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instORingORing :
ℒₒᵣ.ORing
Equations
  • One or more equations did not get rendered due to their size.
source
theorem PointwiseComposition.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
source
theorem PointwiseComposition.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
source
theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.complete (T : ArithmeticTheory) [𝐄𝐐 ℒₒᵣ ≼ T] (φ : ArithmeticSentence) (H : ∀ (M : Type u_1) [inst : ORingStructure M] [M↓[ℒₒᵣ] ⊧* T], M↓[ℒₒᵣ] ⊧ φ) :
T ⊢ φ

provable_of_models

source
theorem PointwiseComposition.FFL.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 ⊢ ∀¹* (φ ⇔ₗ ψ)
source
theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.models_iff_of_provable_iff {T : ArithmeticTheory} {n : ℕ} {φ ψ : ArithmeticSemisentence n} (h : T ⊢ ∀¹* (φ ⇔ₗ ψ)) (V : Type u_1) [ORingStructure V] [V↓[ℒₒᵣ] ⊧* T] (e : Fin n → V) :
(Semiformula.Evalb e) φ ↔ (Semiformula.Evalb e) ψ
source
theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.weakerThan_of_models (T S : ArithmeticTheory) [𝐄𝐐 ℒₒᵣ ≼ S] (H : ∀ (M : Type u_1) [inst : ORingStructure M] [M↓[ℒₒᵣ] ⊧* S], M↓[ℒₒᵣ] ⊧* T) :
T ≼ S
source
theorem PointwiseComposition.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
source
class PointwiseComposition.FFL.FirstOrder.ArithmeticTheory.SoundOn (T : ArithmeticTheory) (F : ArithmeticSentence → Prop) :
Prop

Data and laws for Sound On in FFL.FirstOrder.ArithmeticTheory.

Instances
    source
    instance PointwiseComposition.FFL.FirstOrder.ArithmeticTheory.instSoundOnOfModelsSetStrucORingSentenceStrNat (T : ArithmeticTheory) (F : ArithmeticSentence → Prop) [ℕ↓[ℒₒᵣ] ⊧* T] :
    T.SoundOn F
    source
    theorem PointwiseComposition.FFL.FirstOrder.ArithmeticTheory.SoundOn.of_weakerThan (F : ArithmeticSentence → Prop) (T U : ArithmeticTheory) [U ≼ T] [T.SoundOn F] :
    U.SoundOn F
    source
    theorem PointwiseComposition.FFL.FirstOrder.ArithmeticTheory.consistent_of_sound (T : ArithmeticTheory) (F : ArithmeticSentence → Prop) [T.SoundOn F] (hF : F ⊥) :
    Entailment.Consistent T