Most general formulation of Gödel's incompleteness theorems

Question

Modern statements of Gödel's incompleteness theorems are usually in terms of first-order predicate logic. However, I've often read the claim that they extend to arbitrary formal systems that can prove basic propositions about numbers. Indeed, according to Wikipedia, the original theorems referred to the type theory of Principia Mathematica, which is apparently not based on predicate logic.

My two questions are:

1. What is the most general concept/definition of a formal system for which Gödel's theorems have been stated?
2. How does their proof differ from the predicate logic variant?

Regarding 1., I could imagine several equally general definitions, for example based on either strings of symbols or abstract syntax trees. Being a little biased, I actually think of formal systems as data structures of more or less arbitrary computer programs, so maybe there is a definition based on Turing machines... In any case, it would need to specify what a "proof" of a "theorem" is, but I would like to do without the concept of "axioms." (See also Derivation rules and Godel theorem.)

Regarding 2., I'm specifically thinking about the diagonal lemma (or arithmetic fixed-point theorem, or whatever it is really called). The version I know refers to a "formula with one free variable," but that presupposes such concepts as "formula" and "free variable" in the formal system, and I'm wondering how to generalize that to arbitrary formal systems. I know there are proofs of the first incompleteness theorem which take an entirely different route, but AFAIK they don't carry over to the second incompleteness theorem.

I would like to add that I don't doubt the generality of Gödel's incompleteness theorems in any way. I just feel there is a gap between their claimed general nature and the way they are usually presented. A year ago, I devised a nonstandard formal system for a proof assistant. Although it could easily formalize its own concepts and express its own consistency, a translation of Gödel's incompleteness theorems from predicate logic turned out to be surprisingly nontrivial.

Answer 1

Raymond Smullyan gave a very general formulation in terms of representation systems. They appear in his "Theory of Formal Systems", and in the first and last chapters of "Godel's Incompleteness Theorems". They generalise first- and higher-order systems of logic, type theories, and Post production systems.

A representation system consists of:

1. A countably infinite set $E$ of expressions.

2. A subset $S \subseteq E$, the set of sentences.

3. A subset $T \subseteq S$, the set of provable sentences.

4. A subset $R \subseteq S$, the set of refutable sentences.

5. A subset $P \subseteq E$, the set of (unary) predicates.

6. A function $\Phi : E \times \mathbb{N} \rightarrow E$ such that, whenever $H$ is a predicate, then $\Phi(H,n)$ is a sentence.

The system is complete iff every sentence is either provable or refutable. It is inconsistent iff some sentence is both provable and refutable.

We say a predicate $H$ represents the set $A \subseteq \mathbb{N}$ iff $A = \{ n : \Phi(H,n) \in T \}$.

Let $g$ be a bijection from $E$ to $\mathbb{N}$. We call $g(X)$ the Godel number of $X$. We write $E_n$ for the expression with Godel number $n$.

Let $\overline{A} = \mathbb{N} \setminus A$ and $Q^* = \{ n : \Phi(E_n,n) \in Q \}$.

We have:

1. (Generalised Tarski Theorem) The set $\overline{T^*}$ is not representable.

2. (Generalised Godel Theorem) If $R^*$ is representable, then the system is either inconsistent or incomplete.

3. (Generalised Rosser Theorem) If some superset of $R^* $ disjoint from $T^*$ is representable, then the system is incomplete.

In case it's not clear: in a first-order system, we can take $P$ to be the set of formulas whose only free variable is $x_1$, and $\Phi(H,n) = [\overline{n}/x_1]H$.

Answer 2

Theories can be be represented recursion-theoretically by an encoding of the language as natural numbers (most simply, a bijective encoding, which I assume), and a Turing machine that accepts all and only theorems. Theories defined in terms of a Hilbert system will then be either recursive or partial-recursive sets.

It's easy to formalise the idea of such a language having a provability predicate: it's a predicate with a free variable for which the instantiation of that formula with each natural number is accepted iff the formula corresponding to that number is accepted. Theories that have such a predicate are self-descriptive. If you can formalise a substitution operator, you can diagonalise on this predicate. You get four interesting classes (among others) of theory:

1. For inconsistent theories, any predicate will do as a self-description predicate (always accept), and any binary function will do as a substitution function;
2. Regular completeable theories are not self-descriptive;
3. Self-verifying theories have self-description operators, but not substitution operators, and accept the sentence asserting their own consistency;
4. Goedel-incomplete theories have both self-description operators and substitution operators, and do not accept the sentences asserting their consistency and inconsistency.

Observe that these definitions are generalisable in an important sense: you can extend to notions of hypercomputation, by using oracle Turing machines, allowing "theories" that are sets that are not recursive or partial recursive. The treatment can be generalised in other ways, such as to the second-order concept of mass problems, which is where I learned about this way of looking at incompleteness.

Note though, that the formalisation here of self-descriptive, susbtitution function, and consistency sentence are still dependent on the language of predicate logic. Loking at provability logic might offer a way to generalise this still further.

Answer 3

The general understanding is that if a system is expressive enough to do arithmetic (say, Robinson arithmetic) then Gödel's theorem applies. A computability view would be, if a system can represent all the computable functions, then Gödel's theorem applies. The crucial link here is that arithmetic is enough to represent all the computable functions.

This syllabus gives a great short proof of Gödel's theorem, and the introductory text could help.

Hope this helps.