Let our structure be $(\mathbb{N};+,\times,0,1,<)$. From that structure, Kurt Godel constructed a sentence which has two meanings, a straight-forward number-theoretical meaning, and a higher-level self-referential meaning which basically says, "I am not provable in Peano Arithmetic". But, is there a rigorous definition somewhere of a number-theoretical statement which is self-referential? For example, we can all agree that "$5$ is a prime number" is not self-referential. So, has anyone proposed a formal definition of the intuitive concept of self-referential statement? Or, is this another of those things which is "you know it when you see it"?
Logic – Is There a Formal Definition of a Self-Referential Number Theoretical Statement?
foundationsincompletenesslogicproof-theory
Related Solutions
The usual way that we prove that each sentence $\phi$ is either true or false in a model $M$ is by induction on the structure of $\phi$. So we prove it first for the case where $\phi$ is an atomic formula, then we prove that the property is preserved when we build more complicated sentences with logical connectives and quantifiers.
However, if we say that a sentence is provably true we mean that there is some theory $T$ such that the sentence is provable in $T$. The theory is often part of the context of an argument. Usually, because of the incompleteness theorem, the theory $T$ will not be able to prove true every sentence that happens to hold in some arbitrary model of $T$. So for example, there are sentences of arithmetic (with quantifiers) that are true in the standard natural numbers, but are not provably true in Peano arithmetic. It is the case that every sentence in that language is either true or false in the standard model of arithmetic, but it is not the case that every sentence is provably true or provably false in Peano arithmetic.
There is a standard triviality that forces us to worry about the theory $T$. If we take a sentence $\phi$ that is true in some (at least one) model $M$, then there is a consistent theory in which $\phi$ is provably true: the theory consisting of all sentences that are true in $M$. Therefore, we see that the property of being "provably true" is really a relationship between a sentence and a theory, rather than an intrinsic property of a sentence itself.
Is it possible to deduce Godel's first incompleteness theorem from Chaitin's incompleteness theorem?
Gödel's incompleteness theorem, in its modern form using Rosser's trick, only requires that (beyond being effective and sufficiently strong), the theory must be consistent. There is no requirement that the theory has to be $\omega$-consistent or meet any soundness assumption beyond simple consistency. You cannot apply Chaitin's theorem in its usual form to these theories, in general, because the usual form of Chaitin's theorem assumes more (e.g. many proofs of Chaitin's theorem assume as an extra soundness assumption that the theory only proves true statements.)
Many of the "alternate proofs" also require stronger assumptions than the standard proof of the incompleteness theorem. You have to be very careful when reading about this to check which assumptions are included in each theorem.
In the particular proof of Chaitin's theorem presented by Kritchman and Raz, however, they do not need to assume any particular soundness beyond just consistency. I am going to explain this in detail.
They do need to assume that $T$ is sufficiently strong. In particular, they assume that if $n$ and $L$ satisfy $K(n) < L$, then $T \vdash \hat K(\dot n) < \dot L$. Here $\dot n$ and $\dot L$ are terms of the form $1 + 1 + \cdots + 1$ corresponding to $n$ and $L$, and $\hat K$ is a formula of arithmetic defined directly from the definition of $K$. (Note that the set of pairs $(n,L)$ with $K(n) < L$ is recursively enumerable, so there is no real issue in assuming $T$ proves all true sentences of that form.)
Given the assumption on $T$, their proof goes as follows (rephrased in more precise terms):
Begin proof
Given $L$, we can make a program $e_L$ that does the following:
Search for any $n$ such that $T \vdash \hat K (\dot n) > \dot L$. We do this by searching through all $T$-proofs in an exhaustive manner.
Output the first such $n$ we find, if we ever find one.
Because we can code $L$ into the program as a fixed constant, using the standard coding methods, the length $|e_L|$ of $e_L$ no worse than $2\log(L) + C$ for some constant $C$. In particular, we can fix an $L$ with $|e_L| < L$. Assume such an $L$ is fixed.
For this $L$, suppose $e_L$ returns a value, $n$. Then $K(n) \leq |e_L| < L$. By our assumption that $T$ is sufficiently strong, this means $T$ proves $\hat K (\dot n) < \dot L$.
But if $e_L$ returns $n$ then $T$ also proves $\hat K(\dot n) > \dot L$. This means that if $e_L$ returns a value then $T$ is inconsistent. So, if we assume $T$ is consistent, then $e_L$ cannot return a value. This means that, for our fixed $L= L_T$, $T$ cannot prove $\hat K(\dot n) > \dot L$ for any $n$.
Thus, if we take $n = n_T$ to be such that $K(n) > L$, we have that $\hat K (\dot n) > \dot L$ is a true statement that is not provable in $T$.
End proof
This proof just given (in italics) proves:
If $T$ is a consistent, effective theory of arithmetic that proves every true formula of the form $\hat K(\dot n) < \dot L$, then there is a true statement of the form $\hat K(\dot n) > \dot L$ that is not provable in $T$.
This is almost the same as Gödel's incompleteness theorem. The only difference is that the usual proof of the incompleteness theorem gives us an explicit formula that it is true but not provable in $T$ (namely, the Rosser sentence of $T$). On the other hand, the proof in italics requires us to find $n_T$ in order to have an explicit example, and there is no algorithm to do this.
This is one motivation for what I think of as the "standard form" of Chaitin's theorem. In that form, we look instead for unprovable sentences of the form ($\dagger$): $(\exists x)[\hat K(x) > \dot L]$.
Because we can compute $L= L_T$, we can compute a specific sentence of that form for $T$. But, for the proof to work, we need to have an actual $n$ such that $T \vdash \hat K(\dot n) > \dot L$. So we have to add an additional soundness assumption to the theorem, namely that if $T$ proves a sentence of the form ($\dagger$) then there is an $n$ such that $T$ proves $\hat K(\dot n) > \dot L$.
Overall, in this version of Chaitin's theorem, we have an explicit sentence, but with a stronger soundness assumption. The proof of Gödel's incompleteness theorem using Rosser's method gives us an explicit sentence without any stronger soundness assumption.
Best Answer
I think this is a great question! My personal take would be that there is no fully satisfying formalization yet known, but there also is no convincing argument yet that no such formalization can exist. Incidentally, I strongly recommend the books Diagonalization and self-reference (Smullyan) and Self-reference and modal logic (Smorynski) if you can get your hands on them (they're hard to find).
(For a variety of reasons I'm going to work over a theory - namely first-order Peano arithmetic $\mathsf{PA}$, although the details won't matter - rather than a structure; basically, this is Godelian rather than Tarskian, and is ultimately in my opinion the right way to set things up.)
Let's start with the following naive notion:
(Note that I'm choosing a specific Godel numbering here. We could also vary the numbering, and the question of what a "Godel numbering" really is is a great one, but to me that's a separate question so I'm punting for now.)
Now naive self-referentiality has the nice property of being perfectly formal. However, it's also pretty boring: just take as our choice of $\varphi$ the formula $\tau_n(x)=$ "$x$ is the Godel number of a true $\Sigma_n$ sentence" for some sufficiently large $n$. (This doesn't contradict Tarski, since a different $\tau_n$ is needed for different $n$s. Tarski just rules out a single $\tau$ doing the job for all $n$.) $\mathsf{PA}$ proves the "deflation scheme" $\eta\leftrightarrow\tau_n(\underline{\ulcorner\eta\urcorner})$ whenever $\eta$ is $\Sigma_n$, so this works.
So naive self-referentiality joins the long list of natural-at-first-but-actually-SUPER-BORING ideas in logic. But beating dead horses is great exercise, so let's not stop there. I think that naive self-referentiality is actually unsatisfying for an even deeper reason!
Specifically, I would argue the informal interpretation of $\theta$ as being (rather than merely behaving as) the natural-language sentence "I am $(\Sigma_n$-)true" is not justified by the mere fact that $$(*)\quad\mathsf{PA}\vdash\theta\leftrightarrow\tau_n(\underline{\ulcorner\theta\urcorner}).$$ This is because lots of other sentences also satisfy $(*)$ in place of $\theta$ - namely, any other sentence of the same (or lesser) syntactic complexity. So it seems that information is lost when we choose to construe $\theta$ as self-referential on the basis of $\tau_n$ (for sufficiently large $n$) alone.
Interestingly, a "dual" of this objection can be levied against the Godel sentence itself! This is because it turns out to be $\mathsf{PA}$-provably-equivalent to $\mathsf{Con(PA)}$, and $\mathsf{Con(PA)}$ (I would argue) doesn't have any compelling self-referential character. These two objections together motivate (in my opinion) a strengthening of naive self-reference: informally, say that $\theta$ is irreducibly self-referential iff for some $\varphi$ there is no $\mathsf{PA}$-meaningful difference between being $\theta$ and being a $\varphi$-fixed-point. The precise definition can be found at this old question of mine, asking whether the notion is in fact nontrivial. Sadly, that question is open, and the initial optimism I had has long since faded: I now suspect that either every sentence is irreducibly self-referential, or only the $\mathsf{PA}$-decidable sentences are irreducibly self-referential, and neither of these options is interesting.
Going back to naive self-reference, we could shift attention to the set of ways that a given sentence is naively self-referential instead of the simple yes/no question "is there naive self-reference at all." Specifically, for $\theta$ a sentence let $$\mathsf{NSR}(\theta)=\{\varphi: \theta\mbox{ asserts its own $\varphi$-ness}\}.$$ Maybe some $\theta$s have "larger" $\mathsf{NSR}$s than others; conversely, we could try to "weight" elements of $\mathsf{NSR}(\theta)$ based on how uniquely they pin down $\theta$ (e.g. $\tau_n\in\mathsf{NSR}(\theta)$ whenever $\theta\in\Sigma_n$, so $\tau_n$ should carry little weight in this sense). At the very least, we could look for interesting structural comparisons here. As far as I know, this is largely unexplored. But even if there's something interesting here, note that we would be unlikely to get a clean divide between "self-referential" and "non-self-referential" - rather, we'd more likely see a spectrum of possibilities. I've asked a question which can be thought of as a naive first step in this direction at MathOverflow.