Equivalence of Formulas

Main Definitions

• FirstOrder.Language.Theory.SemanticallyEquivalent: φ ⇔[T] ψ indicates that φ and ψ are equivalent formulas or sentences in models of T.

TODO

• Add a definition of implication modulo a theory T, with φ ⇒[T] ψ defined analogously to φ ⇔[T] ψ.
• Construct the quotient of L.Formula α modulo ⇔[T] and its Boolean Algebra structure.

def FirstOrder.Language.Theory.SemanticallyEquivalent {L : FirstOrder.Language} {α : Type w} {n : ℕ} (T : L.Theory) (φ : L.BoundedFormula α n) (ψ : L.BoundedFormula α n) : Prop

Two (bounded) formulas are semantically equivalent over a theory T when they have the same interpretation in every model of T. (This is also known as logical equivalence, which also has a proof-theoretic definition.)

Equations

• T.SemanticallyEquivalent φ ψ = T ⊨ᵇ φ.iff ψ

def FirstOrder.«term_⇔[_]_» : Lean.TrailingParserDescr

Two (bounded) formulas are semantically equivalent over a theory T when they have the same interpretation in every model of T. (This is also known as logical equivalence, which also has a proof-theoretic definition.)

Equations

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

theorem FirstOrder.Language.Theory.SemanticallyEquivalent.refl {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} (φ : L.BoundedFormula α n) : T.SemanticallyEquivalent φ φ

instance FirstOrder.Language.Theory.SemanticallyEquivalent.instIsReflBoundedFormula {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} : IsRefl (L.BoundedFormula α n) T.SemanticallyEquivalent

Equations

• ⋯ = ⋯

theorem FirstOrder.Language.Theory.SemanticallyEquivalent.symm {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} {φ : L.BoundedFormula α n} {ψ : L.BoundedFormula α n} (h : T.SemanticallyEquivalent φ ψ) : T.SemanticallyEquivalent ψ φ

theorem FirstOrder.Language.Theory.SemanticallyEquivalent.trans {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} {φ : L.BoundedFormula α n} {ψ : L.BoundedFormula α n} {θ : L.BoundedFormula α n} (h1 : T.SemanticallyEquivalent φ ψ) (h2 : T.SemanticallyEquivalent ψ θ) : T.SemanticallyEquivalent φ θ

theorem FirstOrder.Language.Theory.SemanticallyEquivalent.realize_bd_iff {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} {M : Type u_1} [Nonempty M] [L.Structure M] [M ⊨ T] {φ : L.BoundedFormula α n} {ψ : L.BoundedFormula α n} (h : T.SemanticallyEquivalent φ ψ) {v : α → M} {xs : Fin n → M} : φ.Realize v xs ↔ ψ.Realize v xs

theorem FirstOrder.Language.Theory.SemanticallyEquivalent.realize_iff {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {φ : L.Formula α} {ψ : L.Formula α} {M : Type u_2} [Nonempty M] [L.Structure M] [M ⊨ T] (h : T.SemanticallyEquivalent φ ψ) {v : α → M} : φ.Realize v ↔ ψ.Realize v

theorem FirstOrder.Language.Theory.SemanticallyEquivalent.models_sentence_iff {L : FirstOrder.Language} {T : L.Theory} {φ : L.Sentence} {ψ : L.Sentence} {M : Type u_2} [Nonempty M] [L.Structure M] [M ⊨ T] (h : T.SemanticallyEquivalent φ ψ) : M ⊨ φ ↔ M ⊨ ψ

theorem FirstOrder.Language.Theory.SemanticallyEquivalent.all {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} {φ : L.BoundedFormula α (n + 1)} {ψ : L.BoundedFormula α (n + 1)} (h : T.SemanticallyEquivalent φ ψ) : T.SemanticallyEquivalent φ.all ψ.all

theorem FirstOrder.Language.Theory.SemanticallyEquivalent.ex {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} {φ : L.BoundedFormula α (n + 1)} {ψ : L.BoundedFormula α (n + 1)} (h : T.SemanticallyEquivalent φ ψ) : T.SemanticallyEquivalent φ.ex ψ.ex

theorem FirstOrder.Language.Theory.SemanticallyEquivalent.not {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} {φ : L.BoundedFormula α n} {ψ : L.BoundedFormula α n} (h : T.SemanticallyEquivalent φ ψ) : T.SemanticallyEquivalent φ.not ψ.not

theorem FirstOrder.Language.Theory.SemanticallyEquivalent.imp {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} {φ : L.BoundedFormula α n} {ψ : L.BoundedFormula α n} {φ' : L.BoundedFormula α n} {ψ' : L.BoundedFormula α n} (h : T.SemanticallyEquivalent φ ψ) (h' : T.SemanticallyEquivalent φ' ψ') : T.SemanticallyEquivalent (φ.imp φ') (ψ.imp ψ')

def FirstOrder.Language.Theory.semanticallyEquivalentSetoid {L : FirstOrder.Language} {α : Type w} {n : ℕ} (T : L.Theory) : Setoid (L.BoundedFormula α n)

Semantic equivalence forms an equivalence relation on formulas.

Equations

• T.semanticallyEquivalentSetoid = { r := T.SemanticallyEquivalent, iseqv := ⋯ }

theorem FirstOrder.Language.BoundedFormula.semanticallyEquivalent_not_not {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} (φ : L.BoundedFormula α n) : T.SemanticallyEquivalent φ φ.not.not

theorem FirstOrder.Language.BoundedFormula.imp_semanticallyEquivalent_not_sup {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} (φ : L.BoundedFormula α n) (ψ : L.BoundedFormula α n) : T.SemanticallyEquivalent (φ.imp ψ) (φ.not ⊔ ψ)

theorem FirstOrder.Language.BoundedFormula.sup_semanticallyEquivalent_not_inf_not {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} (φ : L.BoundedFormula α n) (ψ : L.BoundedFormula α n) : T.SemanticallyEquivalent (φ ⊔ ψ) (φ.not ⊓ ψ.not).not

theorem FirstOrder.Language.BoundedFormula.inf_semanticallyEquivalent_not_sup_not {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} (φ : L.BoundedFormula α n) (ψ : L.BoundedFormula α n) : T.SemanticallyEquivalent (φ ⊓ ψ) (φ.not ⊔ ψ.not).not

theorem FirstOrder.Language.BoundedFormula.all_semanticallyEquivalent_not_ex_not {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} (φ : L.BoundedFormula α (n + 1)) : T.SemanticallyEquivalent φ.all φ.not.ex.not

theorem FirstOrder.Language.BoundedFormula.ex_semanticallyEquivalent_not_all_not {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} (φ : L.BoundedFormula α (n + 1)) : T.SemanticallyEquivalent φ.ex φ.not.all.not

theorem FirstOrder.Language.BoundedFormula.semanticallyEquivalent_all_liftAt {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} (φ : L.BoundedFormula α n) : T.SemanticallyEquivalent φ (FirstOrder.Language.BoundedFormula.liftAt 1 n φ).all

theorem FirstOrder.Language.Formula.semanticallyEquivalent_not_not {L : FirstOrder.Language} {T : L.Theory} {α : Type w} (φ : L.Formula α) : T.SemanticallyEquivalent φ φ.not.not

theorem FirstOrder.Language.Formula.imp_semanticallyEquivalent_not_sup {L : FirstOrder.Language} {T : L.Theory} {α : Type w} (φ : L.Formula α) (ψ : L.Formula α) : T.SemanticallyEquivalent (φ.imp ψ) (φ.not ⊔ ψ)

theorem FirstOrder.Language.Formula.sup_semanticallyEquivalent_not_inf_not {L : FirstOrder.Language} {T : L.Theory} {α : Type w} (φ : L.Formula α) (ψ : L.Formula α) : T.SemanticallyEquivalent (φ ⊔ ψ) (φ.not ⊓ ψ.not).not

theorem FirstOrder.Language.Formula.inf_semanticallyEquivalent_not_sup_not {L : FirstOrder.Language} {T : L.Theory} {α : Type w} (φ : L.Formula α) (ψ : L.Formula α) : T.SemanticallyEquivalent (φ ⊓ ψ) (φ.not ⊔ ψ.not).not