Equivalence of Formulas

Main Definitions

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

TODO

• Define the quotient of L.Formula α modulo ⇔[T] and its Boolean Algebra structure.

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

φ ⟹[T] ψ indicates that φ implies ψ in models of T.

Equations

• T.Imp φ ψ = T ⊨ᵇ φ.imp ψ

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

φ ⟹[T] ψ indicates that φ implies ψ in models of T.

Equations

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

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

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

Equations

• ⋯ = ⋯

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

instance FirstOrder.Language.Theory.Imp.instIsTransBoundedFormula {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} : IsTrans (L.BoundedFormula α n) T.Imp

Equations

• ⋯ = ⋯

theorem FirstOrder.Language.Theory.bot_imp {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} (φ : L.BoundedFormula α n) : T.Imp ⊥ φ

theorem FirstOrder.Language.Theory.imp_top {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} (φ : L.BoundedFormula α n) : T.Imp φ ⊤

theorem FirstOrder.Language.Theory.imp_sup_left {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} (φ : L.BoundedFormula α n) (ψ : L.BoundedFormula α n) : T.Imp φ (φ ⊔ ψ)

theorem FirstOrder.Language.Theory.imp_sup_right {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} (φ : L.BoundedFormula α n) (ψ : L.BoundedFormula α n) : T.Imp ψ (φ ⊔ ψ)

theorem FirstOrder.Language.Theory.sup_imp {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} {φ : L.BoundedFormula α n} {ψ : L.BoundedFormula α n} {θ : L.BoundedFormula α n} (h₁ : T.Imp φ θ) (h₂ : T.Imp ψ θ) : T.Imp (φ ⊔ ψ) θ

theorem FirstOrder.Language.Theory.sup_imp_iff {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} {φ : L.BoundedFormula α n} {ψ : L.BoundedFormula α n} {θ : L.BoundedFormula α n} : T.Imp (φ ⊔ ψ) θ ↔ T.Imp φ θ ∧ T.Imp ψ θ

theorem FirstOrder.Language.Theory.inf_imp_left {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} (φ : L.BoundedFormula α n) (ψ : L.BoundedFormula α n) : T.Imp (φ ⊓ ψ) φ

theorem FirstOrder.Language.Theory.inf_imp_right {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} (φ : L.BoundedFormula α n) (ψ : L.BoundedFormula α n) : T.Imp (φ ⊓ ψ) ψ

theorem FirstOrder.Language.Theory.imp_inf {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} {φ : L.BoundedFormula α n} {ψ : L.BoundedFormula α n} {θ : L.BoundedFormula α n} (h₁ : T.Imp φ ψ) (h₂ : T.Imp φ θ) : T.Imp φ (ψ ⊓ θ)

theorem FirstOrder.Language.Theory.imp_inf_iff {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} {φ : L.BoundedFormula α n} {ψ : L.BoundedFormula α n} {θ : L.BoundedFormula α n} : T.Imp φ (ψ ⊓ θ) ↔ T.Imp φ ψ ∧ T.Imp φ θ

def FirstOrder.Language.Theory.Iff {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.Iff φ ψ = 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.iff_iff_imp_and_imp {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} {φ : L.BoundedFormula α n} {ψ : L.BoundedFormula α n} : T.Iff φ ψ ↔ T.Imp φ ψ ∧ T.Imp ψ φ

theorem FirstOrder.Language.Theory.imp_antisymm {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} {φ : L.BoundedFormula α n} {ψ : L.BoundedFormula α n} (h₁ : T.Imp φ ψ) (h₂ : T.Imp ψ φ) : T.Iff φ ψ

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

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

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

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

Equations

• ⋯ = ⋯

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

instance FirstOrder.Language.Theory.Iff.instIsSymmBoundedFormula {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} : IsSymm (L.BoundedFormula α n) T.Iff

Equations

• ⋯ = ⋯

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

instance FirstOrder.Language.Theory.Iff.instIsTransBoundedFormula {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} : IsTrans (L.BoundedFormula α n) T.Iff

Equations

• ⋯ = ⋯

theorem FirstOrder.Language.Theory.Iff.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.Iff φ ψ) {v : α → M} {xs : Fin n → M} : φ.Realize v xs ↔ ψ.Realize v xs

theorem FirstOrder.Language.Theory.Iff.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.Iff φ ψ) {v : α → M} : φ.Realize v ↔ ψ.Realize v

theorem FirstOrder.Language.Theory.Iff.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.Iff φ ψ) : M ⊨ φ ↔ M ⊨ ψ

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

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

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

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

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

Semantic equivalence forms an equivalence relation on formulas.

Equations

• T.iffSetoid = { r := T.Iff, iseqv := ⋯ }

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

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

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

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

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

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

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

theorem FirstOrder.Language.BoundedFormula.inf_not_iff_bot {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} (φ : L.BoundedFormula α n) : T.Iff (φ ⊓ φ.not) ⊥

theorem FirstOrder.Language.BoundedFormula.sup_not_iff_top {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} (φ : L.BoundedFormula α n) : T.Iff (φ ⊔ φ.not) ⊤

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

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

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

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