What is some easy illustrative example of an non-recursive formal system and recursive formal system?

Question

I have a difficulty to relate recursion in to formal systems. Would you please show me some easy example (like for example MU-system) of a recursive formal system and non-recursive formal system so that I could understand what the word recursive means in a context of formal systems? Thank you.

Answer 1

It will help, I think, to consider incorrect versions of Godel's incompleteness theorem.

The naive statement of GIT, which one often hears, is

There is no complete consistent theory.

(I'm replacing "formal system" by "theory," by which I mean "first-order theory," here. I'm also going to use "computable" instead of "recursive" below - they're synonyms, and I think the former is more intuitively parsed.)

This is of course bunk, for two reasons. The uninteresting reason is that there are some very simple systems out there; for example, the theory of real closed fields.

The natural response to this is to look at systems which can actually "do something," and this gives us

There is no complete consistent formal system which can do basic arithmetic.

Let's leave the italicized phrase imprecise for a moment, since it's not what I want to focus on; if you like, you can replace this with "contains Peano arithmetic" for simplicity.

This is still false, for one simple reason:

Given a structure $M$, let $Th(M)$ be the set of all sentences true of $M$. Then for any structure $M$, the theory $Th(M)$ is complete and consistent.

This is an immediate consequence of the definition of truth in first-order logic.

• Incidentally, the converse holds too: a consistent theory $T$ is complete iff it is of the form $Th(M)$ for some structure $M$. Of course, we can have $Th(M)=Th(M')$ (when this happens we say $M,M'$ are elementarily equivalent and write "$M\equiv M'$") even when $M$ and $M'$ are significantly different - look into the Lowenheim-Skolem and Compactness theorems for this.

The relevance of this observation is that it kills the second naive version of GIT above: in particular $Th(\mathcal{N})$ extends PA (where $\mathcal{N}$ is the standard model of arithmetic $(\mathbb{N};+,\times,0,1,<)$).

The point is that this is in some sense cheating: we haven't whipped up a complete consistent extension of PA in any "concrete" way. GIT only applies to theories which are "reasonably simple," and one correct version of GIT is:

There is no complete consistent theory which can do basic arithmetic and has a computable set of axioms.

That is, there are four desirable properties of a formal system which GIT is saying are fundamentally incompatible: consistency, completeness, power, and simplicity. The importance of the simplicity of the theory will become clear when you read the proof, but briefly it's because we want the theory to be able to prove things about itself, and that requires the theory to be reasonably concrete.