∀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 A from the set Γ.
Γ ⊢ A ≡ ∃Γ ⊆ FS Provable(Γ, A)