 No restrictions are placed on what form the axioms, rules and therefore theorems of a formal system are to be. Truth for elementary propositions of a formal system consists simply in their provability in the system. One of his formal systems (Example 7, p. 23) has only one predicate “a unary predicate expressed by Gödel by the words ‘ist beweisbar’” (p. 23), i.e., a provability predicate. The elementary truths of this system can be interpreted as claims about provability in the underlying system. Any formal system of the usual sort could be ‘reduced’ into one in which there is only one provability predicate and truth (= provability) in the reducing system of the elementary proposition \(\vdash \langle \phi \rangle\) holds only when \(\phi\) is provable in the reduced system (pp. 34–35). Curry allows that one can form compounds from elementary propositions by means of the usual logical operators in order to express complex propositions in the language of proof theory (Chapter IX).