Undecidability in diagonalizable algebras
V. Yu. Shavrukov · Journal of Symbolic Logic · 1997
Abstract If a formal theory T is able to reason about its own syntax, then the diagonalizable algebra of T is defined as its Lindenbaum sentence algebra endowed with a unary operator □ which sends a sentence φ to the sentence □φ asserting the provability of φ in T. We prove that the first order theories of diagonalizable algebras of a wide class of theories are undecidable and establish some related results.