Documentation

LeanPool.PointwiseComposition.Foundation.FirstOrder.LK.Eq

Supporting results for pointwise provable equality.

source
theorem PointwiseComposition.FFL.FirstOrder.consequence_iff_eq {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝐄𝐐 L ≼ T] {σ : Sentence L} :
T ⊨[Tarski.Struc L] σ ↔ ∀ (M : Type v) [inst : Nonempty M] [inst_1 : Tarski.Structure L M] [Tarski.Structure.Eq L M], M↓[L] ⊧* T → M↓[L] ⊧ σ
source
theorem PointwiseComposition.FFL.FirstOrder.consequence_iff_eq' {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝐄𝐐 L ≼ T] {σ : Sentence L} :
T ⊨[Tarski.Struc L] σ ↔ ∀ (M : Type v) [inst : Nonempty M] [inst_1 : Tarski.Structure L M] [Tarski.Structure.Eq L M] [M↓[L] ⊧* T], M↓[L] ⊧ σ
source
theorem PointwiseComposition.FFL.FirstOrder.satisfiable_iff_eq {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝐄𝐐 L ≼ T] :
Semantics.Satisfiable (Tarski.Struc L) T ↔ ∃ (M : Type v) (x : Nonempty M) (x_1 : Tarski.Structure L M) (_ : Tarski.Structure.Eq L M), M↓[L] ⊧* T
source
instance PointwiseComposition.FFL.FirstOrder.instModelsSetStrucSentenceStrModelOfSatEqAxiomOfWeakerThanTheory {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝐄𝐐 L ≼ T] (sat : Semantics.Satisfiable (Tarski.Struc L) T) :
(ModelOfSat sat)↓[L] ⊧* 𝐄𝐐 L
source
def PointwiseComposition.FFL.FirstOrder.ModelOfSatEq {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝐄𝐐 L ≼ T] (sat : Semantics.Satisfiable (Tarski.Struc L) T) :
Type v

The Model Of Sat Eq construction in FFL.FirstOrder.

Equations
Instances For
    source
    instance PointwiseComposition.FFL.FirstOrder.ModelOfSatEq.instNonempty {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝐄𝐐 L ≼ T] (sat : Semantics.Satisfiable (Tarski.Struc L) T) :
    Nonempty (ModelOfSatEq sat)
    source
    @[instance_reducible]
    noncomputable instance PointwiseComposition.FFL.FirstOrder.ModelOfSatEq.struc {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝐄𝐐 L ≼ T] (sat : Semantics.Satisfiable (Tarski.Struc L) T) :
    Tarski.Structure L (ModelOfSatEq sat)
    Equations
    source
    instance PointwiseComposition.FFL.FirstOrder.ModelOfSatEq.instEq {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝐄𝐐 L ≼ T] (sat : Semantics.Satisfiable (Tarski.Struc L) T) :
    Tarski.Structure.Eq L (ModelOfSatEq sat)
    source
    theorem PointwiseComposition.FFL.FirstOrder.ModelOfSatEq.models {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝐄𝐐 L ≼ T] (sat : Semantics.Satisfiable (Tarski.Struc L) T) :
    (ModelOfSatEq sat)↓[L] ⊧* T
    source
    instance PointwiseComposition.FFL.FirstOrder.ModelOfSatEq.mod {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝐄𝐐 L ≼ T] (sat : Semantics.Satisfiable (Tarski.Struc L) T) :
    (ModelOfSatEq sat)↓[L] ⊧* T
    source
    @[instance_reducible]
    noncomputable instance PointwiseComposition.FFL.FirstOrder.ModelOfSatEq.instZeroOfZero {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝐄𝐐 L ≼ T] (sat : Semantics.Satisfiable (Tarski.Struc L) T) [Semiterm.Operator.Zero L] :
    Zero (ModelOfSatEq sat)
    Equations
    source
    instance PointwiseComposition.FFL.FirstOrder.ModelOfSatEq.strucZero {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝐄𝐐 L ≼ T] (sat : Semantics.Satisfiable (Tarski.Struc L) T) [Semiterm.Operator.Zero L] :
    Tarski.Structure.Zero L (ModelOfSatEq sat)
    source
    @[instance_reducible]
    noncomputable instance PointwiseComposition.FFL.FirstOrder.ModelOfSatEq.instOneOfOne {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝐄𝐐 L ≼ T] (sat : Semantics.Satisfiable (Tarski.Struc L) T) [Semiterm.Operator.One L] :
    One (ModelOfSatEq sat)
    Equations
    source
    instance PointwiseComposition.FFL.FirstOrder.ModelOfSatEq.instOne {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝐄𝐐 L ≼ T] (sat : Semantics.Satisfiable (Tarski.Struc L) T) [Semiterm.Operator.One L] :
    Tarski.Structure.One L (ModelOfSatEq sat)
    source
    @[instance_reducible]
    noncomputable instance PointwiseComposition.FFL.FirstOrder.ModelOfSatEq.instAddOfAdd {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝐄𝐐 L ≼ T] (sat : Semantics.Satisfiable (Tarski.Struc L) T) [Semiterm.Operator.Add L] :
    Add (ModelOfSatEq sat)
    Equations
    • One or more equations did not get rendered due to their size.
    source
    instance PointwiseComposition.FFL.FirstOrder.ModelOfSatEq.instAdd {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝐄𝐐 L ≼ T] (sat : Semantics.Satisfiable (Tarski.Struc L) T) [Semiterm.Operator.Add L] :
    Tarski.Structure.Add L (ModelOfSatEq sat)
    source
    @[instance_reducible]
    noncomputable instance PointwiseComposition.FFL.FirstOrder.ModelOfSatEq.instMulOfMul {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝐄𝐐 L ≼ T] (sat : Semantics.Satisfiable (Tarski.Struc L) T) [Semiterm.Operator.Mul L] :
    Mul (ModelOfSatEq sat)
    Equations
    • One or more equations did not get rendered due to their size.
    source
    instance PointwiseComposition.FFL.FirstOrder.ModelOfSatEq.instMul {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝐄𝐐 L ≼ T] (sat : Semantics.Satisfiable (Tarski.Struc L) T) [Semiterm.Operator.Mul L] :
    Tarski.Structure.Mul L (ModelOfSatEq sat)
    source
    @[instance_reducible]
    instance PointwiseComposition.FFL.FirstOrder.ModelOfSatEq.instLTOfLT {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝐄𝐐 L ≼ T] (sat : Semantics.Satisfiable (Tarski.Struc L) T) [Semiformula.Operator.LT L] :
    LT (ModelOfSatEq sat)
    Equations
    • One or more equations did not get rendered due to their size.
    source
    instance PointwiseComposition.FFL.FirstOrder.ModelOfSatEq.instLT {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝐄𝐐 L ≼ T] (sat : Semantics.Satisfiable (Tarski.Struc L) T) [Semiformula.Operator.LT L] :
    Tarski.Structure.LT L (ModelOfSatEq sat)
    source
    @[instance_reducible]
    instance PointwiseComposition.FFL.FirstOrder.ModelOfSatEq.instMembershipOfMem {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝐄𝐐 L ≼ T] (sat : Semantics.Satisfiable (Tarski.Struc L) T) [Semiformula.Operator.Mem L] :
    Membership (ModelOfSatEq sat) (ModelOfSatEq sat)
    Equations
    • One or more equations did not get rendered due to their size.
    source
    instance PointwiseComposition.FFL.FirstOrder.ModelOfSatEq.instMem {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝐄𝐐 L ≼ T] (sat : Semantics.Satisfiable (Tarski.Struc L) T) [Semiformula.Operator.Mem L] :
    Tarski.Structure.Mem L (ModelOfSatEq sat)