Why is Q (Robinson arithmetic) both undecidable and axiomatizable?

I'm studying computability and its terminology is very confusing. So, Q (Robinson arithmetic) is undecidable AND axiomatizable, right?

But if axiomatizable means that the collection of Q theorems is decidable, that is, we can decide/know which wffs are axioms, then why the theory itself is undecidable? Do we have undecidable wffs that are not axioms? If so, what does that mean?

I think I'm not sure about the distinction between axioms and the collection of theorems of a certain theory, which I know is very basic, but too subtle for me.

Solution 1:

First: The difference between axioms and theorems is this: Axioms are given statements that reflect elementary truths that we suppose to be true of some domain. For example, $\forall x \ x+0=x$ is one of the axioms of Robinson Arithmetic ($Q$), and indeed it expresses some very elementary truth about arithmetic.

A theorem, on the other hand, is some statement we can infer from the axioms. So this is typically something more complicated. For example, we can combine the axioms $\forall x \ x+0=x$ and $\forall x \forall y \ x + s(y) = s(x+y)$ to infer the theorem that $\forall x \ x + s(0) = s(x)$.

There are a few different sets of axioms for Robinson arithmetic, but the idea is that there are only a limited number of axioms. The Robinson Arithmetic Wikipedia page shows $7$ axioms for $Q$.

Now, the theory of $Q$ is the set of all theorems, i.e. all the statements that you can infer from the axioms. I think you can easily see that there are infinitely many theorems.

A set of statements being decidable means that there is some systematic algorithm that can decide, given any statement, whether it is a member of that set or not.

Note that any finite set of statements is intuitively decidable: for any given statement, we can simply compare it, one by one, with the finite set of statements and see if they match: we will either get a match or, after some finite amount of time, find that the statement does not match any of them. So, either way, we get our answer, meaning that the set of statements is decidable.

OK, but what exactly do we mean by decidable? As you will find in your studies on computability, it was Turing who operationalized the notion of systematic algorithms (computations) using his Turing-machines. Thus, be 'decidable' we typically mean 'Turing-machine-decidable'.

Another notion you are likely to run into in your studies on computability is recursiveness. There is a separate definition of what it means for a set to be a recursive set, and as it turns out, a a set is 'decidable' if and only if it is recursive.

A theory being axiomatizable means that there is a limited set of axioms from which all statements in that theory can be derived. By 'limited' we mean 'recursive', i.e. the set of axioms should be a decidable set.

The set of axioms from Q is decidable: given any statement, we can decide whether that statement is one of its axioms. This is because there are only finitely many axioms, and as we already saw, any finite set of statements is decidable.

Still, there can also be infinite sets that are decidable. The Peano Axioms, for example, is an infinite set of statements: besides a small number of axioms that are pretty much the same as $Q$, it also contains an infinite number of instances of an axiom schema called the axiom of induction. The Peano Axioms still are a decidable set though, since it is easy to verify whether some given statement is one of the basic axioms, or an instance of the axiom of induction.

Note that the claim that $Q$ is axiomatizable is a straightforward consequence of the fact that we defined $Q$ to be the set of statements that logically follow from its axioms, and the fact that that set of axioms is finite, and therefore a decidable set of statements.

For the theory of $Q$, things are quite different. Again, note that there are infinitely many theorems of $Q$. Now, as we saw, that does in and of itself not mean that that set is not decidable. But, in this case, infinity does rear its ugly head, and the theory of $Q$ turns out to be undecidable.

Since you're doing computability theory, let's make a connection with the halting problem: you probably already know that the halting problem is undecidable: there is no general algorithm that can always tell, for any given algorithm and input, whether that algorithm is going to eventually halt on that input or not. So: any algorithm on any input is either going to halt or not, but we don't always know whether it does or not.

OK, so now consider the question as whether or not some statement is a statement of the theory of Q. Since Q is axiomatizable, we know that there is an algorithm that, if the given statement is a theorem of Q, the algorithm will eventually say that it is: one such algorithm is to simply go through all possible first-order logic proofs (the set of which is enumerable, so we can indeed go theough those one by one), and see if it is a derivation of that statement starting with the axioms of Q.

Indeed, as such, we can say that theoremhood-of-Q is 'semi-decidable': if some given statement is a theorem of Q, then this algorithm will eventually tell us that that is so. And that is like the halting problem: if some algorithm with a given input will eventually halt, then we will eventually know that as well, simply by running that algorithm on that input.

However, what if this algorithm gets as input a statement that is not a theorem of Q? Then there exists of course no such proof, and that algorithm will never stop. And if it never stops, then it also does not tell us that it isn't a theorem, i.e. it is not a theorem, but we don't know that it is not a theorem. Of course, if we would know that the algorithm would never stop, then we would have our answer (answer: it is not a theorem), but we already know that we can't always know whether some algorithm will halt or not.

Ok, so that's the intuitive connection. Pleas note that this is not a proof that Q is not decidable: maybe there is some other algorithm that can tell for any theorem that it is a theorem and for any non-theorem that it is not a theorem... but as it turns out, there isn't: deciding whether or not something is a theorem turns out to be just as difficult as deciding whether some algorithm halts or not.