Fulfilling Tarski’s ∀x True(x) ↔ φ(x)

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)