We define a language for second-order arithmetic using the (positive) connectives ∧ and ∨, the (positive) quantifiers ∀ and ∃, and with negation ‘pushed to the atoms’ under the form of atomic formula t[esdot ]u, t≠u, t∈X, t∈X where t and u stand for first-order terms and X for a second-order variable.

We define and study the translation from this language to the more usual implicational language containing the entailment connective →. We also study the converse translation. Next we define the appropriate notion of syntactical truth predicate for this language (such a notion has been introduced for the implicational language in Colson and Grigorieff (1998)). We establish using the previous translations that the existence of such a predicate for this language is equivalent to the the existence of such a predicate for the implicational language. This result is established in a predicative formal system. We conclude by discussing some elementary attempts to construct such a truth predicate by a fixed point technique.