Iff — Mathlib

English

Two bounded formulas φ, ψ are semantically equivalent over T if they have the same interpretation in every model of T.

Русский

Две ограниченные формулы φ и ψ семантически эквивалентны относительно теории T, если во всех моделях T они имеют одинаковую интерпретацию.

LaTeX

$$$T \\models^\\text{bounded} (φ \\iff ψ)$$$

Lean4

/-- 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.) -/
protected def Iff (T : L.Theory) (φ ψ : L.BoundedFormula α n) : Prop :=
  T ⊨ᵇ φ.iff ψ

Похожие утверждения