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.