A note on the diagonalizable algebras of PA and ZF (Q685077)

If a formal theory \(T\) is strong enough to formalize its own syntax, then the diagonalizable algebra of \(T\) is defined to be the Lindenbaum sentence algebra of \(T\) endowed with a unary operator \(\square\) induced by the Gödel provability predicate of \(T\). The paper under review shows that the diagonalizable algebras of PA and ZF, as well as those of many other pairs of theories differing considerably in strength, are not isomorphic. The proof exploits the difference between the collections of provably recursive functions of the two theories and utilizes the existence of nonspeedable recursive functions.