Recognition complexity of theories and their computational expressivity (Q694245)

The computational complexity of a first-order theory is the difficulty to prove or disprove a formal statement to be true in a given theory. There are decidable theories known to have computational complexities bigger than functions given by towers of exponents. The computational complexity for arbitrary theories of Boolean algebras is discussed. In parallel, a new notion is introduced: computational expressivity. This is the possibility of a theory to simulate long computations, and is a notion that can be applied also for undecidable theories. It is proven that Peano arithmetic has a computational expressivity bigger than Boolean algebras.