Beth Definability (Corollary 7.5)

def PDL.Formula.impDef (φ : Formula) (p : ℕ) : Prop

Implicit determination of a propositional letter by agreement of all two-letter substitutions.

Equations

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

def PDL.Formula.expDef (ψ : Formula) (p : ℕ) (φ : Formula) : Prop

An explicit definition using the original vocabulary with the defined letter removed.

Equations

• ψ.expDef p φ = (ψ.voc ⊆ φ.voc \ {Sum.inl p} ∧ PDL.vDash.SemImplies φ (((PDL.Formula.atom_prop p).and ψ.neg).neg.and (ψ.and (PDL.Formula.atom_prop p).neg).neg))

theorem PDL.beth {p : ℕ} (φ : Formula) (h : φ.impDef p) : ∃ (ψ : Formula), ψ.expDef p φ

For any implicit definition there exists an explicit one.