A related notion is $\omega$-incompleteness: this is when a theory can prove each of $F(0), F(S0), F(SS0), \dots$ but *can't* prove $\forall x Fx$. Whereas $\omega$-inconsistent theories can *prove the negation* of $\forall x Fx$.

Here I'll mention some further notions that you may encounter when you read about these issues. They aren't necessary for the rest of our discussion here, though.
One kind of quantification we can call *bounded*. We might represent that as $\exists x\lt n. \phi$ or $\forall x\lt n.\phi$, where these are to be understood as abbreviating the following formulas in the language of arithmetic:
> $\exists x (x\lt S^n0 \wedge \phi)$
> $\forall x (x\lt S^n0 \cond \phi)$
Of course, we could have used $\le$ instead of $\lt$.
It's sometimes useful to talk about what can be arithmetically defined by formulas in the language of arithmetic that use no quantifiers, or if they do use quantifiers, only used them in those "bounded" patterns. These formulas are sometimes said to have quantifier complexity $\Delta$ (or $\Delta_0$). Burgess uses different language; he calls these formulas *rudimentary*.
Now consider formulas that can be put into prenex form (all quantifiers at the front), where they consist of a sequence of zero or more *unbounded* $\exists$s, followed by a formula of complexity $\Delta$. These formulas are sometimes said to have quantifier complexity $\Sigma_1$. Burgess calls them $\exists$-rudimentary. In fact we only need to think about a single unbounded $\exists$; a sequence of more than one will be equivalent to a single unbounded $\exists$ followed by further *bounded* $\exists$s. Note also that $\Delta$ formulas count as $\Sigma_1$, because we allow for the case where there are zero leading unbounded $\exists$s.
Similarly, formulas that in prenex form consist of a sequence of zero or more unbounded $\forall$s, followed by a formula that's of class $\Delta$, are said to have quantifier complexity $\Pi_1$ or to be $\forall$-rudimentary. Here too we really only need to think about a single unbounded $\forall$.
The subscripts in $\Sigma_1$ and $\Pi_1$ are to allow for cases where we have a sequence of zero or more $\forall$s followed by a $\Sigma_1$ formula. That would be a $\Pi_2$ formula; and so on.
Some interesting facts:
* for any $\Delta$ sentence in the language of arithmetic, $Q$ can either prove it or prove its negation
* if a $\Sigma_1$ sentence is true on the standard model of arithmetic, then $Q$ can prove it
* if a $\Pi_1$ sentence can be proved by a consistent extension of $Q$, then it's true on the standard model of arithmetic
There are also interesting relations between these syntactic categories and what kinds of functions and relations can be arithmetically defined in terms of them. I won't pause to explain that, though. You can read Smith or Boolos Burgess and Jeffrey for more details.

## 10 ##
Okay, so now we're in a position to finally talk about Goedel's First Incompleteness Theorem. In popular discussion, there are really three different, closely related but importantly-different-in-the-details theorems here. So we might do better to talk about Goedel's First Incompleteness Triad. And even then, each corner of the triad can be formulated in subtly different ways; and furthermore, what's interesting is not just the Triad itself but all sorts of corollaries that quickly follow from it.
But I will exposit this in terms of a Triad. One of the corners of the Triad is closest to what Goedel strictly speaking proved in 1931.
In the following, I will sometimes talk of an axiomatizable theory. By this you can take me to mean a theory where the set of code numbers of the theory's axioms, for our specified coding scheme, is primitively recursive. Correlates of our results would also hold if the axioms were merely decidable, but that would complicate our discussion. In any event, the only theories we're dealing with have primitively recursive axiomatizations, and I will just call these theories "axiomatizable."
In some cases I'll want to discuss theories that *may* not be axiomatizable in that way, such as true arithmetic. (Indeed we'll see it *isn't* so axiomatizable.) In that event, I'll omit the adjective "axiomatizable." In other cases I'll want to talk more specifically about theories (like our minimal arithmetics $Q$) that are *finitely* axiomatizble.
I'll call the three corners of our Triad **A**, **B**, and **C**. Let's begin with Theorem B. (I'm staying consistent with the labeling I used in class, but am now discussing the corners in a different order.)
>**B**. If $T$ is an axiomatizable theory in the language of arithmetic that is deductively consistent and strong enough to arithmetically define all decidable relations on the numbers, then $T$ is deductively incomplete.
As it turns out, minimal arithmetic and its extensions like Peano arithmetic are strong enough to arithmetically define all (not-necessarily-primitively) recursive relations on the numbers, which we assume is the same as all decidable relations on the numbers. So this theorem says that these theories are, if consistent, deductively incomplete. Hence they fall short of true arithmetic, which by definition includes all the sentences that are true in the standard model of arithmetic.
This theorem is what Smith calls his Theorem 5. He derives it as a quick result from two other theorems:
>Smith-3. If $T$ is an axiomatizable theory in the language of arithmetic that is deductively consistent and deductively complete, then it is decidable whether any given sentence is a theorem of $T$.
(See also Burgess Theorem 15.7) We already know that we can effectively enumerate the consequences of any (at least effectively enumerable) set of premises, so we could decide the question whether a given $\phi$ is a theorem of $T$ just by enumerating the consequences of $T$'s axioms; if $T$ is deductively complete we're guaranteed to eventually see $\phi$ or $\neg\phi$ in the list, and then we can give our answer.
What if $T$ is *in*consistent? Well, in that case too it's easy to decide whether $\phi$ is an axiom. Just always say "yes."
But what if we don't know whether $T$ is consistent or not? This is a good point to get clear on: *it doesn't matter*. When we ask whether we can decide whether some formula belongs to some set, it doesn't matter how the set was described. If it's in fact the set that includes all the wffs in the language, then always saying "yes" is in fact an effective decision procedure for saying whether an arbitrary formula belongs to the set. Even if you don't know, and can't prove, that the way you in fact specified the set is equivalent to the set as specified here. If you want a finer-grained notion of deciding questions, you may well be able to find or develop such. But that is not the way the standard notions that we're working with are understood. To take another example, it is effectively decidable what numbers belong to this set:
> $\set{x\where x~\textrm{is even}\vee \textrm{God exists}}$
If God exists, then the decision procedure is to always say "yes"; if God doesn't exist, then the decision procedure is to say "yes" iff the number is even (which is a decidable question). Now *which* of those *is* the decision procedure? I wish I knew. But in either event, there is a decision procedure, which can effectively give the correct answer for any argument $x$ in a finite number of steps. So the set --- whichever set it turns out to be --- is decidable.
In the present context too, we don't need to know or prove anything about whether $T$ is consistent. If it is, then the decision procedure implied by Smith-3 is the more laborious one I described of eumerating all the theorems and seeing which of $\phi$ or $\neg\phi$ appears. If it isn't consistent, then the decision procedure is the easier one of always saying "yes, the formula you're asking about is provable."

The other theorem Smith uses to derive our Goedel Theorem B is:
> Smith-4. If $T$ is an axiomatizable theory in the language of arithmetic that is deductively consistent and strong enough to arithmetically define all decidable relations on the numbers, then $T$ is not decidable.
See Smith sections 7 and 8 for an informal justification for this. (The introduction to Episode 6 is also relevant.)
It follows that **if you have axiomatizable + consistent + strong-enough-to-define-the-decidable, you can't also have complete**. That's what Goedel Theorem B says.
One downside of our Goedel Theorem B is that it doesn't actually construct a sentence that's neither provable nor disprovable. It just tells us that *there is* such a sentence. Also, it's somewhat difficult to get clear on a rigorous understanding of "effectively decidable," and to persuade ourselves that $Q$ and Peano arithmetic are "strong-enough-to-define-the-decidable."
The other two corners of our triad won't have these shortcomings.
Back in section 7, we posited the formula $H$, which was:
> $\forall y. y~\textrm{is the self-application of}~x \cond \neg\,T\textrm{-provable}~y$
Notice that $H$ is a formula with one free variable $x$. We let $G$ be the self-application of $H$ wrt that variable. In effect, $G$ says "I am not provable from $T$".
What Goedel did was (using the term I introduced at the end of section 8) **arithmetize** this construction.
To see how this works, I think it's helpful to separate the relevant notions into three parallel versions. We'll let $Q$ be our relevant $T$; then let's say that:
* $\textrm{is a lexical proof from}~Q~\textrm{of}$ is a relation between a sequence of formulas $\Xi$ and a formula $\phi$, that holds just when $\Xi$ constitutes a proof of $\phi$ from axioms of $Q$.
* $\textrm{is a coded proof from}~Q~\textrm{of}$ is a relation between a code number $\#\Xi$ and a code number $\#\phi$, that holds just the previous relation holds between $\Xi$ and $\phi$. This will be a primitively recursive relation on its numerical arguments.
* Since the previous relation is primitively recursive, it will be arithmetically definable in any theory strong enough to define the primitively recursive. Let $\mathsf{is~a~coded~proof~from}~Q$ be the open formula that defines this in $Q$. Then:
* when $\#\Xi~\textrm{is a coded proof from}~Q~\textrm{of}~\#\phi$, then $Q\proves \mathsf{is~a~coded~proof~from}~Q(S^{\#\Xi}0, S^{\#\phi}0)$
* when not, then $Q\proves \neg\,\mathsf{is~a~coded~proof~from}~Q(S^{\#\Xi}0, S^{\#\phi}0)$
Similarly, let's say that:
* $\textrm{is the lexical self-application of}$ is a relation between a formula $\phi$ and the application of that formula to its own code number. This could be construed in several ways:
* $\phi[x\leftarrow S^{\#\phi}0]$
* $\forall x. x=S^{\#\phi}0 \cond \phi$
* $\exists x. x=S^{\#\phi}0 \wedge \phi$
The literature on Goedel tends to follow the last of these.
* $\textrm{is the coded self-application of}$ is a relation that holds between code numbers $\#\phi$ and $\#\psi$ when the previous relation holds between formulas $\phi$ and $\psi$. This will be a primitively recursive relation on its numerical arguments. Note that Smith and Burgess call this relation $\textrm{diag}$.
* Since the previous relation is primitively recursive, it will be arithmetically definable in any theory strong enough to define the primitively recursive. Indeed, its associated function will be definable in the stronger, functional sense. Let $\mathsf{is~the~coded~self{-}application}$ be the open formula that defines this in $Q$. Then:
* $\#\phi~\textrm{is the coded self-application of}~\#\psi$ iff $Q\proves \forall y. y=S^{\#\psi}0 \bicond \mathsf{is~the~coded~self{-}application}(S^{\#\phi}0, y)$
At this point, we could define $Q\textrm{-provable}~y$ as $\exists p. \mathsf{is~a~coded~proof~from}~Q(p,y)$, then define $H$ as we did before:
> $\forall y. \mathsf{is~the~coded~self{-}application}(x, y) \cond \neg\exists p. \mathsf{is~a~coded~proof~from}~Q(p, y)$
Smith works instead with the equivalent $U$, which we can understand as:
> $\forall p \forall y. \mathsf{is~the~coded~self{-}application}(x,y) \cond \neg\,\mathsf{is~a~coded~proof~from}~Q(p, y)$
Both of these say, intuitively, that Nothing is a proof of $x$'s self-application. We then apply $U$ to itself, and let $G$ be the result. Now we'll be able to show, as in section 7, that if $Q$ is consistent, then $Q\not\proves G$ and $Q\not\proves\neg G$.
The remaining corners of our First Incompleteness Triad differ in what assumptions they rely on to show this.
One of the corners is the theorem that:
>**A**. If $T$ is an axiomatizable theory in the language of arithmetic that is not merely deductively consistent but *arithmetically sound* (that is, all its axioms are true on the standard model of that language), then $T$ will be deductively incomplete.
In other words, **axiomatizable + arithmetically sound implies incomplete**. This theorem doesn't tell us that *true arithmetic* is incomplete, because it's not axiomatizable. It does tell us that axiomatizable theories like minimal arithmetic and Peano arithmetic are incomplete, if their theorems are subsets of true arithmetic. (The most salient way in which they'd fail to be sound is if they were deductively inconsistent. But being sound is a stronger constraint than merely being consistent.)
This theorem approximates what Smith calls his Theorem 1. See also the refinements in his Theorems 37 and 38.
To prove this theorem, we first construct a Goedel sentence $G$ that concerns provability in $T$. We don't require the relations $\textrm{is a coded proof from}~T~\textrm{of}$ and $\textrm{is the coded self-application of}$ to be arithmetically definable in $T$, but merely in true arithmetic.
Next we establish the lemma that $G$ will be "standardly true" --- that is, true in the standard model of arithmetic --- iff it's not provable from $T$. How? Observe that the lhs of this biconditional requires that for all proof-codes $m$, $\interp{\neg\,\mathsf{is~a~coded~proof~from}~T(S^m0, S^{\#G}0)}_{\script N}$ is $\True$; which given what the embedded formula defines in true arithmetic, will be the case iff no $m$ is the code for a proof from $T$ of $G$. That establishes our lemma.
Then we observe that if $T$ *could* prove $G$, it would (by our lemma) therefore be proving something that's not standardly true --- contradicting the assumption that $T$ is arithmetically sound. So $T$ can't prove $G$, and (again by our lemma) this shows that $G$ *is* standardly true. Hence if $T$ is arithmetically sound, it can't prove $\neg G$ either.
That's all it takes to prove Goedel Theorem A. The hard work is in the construction of $G$, and defending the claim that the relevant notions can be arithmetically defined.
Though it's easy to prove Theorem A, this theorem relies on semantic notions like a theory's being arithmetically sound: its theorems being true in a certain model. So some philosophers (especially around the time Goedel was writing) would be suspicious of it for that reason. The third corner of our triad, on the other hand, only relies on non-semantic notions, and notions that (unlike those used in Theorem B) are entirely rigorous, like the notion of a primitively recursive function. Our theorem here is:
> **C**. If $T$ is an axiomatizable theory that is deductively consistent and extends $Q$ (really, extends any theory of arithmetic strong enough to arithmetically define all primitively recursive relations; $Q$ is such a theory), then there will be a "Goedel sentence" $G$ such that $T\not\proves G$, and also (unless $T$ is $\omega$-inconsistent) $T\not\proves \neg G$.
Simplifying, this says that **axiomatizable + consistent + strong-enough-to-define-the-primitively-recursive implies incomplete**. This is what Burgess calls Theorem 17.9. (His Theorem 17.7 approximates our Theorem B and Theorem C in different ways.) Theorem C approximates what Smith calls his Theorem 2; see also the refinements in his Theorems 44, 45, and 48.
This is what Goedel historically proved. He didn't talk about $Q$, which hadn't at that point yet been formulated, but merely about theories being strong-enough-to-define-the-primitively-recursive.
A few years later Rosser came up with a more complicated sentence (the Rosser sentence, that says "For any proof of me, there's an earlier proof of my negation"), that has the advantage of allowing us to remove the hedge about $\omega$-consistency, and just rely on $T$'s merely being consistent. But it has the disadvantage of being harder to think about. So I'll just continue using the Goedel sentence.
First, we construct our sentence $G$, concerning provability in $Q$ and where the relevant relations are arithmetically definable in $Q$.
Next, let's persuade ourselves that $Q\not\proves G$. Suppose for reductio that $Q$ did prove $G$. That is:
(i) $Q\proves \forall p \forall y. \mathsf{is~the~coded~self{-}application}(S^{\#U}0,y) \cond \neg\,\mathsf{is~a~coded~proof~from}~Q(p, y)$
Equivalently:
(ii) $Q\proves \forall p. \neg\,\mathsf{is~a~coded~proof~from}~Q(p, S^{\#G}0)$
Well, if $Q$ *did* prove $G$, then the proof would have a code number $m$. Then by virtue of what $\mathsf{is~a~coded~proof~from}~Q$ defines in $Q$, that would mean that:
(iii) $Q\proves \mathsf{is~a~coded~proof~from}~Q(S^m0, S^{\#G}0)$
But (ii) and (iii) could only both be true if $Q$ were inconsistent, which our Theorem assumes is not the case.
Next, let's ask whether $Q$ might prove $\neg G$? That is:
(iv) $Q\proves \neg\forall p \forall y. \mathsf{is~the~coded~self{-}application}(S^{\#U}0,y) \cond \neg\,\mathsf{is~a~coded~proof~from}~Q(p, y)$
Equivalently:
(iv) $Q\proves \neg\forall p. \neg\,\mathsf{is~a~coded~proof~from}~Q(p, S^{\#G}0)$
However, we saw above that for no $m$ could $Q$ prove (iii). Indeed, it can be shown that $Q$ will prove the negation of (iii) for every $m$. Hence, if $Q$ also proved (iv), then $Q$ would be $\omega$-inconsistent.
That completes the proof of Theorem C.
All of this would be reproducable in any extension $T$ of $Q$ that remained axiomatizable and consistent. (We need $T$ to be axiomatizable so that the notion of being a proof from $T$ can be primitively recursive.)
If we rely not just on the fact that $\textrm{is~the~coded~self{-}application~of}$ is arithmetically definable, but on the fact that it's also *functionally* definable, then we can prove that not only is $G$ not provable in $Q$, it's also *provable in* $Q$ that
(v) $G \bicond \neg\,Q\textrm{-provable}(S^{\#G}0)$
See Smith sections 38, 39, and 40.3; and Burgess Lemma 17.1.
## 11 ##
Okay, so $G$ is neither provable nor disprovable from some favored axiomatization of arithmetic; why don't we then just add $G$ as a further axiom? You can do that. But then --- so long as your new theory is still axiomatizable and deductively consistent --- the First Incompleteness Theorem will still apply, and so there will be a *new* Goedel sentence that talks about its own unprovability in the new theory. Plus, since the new theory is an extension of the old one, the new Goedel sentence won't be provable from the old theory, either. (See Smith sections 3.2 and 34.4.)
## 12 ##
Here are some of the other results that quickly follow from the First Incompleteness Theorem, or the apparatus we develop to prove it.
* The set of (codes of) theorems of any consistent extension of $Q$ can't be *arithmetically definable in that theory*. (See Burgess Theorem 17.2; note that the theory here needn't be axiomatizable.)
* In particular, the previous result applies to true arithmetic. (This is called **Tarski's Theorem**; see Burgess Theorem 17.3.)
* So the set of (codes of) theorems of true arithmetic can't be (primitively or not) *recursive*, either, since it's known that recursive sets are definable in true arithmetic. (See Burgess Theorem 17.4 and Smith Theorem 7. On the assumption that recursive = effectively decidable, this is called **the undecidability of (true) arithmetic**.)
* Nor can the set of (codes of) theorems of any consistent extension of $Q$ be recursive (that is, decidable). (This is called the **essential undecidability** of $Q$: not only is it undecidable what $Q$'s theorems are, this remains true for any consistent extension. See Burgess Theorem 17.5. Burgess proves his 17.7 from this and Smith-3/Burgess 15.7.)
* Since $Q$ is *finitely* axiomatizable, if there were a way to effectively decide what sentences are first-order validities, then we could decide what's a theorem of $Q$ by just checking whether some long conditional (with $Q$'s axioms in the antecedent) was valid. Since we just said it's *undecidable* what's a theorem of $Q$, this gives us one proof of the undecidability of first-order validity. (This is called **Church's Theorem**; see Burgess Theorem 17.6 and Smith Theorem 6.)
## 13 ##
What about Goedel's Second Incompleteness Theorem?
Quickly, what's done here is to prove in a slight strengthening of $Q$ --- let's call it $Q'$ (see Smith Definition 63 for details) --- that:
> $(\bot~\textrm{is not provable from}~Q') \cond G~\textrm{is not provable from}~Q'$
(See Smith Theorem 57.) That just amounts to recapitulating part of the proof of the First Incompleteness Theorem but *within* $Q'$, instead of in our informal metalanguage. But since the consequent of this conditional is (provably in $Q$) equivalent to the Goedel sentence for $Q'$, this tells us:
> $Q'\proves (\bot~\textrm{is not provable from}~Q') \cond G$
and hence:
> if $Q'\proves\bot~\textrm{is not provable from}~Q'$, then $Q'\proves G$.
However we know from the First Incompleteness Theorem that if $Q'$ is consistent, then $Q'\not\proves G$. Result:
> if $Q'$ is consistent, then $Q'\not\proves\bot~\textrm{is not provable from}~Q'$.
(See Smith Theorem 58.) Another way to say this is: if $Q'$ is consistent, it can't prove that that fact about itself. The same holds for any axiomatizable extension of $Q'$, such as Peano arithmetic. (See Burgess Theorem 18.1.)
That needn't mean that it's impossible to rigorously prove that these theories are consistent; only that it's not possible to prove it *in the theories themselves*. One might prove it in a stronger theory; or in a different theory, that's neither weaker nor stronger. (As mentioned in section 3, Gentzen proved the consistency of Peano arithmetic in a different theory, a strengthened version of "primitively recursive arithmetic.") But then it can fairly be asked, why are we entitled to the assumption that these other theories are consistent?
There are many serious and hard questions about the significance of the Second Incompleteness Theorem, that we won't try to sort out here.