Beth Definability (Corollary 7.5)

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

Equations

• φ.impDef p = ∀ (p0 p1 : ℕ), repl_in_F p (·p0) φ⋀repl_in_F p (·p1) φ⊨~(·p0⋀~·p1)⋀~(·p1⋀~·p0)

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

Equations

• ψ.expDef p φ = (ψ.voc ⊆ φ.voc \ {Sum.inl p} ∧ φ⊨~(·p⋀~ψ)⋀~(ψ⋀~·p))

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

For any implicit definition there exists an explicit one.