∀**x True(x) ↔ φ(x) **is fulfilled by the satisfaction of the Provability predicate on the basis of axioms:

∀**x True(x) ↔ ∃Γ ⊆ FS ∧ Axioms(Γ) Provable(Γ, x)**

Syntactic Consequence (Provability)

A formula ** A** is a syntactic consequence within some formal system

of a set

**Γ**of formulas if there is a formal proof in of

**from the set**

*A***Γ**.

**Γ ⊢**≡

_{}A**∃Γ ⊆ FS Provable(Γ, A)**