Defining Tarski’s 1933 ∀x True(x) ↔ φ(x)

Provable explained in using conventional notation:
Logical_consequence#Syntactic_consequence

Direct quote from above Wikipedia link:
A formula A is a syntactic consequence within some formal system FS of a set Γ of formulas if there is a formal proof in FS of A from the set Γ.
ProvableFS (Γ, A)  // Paraphrase of Γ ⊢FS A

In other words: Formula A is Provable within Formal System FS if there exists an inference chain (connected sequence of WFF) from a set of Formula Γ to Formula A.

Furthermore if Γ are axioms of FS, then Provable(Γ, A) ≡ True(A) in FS:
TrueFS(A) ≡ ProvableFS (Γ, A)    
FalseFS(A) ≡ ProvableFS (Γ, ~A) 

Last paragraph copyright 2017 Pete Olcott