Theorems · Definition · logic and foundations

FirstOrder.Language.Theory.Iff

{L : FirstOrder.Language} → {α : Type w} → {n : ℕ} → 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.)

Defined in

Mathlib.ModelTheory.Equivalence

Cited by

32 results in Mathlib

Foundations

Depth 22 from the axioms · uses no axioms