Are theorems in a mathematical theory effectively checkable?

Question

I wonder whether it is possible to effectively check whether some theorem of a mathematical theory (for example group theory) is provable from axioms of that theory. I know that in propositional logic and for example Hilbert's axiomatic system, it is possible to effectively check whether a theorem follows from it's premises/axioms. I also know that in 20th century there were efforts in mathematics to formalize mathematics (maybe so that it would be possible to effectively check whether a theorem follows from axioms of the theory?). Let's say I want to check by a computer whether a theorem follows from axioms of the group theory. Is it possible to check it by a computer? If so, how is it done?

Answer 1

The answer depends crucially on what objects you are trying to study. First, we fix a theory, say that of Abelian Groups, Graphs, ZFC, etc. Then we can ask if there is a program meeting the following specification:

Given a sentence $\varphi$ in the theory of interest, output either

• a proof of $\varphi$ from the axioms, which tells us that every model satisfies $\varphi$

• a model $\mathfrak{M}$ which satisfies $\lnot \varphi$, showing that there is no proof of $\varphi$.

This problem is called the Decision Problem for $T$, since it decides if a formula is provable or not. We say that a program which does the above decides $T$. If such a program exists, then we say $T$ is decidable, and if no such program exists, then $T$ is undecidable.

As I said, trying to determine if a theory is decidable or not is a fairly delicate field of study. One thing you should know before starting is that efficient algorithms are fairly hard to come by. A lot of decision procedures, when they exist, are doubly exponential in runtime.

---

For convenience, here is a quick selection of some results in this area:

• The theory of Groups is undecidable
• The theory of Abelian Groups is decidable
• The theory of $(\mathbb{Q}, <)$ is decidable
  • More generally, any theory admitting Quantifier Elimination is decidable
• The theory of $(\mathbb{N}, +)$ is decidable
• The theory of $(\mathbb{N}, \times)$ is decidable
• The theory of $(\mathbb{N}, +, \times)$ is undecidable
  • More generally, any theory powerful enough to "do logic" inside of it is undecidable. This is basically the first incompleteness theorem
• The theory of Graphs is undecidable
• The theory of Graphs is decidable if we restrict attention to $\forall^*\exists^*$ formulas

---

Some useful references might be this wikipdedia page, as well as

• Rabin's "Decidable theories"
• Tarski, Mostowski, and Robinson's "Undecidable theories"
• Ferrante and Rackoff's "The computational complexity of logical theories"

---

I hope this helps ^_^