theorem 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] ⊧ σ

theorem 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] ⊧ σ

theorem 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

instance 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

def FFL.FirstOrder.ModelOfSatEq {L : Language} [Semiformula.Operator.Eq L] {T : Theory L} [𝗘𝗤 L ⪯ T] (sat : Semantics.Satisfiable (Tarski.Struc L) T) : Type v

Equations

• FFL.FirstOrder.ModelOfSatEq sat = FFL.FirstOrder.Tarski.Structure.Eq.QuotEq L (FFL.FirstOrder.ModelOfSat sat)

instance 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)

@[instance_reducible]

noncomputable instance 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

• FFL.FirstOrder.ModelOfSatEq.struc sat = FFL.FirstOrder.Tarski.Structure.Eq.QuotEq.struc

instance 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)

theorem 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

instance 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

@[instance_reducible]

noncomputable instance 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

• FFL.FirstOrder.ModelOfSatEq.instZeroOfZero sat = { zero := FFL.FirstOrder.Semiterm.Operator.val ![] op(0) }

instance 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)

@[instance_reducible]

noncomputable instance 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

• FFL.FirstOrder.ModelOfSatEq.instOneOfOne sat = { one := FFL.FirstOrder.Semiterm.Operator.val ![] op(1) }

instance 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)

@[instance_reducible]

noncomputable instance 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

• FFL.FirstOrder.ModelOfSatEq.instAddOfAdd sat = { add := fun (x y : FFL.FirstOrder.ModelOfSatEq sat) => FFL.FirstOrder.Semiterm.Operator.val ![x, y] op(+) }

instance 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)

@[instance_reducible]

noncomputable instance 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

• FFL.FirstOrder.ModelOfSatEq.instMulOfMul sat = { mul := fun (x y : FFL.FirstOrder.ModelOfSatEq sat) => FFL.FirstOrder.Semiterm.Operator.val ![x, y] op(*) }

instance 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)

@[instance_reducible]

instance 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

• FFL.FirstOrder.ModelOfSatEq.instLTOfLT sat = { lt := fun (x y : FFL.FirstOrder.ModelOfSatEq sat) => FFL.FirstOrder.Semiformula.Operator.val ![x, y] op(<) }

instance 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)

@[instance_reducible]

instance 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

• FFL.FirstOrder.ModelOfSatEq.instMembershipOfMem sat = { mem := fun (x y : FFL.FirstOrder.ModelOfSatEq sat) => FFL.FirstOrder.Semiformula.Operator.val ![y, x] op(∈) }

instance 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)