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](https://mathoverflow.net/questions/29774/derivation-rules-and-godel-theorem/29989#29989).)


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.



Most general formulation of Gödel's incompleteness theorems
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$.


