 Here is a simple and philosophically useful application of Padoa’s method. Suppose the proof system of \(L\) is Peano Arithmetic and that \(L\) is expanded by the addition of a unary predicate \(Tr\) (for “Gödel number of a true sentence of \(L\)”). Let \(\mathbf{H}\) be the theory consisting of all the sentences (the “Tarski biconditionals”) of the following form: