Axiom 1 says that an atomic sentence of the language of Peano arithmetic is true if and only if it is true according to the arithmetical truth predicate for this language \((Tr_0\) was defined in Section 3.1). Axioms 2–6 claim that truth commutes with all connectives and quantifiers. Axiom 5 says that a universally quantified sentence of the language of arithmetic is true if and only if all its numerical instances are true.  \(Sent_{PA}(\forall v{\scriptsize A})\) says that \({\scriptsize A}(v)\) is a formula with at most \(v\) free (because \(\forall v{\scriptsize A}(v)\) is a sentence).