Incompleteness

Incompleteness and Provability

content/incompleteness/incompleteness-provability/incompleteness-provability.tex

% Part: incompleteness% Chapter: first-incompleteness\documentclass[../../../include/open-logic-chapter]{subfiles}\begin{document}\olchapter{inc}{inp}{Incompleteness and Provability}\olimport{introduction}\olimport{fixed-point-lemma}\olimport{first-incompleteness-thm}\olimport{rosser-thm}\olimport{godels-paper}\olimport{provability-conditions}\olimport{second-incompleteness-thm}\olimport{lob-thm}\olimport{tarski-thm}\OLEndChapterHook\end{document}

content/incompleteness/incompleteness-provability/introduction.tex

% Part: incompleteness% Chapter: incompleteness-provability% Section: introduction\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{inc}{inp}{int}\olsection{Introduction}Hilbert thought that a system of axioms for a mathematical structure,such as the natural numbers, is inadequate unless it allows one toderive all true statements about the structure. Combined with hislater interest in formal systems of deduction, this suggests that hethought that we should guarantee that, say, the formal systems we areusing to reason about the natural numbers is not only consistent, butalso \emph{complete}, i.e., every statement in its language is either!!{derivable} or its negation is. G\"odel's first incompleteness theoremshows that no such system of axioms exists: there is no complete,consistent, !!{axiomatizable} formal system for arithmetic.  In fact,no ``sufficiently strong,'' consistent, !!{axiomatizable} mathematicaltheory is complete.A more important goal of Hilbert's, the centerpiece of his program forthe justification of modern (``classical'') mathematics, was to findfinitary consistency proofs for formal systems representing classicalreasoning.  With regard to Hilbert's program, then, G\"odel's secondincompleteness theorem was a much bigger blow. The secondincompleteness theorem can be stated in vague terms, like the firstincompleteness theorem. Roughly speaking, it says that no sufficientlystrong theory of arithmetic can prove its own consistency. We willhave to take ``sufficiently strong'' to include a little bit morethan~$\Th{Q}$.The idea behind G\"odel's original proof of the incompleteness theoremcan be found in the Epimenides paradox. Epimenides, a Cretan, assertedthat all Cretans are liars; a more direct form of the paradox is theassertion ``this sentence is false.'' Essentially, by replacing truthwith !!{derivability}, G\"odel was able to formalize !!a{sentence}which, in a roundabout way, asserts that it itself is not!!{derivable}.  If that !!{sentence} were !!{derivable}, the theorywould then be inconsistent.  G\"odel showed that the negation of that!!{sentence} is also not !!{derivable} from the system of axioms he wasconsidering. (For this second part, G\"odel had to assume that thetheory~$\Th{T}$ is what's called ``$\omega$-consistent.''$\omega$-Consistency is related to consistency, but is a strongerproperty.\footnote{That is, any $\omega$-consistent theory isconsistent, but not vice versa.} A few years after G\"odel, Rossershowed that assuming simple consistency of~$\Th{T}$ is enough.)The first challenge is to understand how one can construct !!a{sentence}that refers to itself. For every !!{formula}~$!A$ in the languageof~$\Th{Q}$, let~$\gn{!A}$ denote the numeral correspondingto~$\Gn{!A}$. Think about what this means: $!A$~is !!a{formula} in thelanguage of~$\Th{Q}$, $\Gn{!A}$~is a natural number, and $\gn{!A}$~isa \emph{term} in the language of~$\Th{Q}$. So every !!{formula}~$!A$in the language of~$\Th{Q}$ has a \emph{name},~$\gn{!A}$, which is aterm in the language of~$\Th{Q}$; this provides us with a conceptualframework in which !!{formula}s in the language of~$\Th{Q}$ can ``say''things about other !!{formula}s. The following lemma is known as thefixed-point lemma.\begin{lem}Let $\Th{T}$ be any theory extending~$\Th{Q}$, and let $!B(x)$ be any!!{formula} with only the variable~$x$ free. Then there is!!a{sentence}~$!A$ such that $\Th{T} \Proves!A \liff !B(\gn{!A})$.\end{lem}The lemma asserts that given any property $!B(x)$, there is!!a{sentence}~$!A$ that asserts ``$!B(x)$ is true of me,'' and$\Th{T}$ ``knows'' this.How can we construct such !!a{sentence}? Consider the following versionof the Epimenides paradox, due to Quine:\begin{quote}``Yields falsehood when preceded by its quotation'' yields falsehoodwhen preceded by its quotation.\end{quote}This sentence is not directly self-referential. It simply makes anassertion about the syntactic objects between quotes, and, in doingso, it is on par with sentences like\begin{enumerate}\item ``Robert'' is a nice name.\item ``I ran.'' is a short sentence.\item ``Has three words'' has three words.\end{enumerate}But what happens when one takes the phrase ``yields falsehood whenpreceded by its quotation,'' and precedes it with a quoted version ofitself? Then one has the original sentence!{} In short, the sentenceasserts that it is false.\end{document}

content/incompleteness/incompleteness-provability/fixed-point-lemma.tex

% Part: incompleteness% Chapter: incompleteness-provability% Section: fixed-point-lemma\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{inc}{inp}{fix}\olsection{The Fixed-Point Lemma}\begin{explain}The fixed-point lemma says that for any !!{formula}~$!B(x)$, there is!!a{sentence}~$!A$ such that $\Th{T} \Proves !A \liff !B(\gn{!A})$,provided $\Th{T}$ extends~$\Th{Q}$.  In the case of the liar sentence,we'd want $!A$ to be equivalent (provably in~$\Th{T}$) to~``$\gn{!A}$is false,'' i.e., the statement that $\Gn{!A}$ is the G\"odel numberof a false !!{sentence}. To understand the idea of the proof, it willbe useful to compare it with Quine's informal gloss of~$!A$ as,``{}`yields a falsehood when preceded by its own quotation' yields afalsehood when preceded by its own quotation.''  The operation oftaking an expression, and then forming a sentence by preceding thisexpression by its own quotation may be called \emph{diagonalizing} theexpression, and the result its diagonalization. So, thediagonalization of `yields a falsehood when preceded by its ownquotation' is ``{}`yields a falsehood when preceded by its ownquotation' yields a falsehood when preceded by its own quotation.''Now note that Quine's liar sentence is not the diagonalization of`yields a falsehood' but of `yields a falsehood when preceded by itsown quotation.' So the property being diagonalized to yield the liarsentence itself involves diagonalization!{}In the language of arithmetic, we form quotations of !!a{formula} withone free variable by computing its G\"odel numbers and thensubstituting the standard numeral for that G\"odel number into thefree variable. The diagonalization of~$!E(x)$ is $!E(\num{n})$, where$n = \Gn{!E(x)}$. (From now on, let's abbreviate $\num{\Gn{!E(x)}}$ as$\gn{!E(x)}$.)  So if $!B(x)$ is ``is a falsehood,'' then ``yields afalsehood if preceded by its own quotation,'' would be ``yields afalsehood when applied to the G\"odel number of its diagonalization.''If we had a symbol~$\Obj{diag}$ for the function $\fn{diag}(n)$ whichcomputes the G\"odel number of the diagonalization of the !!{formula}with G\"odel number~$n$, we could write $!E(x)$ as$!B(\Obj{diag}(x))$. And Quine's version of the liar sentence wouldthen be the diagonalization of it, i.e., $!E(\gn{!E(x)})$ or$!B(\Obj{diag}(\gn{!B(\Obj{diag}(x))}))$.  Of course, $!B(x)$ couldnow be any other property, and the same construction would work. Forthe incompleteness theorem, we'll take $!B(x)$ to be ``$x$~is not!!{derivable} in~$\Th{T}$.'' Then $!E(x)$ would be ``yields!!a{sentence} not !!{derivable} in~$\Th{T}$ when applied to theG\"odel number of its diagonalization.''To formalize this in~$\Th{T}$, we have to find a way to formalize$\fn{diag}$. The function $\fn{diag}(n)$ is computable, in fact, it isprimitive recursive: if $n$ is the G\"odel number of aformula~$!E(x)$, $\fn{diag}(n)$ returns the G\"odel numberof~$!E(\gn{!E(x)})$. (Recall, $\gn{!E(x)}$ is the standard numeral ofthe G\"odel number of~$!E(x)$, i.e., $\num{\Gn{!E(x)}}$). If$\Obj{diag}$ were a function symbol in $\Th{T}$ representing thefunction $\fn{diag}$, we could take $!A$ to be the formula$!B(\Obj{diag}(\gn{!B(\Obj{diag}(x))}))$. Notice that\begin{align*}\fn{diag}(\Gn{!B(\Obj{diag}(x))}) & = \Gn{!B(\Obj{diag}(\gn{!B(\Obj{diag}(x))}))} \\& = \Gn{!A}.\end{align*}Assuming $\Th{T}$ can !!{derive}\[\Obj{diag}(\gn{!B(\Obj{diag}(x))}) = \gn{!A},\]it can !!{derive} $!B(\Obj{diag}(\gn{!B(\Obj{diag}(x))}))\liff !B(\gn{!A})$. But the left hand side is, bydefinition,~$!A$.Of course, $\Obj{diag}$ will in general not be a function symbol of$\Th{T}$, and certainly is not one of~$\Th{Q}$. But, since $\fn{diag}$is computable, it is \emph{representable} in~$\Th{Q}$ by some formula$!D_{\fn{diag}}(x,y)$. So instead of writing $!B(\Obj{diag}(x))$ wecan write $\lexists[y][(!D_{\fn{diag}}(x,y) \land !B(y))]$. Otherwise,the proof sketched above goes through, and in fact, it goes throughalready in~$\Th{Q}$.\end{explain}\begin{lem}\ollabel{lem:fixed-point} Let $!B(x)$ be any formula with one freevariable~$x$. Then there is a sentence~$!A$ such that $\Th{Q} \Proves!A \liff !B(\gn{!A})$.\end{lem}\begin{proof}Given $!B(x)$, let $!E(x)$ be the formula$\lexists[y][(!D_{\fn{diag}}(x,y) \land !B(y))]$ and let $!A$~be itsdiagonalization, i.e., the formula $!E(\gn{!E(x)})$.Since $!D_{\fn{diag}}$ represents $\fn{diag}$, and$\fn{diag}(\Gn{!E(x)}) = \Gn{!A}$, $\Th{Q}$ can !!{derive}\begin{align}  & !D_{\fn{diag}}(\gn{!E(x)}, \gn{!A}) \ollabel{repdiag1} \\  & \lforall[y][(!D_{\fn{diag}}(\gn{!E(x)},y) \lif  \eq[y][\gn{!A}])]. \ollabel{repdiag2}\end{align}Now we show that $\Th{Q} \Proves !A \liff !B(\gn{!A})$. We argueinformally, using just logic and facts !!{derivable} in~$\Th{Q}$.First, suppose~$!A$, i.e., $!E(\gn{!E(x)})$. Going back to thedefinition of $!E(x)$, we see that $!E(\gn{!E(x)})$ just is\[\lexists[y][(!D_{\fn{diag}}(\gn{!E(x)},y) \land !B(y))].\]Consider such a~$y$. Since $!D_{\fn{diag}}(\gn{!E(x)},y)$, by\olref{repdiag2}, $y = \gn{!A}$. So, from $!B(y)$ wehave~$!B(\gn{!A})$.Now suppose $!B(\gn{!A})$. By \olref{repdiag1}, we have\begin{align*}& !D_{\fn{diag}}(\gn{!E(x)}, \gn{!A}) \land !B(\gn{!A}).\intertext{It followsthat}& \lexists[y][(!D_{\fn{diag}}(\gn{!E(x)},y) \land !B(y))].\end{align*}But that's just $!E(\gn{!E(x)})$, i.e.,~$!A$.\end{proof}\begin{digress}You should compare this to the proof of the fixed-point lemma incomputability theory. The difference is that here we want to define a\emph{statement} in terms of itself, whereas there we wanted to definea \emph{function} in terms of itself; this difference aside, it isreally the same idea.\end{digress}\begin{prob}   !!^a{formula}~$!A(x)$ is a \emph{truth definition} if $\Th{Q}  \Proves !B \liff !A(\gn{!B})$ for all !!{sentence}s~$!B$. Show that  no !!{formula} is a truth definition by using the fixed-point lemma.\end{prob}\end{document}

content/incompleteness/incompleteness-provability/first-incompleteness-thm.tex

% Part: incompleteness% Chapter: incompleteness-provability% Section: first-incompleteness-thm\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{inc}{inp}{1in}\olsection{The First Incompleteness Theorem}We can now describe G\"odel's original proof of the firstincompleteness theorem. Let $\Th{T}$ be any computably axiomatized theoryin a language extending the language of arithmetic, such that $\Th{T}$includes the axioms of $\Th{Q}$. This means that, in particular, $\Th{T}$represents computable functions and relations.We have argued that, given a reasonable coding of formulas and proofsas numbers, the relation $\Prf[\Th{T}](x,y)$ is computable, where$\Prf[\Th{T}](x,y)$ holds if and only if $x$ is the G\"odel number of!!a{derivation} of the !!{formula} with G\"odel number~$y$in~$\Th{T}$. In fact, for the particular theory that G\"odel had inmind, G\"odel was able to show that this relation is primitiverecursive, using the list of 45 functions and relations in hispaper. The 45th relation, $x B y$, is just $\Prf[\Th{T}](x,y)$ for hisparticular choice of~$\Th{T}$. Remember that where G\"odel uses theword ``recursive'' in his paper, we would now use the phrase``primitive recursive.''Since $\Prf[\Th{T}](x,y)$ is computable, it is representable in $\Th{T}$. Wewill use $\OPrf[\Th{T}](x,y)$ to refer to the formula that representsit. Let $\OProv[\Th{T}](y)$ be the formula$\lexists[x][\OPrf[\Th{T}](x,y)]$. This describes the 46th relation,$\fn{Bew}(y)$, on G\"odel's list. As G\"odel notes, this is the onlyrelation that ``cannot be asserted to be recursive.''  What heprobably meant is this: from the definition, it is not clear that itis computable; and later developments, in fact, show that it isn't.Let $\Th{T}$ be an !!{axiomatizable} theory containing~$\Th{Q}$. Then$\Prf[\Th{T}](x, y)$ is decidable, hence representable in~$\Th{Q}$ by!!a{formula}~$\OPrf[\Th{T}](x, y)$. Let $\OProv[\Th{T}](y)$ be the formula wedescribed above. By the fixed-point lemma, there is a formula$!G_\Th{T}$ such that $\Th{Q}$ (and hence $\Th{T}$) !!{derive}s\begin{equation}\ollabel{eqn:qpf}!G_\Th{T} \liff \lnot \OProv[\Th{T}](\gn{!G_\Th{T}}).\end{equation}Note that $!G_\Th{T}$ says, in essence, ``$!G_\Th{T}$ is not!!{derivable} in~$\Th{T}$.''\begin{lem}\ollabel{lem:cons-G-unprov}If $\Th{T}$ is a consistent, !!{axiomatizable} theoryextending~$\Th{Q}$, then $\Th{T} \Proves/ !G_\Th{T}$.\end{lem}\begin{proof}Suppose $\Th{T}$ !!{derive}s $!G_\Th{T}$. Then there \emph{is}!!a{derivation}, and so, for some number $m$, the relation $\Prf[\Th{T}](m,\Gn{!G_\Th{T}})$ holds. But then $\Th{Q}$ !!{derive}s the sentence$\OPrf[\Th{T}](\num m, \gn{!G_\Th{T}})$. So $\Th{Q}$ !!{derive}s$\lexists[x][\OPrf[\Th{T}](x,\gn{!G_\Th{T}})]$, which is, by definition,$\OProv[\Th{T}](\gn{!G_\Th{T}})$. By \olref{eqn:qpf}, $\Th{Q}$ !!{derive}s$\lnot !G_\Th{T}$, and since $\Th{T}$ extends $\Th{Q}$, sodoes~$\Th{T}$. We have shown that if $\Th{T}$ !!{derive}s $!G_\Th{T}$, thenit also !!{derive}s $\lnot !G_\Th{T}$, and hence it would be inconsistent.\end{proof}\begin{defn}\ollabel{thm:oconsis-q}A theory $\Th{T}$ is \emph{$\omega$-consistent} if the following holds: if$\lexists[x][!A(x)]$ is any sentence and $\Th{T}$ !!{derive}s $\lnot!A(\num 0)$, $\lnot !A(\num 1)$, $\lnot !A(\num 2)$, \dots then $\Th{T}$does not prove $\lexists[x][!A(x)]$.\end{defn}Note that every $\omega$-consistent theory is also consistent. Thisfollows simply from the fact that if $\Th{T}$ is inconsistent, then$\Th{T} \Proves !A$ for every~$!A$. In particular, if $\Th{T}$ isinconsistent, it !!{derive}s both $\lnot !A(\num n)$ for every~$n$ andalso !!{derive}s~$\lexists[x][!A(x)]$. So, if $\Th{T}$ isinconsistent, it is $\omega$-inconsistent. By contraposition, if$\Th{T}$ is $\omega$-consistent, it must be consistent.\begin{lem}\ollabel{lem:omega-cons-G-unref}If $\Th{T}$ is an $\omega$-consistent, !!{axiomatizable} theoryextending~$\Th{Q}$, then $\Th{T} \Proves/ \lnot !G_\Th{T}$.\end{lem}\begin{proof}We show that if $\Th{T}$ !!{derive}s $\lnot !G_\Th{T}$, then it is$\omega$-inconsistent. Suppose $\Th{T}$ !!{derive}s $\lnot !G_\Th{T}$. If$\Th{T}$ is inconsistent, it is $\omega$-inconsistent, and we aredone. Otherwise, $\Th{T}$ is consistent, so it does not !!{derive}$!G_\Th{T}$ by \olref{lem:cons-G-unprov}. Since there is no!!{derivation} of $!G_\Th{T}$ in $\Th{T}$, $\Th{Q}$ !!{derive}s\[\lnot \OPrf[\Th{T}](\num 0, \gn{!G_\Th{T}}), \lnot \OPrf[\Th{T}](\num 1,\gn{!G_\Th{T}}), \lnot \OPrf[\Th{T}](\num 2, \gn{!G_\Th{T}}), \dots\]and so does~$\Th{T}$.  On the other hand, by \olref{eqn:qpf}, $\lnot!G_\Th{T}$ is equivalent to$\lexists[x][\OPrf[\Th{T}](x,\gn{!G_\Th{T}})]$. So $\Th{T}$ is$\omega$-inconsistent.\end{proof}\begin{prob}  Every $\omega$-consistent theory is consistent. Show that the  converse does not hold, i.e., that there are consistent but  $\omega$-inconsistent theories. Do this by showing that $\Th{Q} \cup  \{\lnot !G_\Th{Q}\}$ is consistent but $\omega$-inconsistent.\end{prob}\begin{thm}\ollabel{thm:first-incompleteness} Let $\Th{T}$ be any$\omega$-consistent, !!{axiomatizable} theory extending~$\Th{Q}$. Then$\Th{T}$ is not complete.\end{thm}\begin{proof}  If $\Th{T}$ is $\omega$-consistent, it is consistent, so $\Th{T}  \Proves/ !G_\Th{T}$ by \olref{lem:cons-G-unprov}.  By  \olref{lem:omega-cons-G-unref}, $\Th{T} \Proves/ \lnot !G_\Th{T}$.  This means that $\Th{T}$ is incomplete, since it !!{derive}s neither  $!G_\Th{T}$ nor $\lnot !G_\Th{T}$.\end{proof}\end{document}

content/incompleteness/incompleteness-provability/rosser-thm.tex

% Part: incompleteness% Chapter: incompleteness-provability% Section: rosser-thm\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{inc}{inp}{ros}\olsection{Rosser's Theorem}Can we modify G\"odel's proof to get a stronger result, replacing``$\omega$-consistent'' with simply ``consistent''? The answer is``yes,'' using a trick discovered by Rosser.  Rosser's trick is to usea ``modified'' !!{derivability} predicate $\ORProv_T(y)$ instead of$\OProv[\Th{T}](y)$.\begin{thm}\ollabel{thm:rosser}Let $\Th{T}$ be any consistent, !!{axiomatizable} theoryextending $\Th{Q}$. Then $\Th{T}$ is not complete.\end{thm}\begin{proof}Recall that $\OProv[\Th{T}](y)$ is defined as $\lexists[x][\OPrf[\Th{T}](x,  y)]$, where $\OPrf[\Th{T}](x, y)$ represents the decidable relation whichholds iff $x$ is the G\"odel number of !!a{derivation} of the!!{sentence} with G\"odel number~$y$. The relation that holds between$x$ and~$y$ if $x$~is the G\"odel number of a \emph{refutation} of thesentence with G\"odel number~$y$ is also decidable. Let $\fn{not}(x)$be the primitive recursive function which does the following: if $x$is the code of a formula $!A$, $\fn{not}(x)$ is a code of $\lnot!A$. Then $\Refut[\Th{T}](x, y)$ holds iff $\Prf[\Th{T}](x, \fn{not}(y))$.  Let$\ORefut[\Th{T}](x, y)$ represent it.  Then, if $\Th{T} \Proves \lnot !A$and $\delta$ is a corresponding !!{derivation}, $\Th{Q} \Proves\ORefut[\Th{T}](\gn{\delta}, \gn{!A})$.  We define $\ORProv[\Th{T}](y)$ as\[\lexists[x][(\OPrf[\Th{T}](x,y) \land \lforall[z][(z < x \lif \lnot  \ORefut[\Th{T}](z,y))])].\]Roughly, $\ORProv[\Th{T}](y)$ says ``there is a proof of $y$ in $\Th{T}$,and there is no shorter refutation of~$y$.''  Assuming $\Th{T}$ isconsistent, $\ORProv[\Th{T}](y)$ is true of the same numbers as$\OProv[\Th{T}](y)$; but from the point of view of \emph{provability}in~$\Th{T}$ (and we now know that there is a difference between truthand provability!) the two have different properties. If $\Th{T}$ is\emph{in}consistent, then the two do \emph{not} hold of the samenumbers!{} ($\ORProv[\Th{T}](y)$ is often read as ``$y$ is Rosserprovable.'' Since, as just discussed, Rosser provability is not somespecial kind of provability---in inconsistent theories, there are!!{sentence}s that are provable but not Rosser provable---this may beconfusing. To avoid the confusion, you could instead read it as``$y$ is shmovable.'')By the fixed-point lemma, there is a formula $!R_\Th{T}$ such that\begin{equation}  \Th{Q} \Proves !R_\Th{T} \liff \lnot \ORProv[\Th{T}](\gn{!R_\Th{T}}).  \ollabel{RT}\end{equation}In contrast to the proof of \olref[1in]{thm:first-incompleteness},here we claim that if $\Th{T}$ is consistent, $\Th{T}$ doesn't !!{derive}$!R_\Th{T}$, and $\Th{T}$ also doesn't !!{derive} $\lnot !R_\Th{T}$. (Inother words, we don't need the assumption of $\omega$-consistency.)First, let's show that $\Th{T} \Proves/ !R_{\Th{T}}$.  Suppose it did, sothere is !!a{derivation} of~$!R_{\Th{T}}$ from~$T$; let $n$ be its G\"odelnumber. Then $\Th{Q} \Proves \OPrf[\Th{T}](\num{n}, \gn{!R_{\Th{T}}})$, since$\OPrf[\Th{T}]$ represents $\Prf[\Th{T}]$ in~$\Th{Q}$. Also, for each $k < n$,$k$ is not the G\"odel number of !!a{derivation} of $\lnot !R_{\Th{T}}$, since $\Th{T}$ isconsistent. So for each $k < n$, $\Th{Q} \Proves \lnot\ORefut[\Th{T}](\num{k}, \gn{!R_{\Th{T}}})$. By \olref[req][min]{lem:less-nsucc},$\Th{Q} \Proves \lforall[z][(z < \num{n} \lif \lnot \ORefut[\Th{T}](z,  \gn{!R_{\Th{T}}}))]$. Thus,\[\Th{Q} \Proves \lexists[x][(\OPrf[\Th{T}](x,\gn{!R_{\Th{T}}}) \land \lforall[z][(z    < x \lif \lnot \ORefut[\Th{T}](z,\gn{!R_{\Th{T}}}))])],\]but that's just $\ORProv[\Th{T}](\gn{!R_{\Th{T}}})$. By \olref{RT}, $\Th{Q}\Proves \lnot !R_{\Th{T}}$. Since $\Th{T}$ extends $\Th{Q}$, also $\Th{T}\Proves \lnot !R_{\Th{T}}$. We've assumed that $\Th{T} \Proves !R_{\Th{T}}$, so$\Th{T}$ would be inconsistent, contrary to the assumption of thetheorem.Now, let's show that $\Th{T} \Proves/ \lnot !R_{\Th{T}}$. Again, suppose itdid, and suppose $n$ is the G\"odel number of !!a{derivation}of~$\lnot !R_{\Th{T}}$. Then $\Refut[\Th{T}](n, \Gn{!R_{\Th{T}}})$ holds, and since$\ORefut[\Th{T}]$ represents $\Refut[\Th{T}]$ in $\Th{Q}$, $\Th{Q} \Proves\ORefut[\Th{T}](\num{n}, \gn{!R_{\Th{T}}})$. We'll again show that $\Th{T}$ wouldthen be inconsistent because it would also !!{derive}~$!R_{\Th{T}}$.  Since\begin{align*}\Th{Q} & \Proves !R_{\Th{T}} \liff \lnot \ORProv[\Th{T}](\gn{!R_{\Th{T}}}), \intertext{and since $\Th{T}$ extends~$\Th{Q}$, it suffices to show that}\Th{Q} & \Proves \lnot \ORProv[\Th{T}](\gn{!R_{\Th{T}}}).\end{align*}The !!{sentence} $\lnot\ORProv[\Th{T}](\gn{!R_{\Th{T}}})$, i.e.,\begin{align*}  \lnot & \lexists[x][(\OPrf[\Th{T}](x,\gn{!R_{\Th{T}}}) \land    \lforall[z][(z < x \lif \lnot \ORefut[\Th{T}](z,\gn{!R_{\Th{T}}}))])],  \intertext{is logically equivalent to}  & \lforall[x][(\OPrf[\Th{T}](x,\gn{!R_{\Th{T}}}) \lif    \lexists[z][(z < x \land \ORefut[\Th{T}](z,\gn{!R_{\Th{T}}}))])].\end{align*}We argue informally using logic, making use of facts about what$\Th{Q}$ !!{derive}s. Suppose $x$ is arbitrary and $\OPrf[\Th{T}](x,\gn{!R_{\Th{T}}})$. We already know that $\Th{T} \Proves/ !R_{\Th{T}}$, and so forevery $k$, $\Th{Q} \Proves \lnot \OPrf[\Th{T}](\num{k}, \gn{!R_{\Th{T}}})$. Thus,for every $k$ it follows that $\eq/[x][\num{k}]$. In particular, wehave (a) that $\eq/[x][\num{n}]$.  We also have $\lnot(\eq[x][\num{0}]\lor \eq[x][\num{1}] \lor \dots \lor \eq[x][\num{n-1}])$ and so by\olref[req][min]{lem:less-nsucc}, (b) $\lnot(x < \num{n})$. By\olref[req][min]{lem:trichotomy}, $\num{n} < x$. Since $\Th{Q} \Proves\ORefut[\Th{T}](\num{n}, \gn{!R_{\Th{T}}})$, we have $\num{n} < x \land\ORefut[\Th{T}](\num{n}, \gn{!R_{\Th{T}}})$, and from that $\lexists[z][(z < x\land \ORefut[\Th{T}](z,\gn{!R_{\Th{T}}}))]$. Since $x$ was arbitrary we get, asrequired, that\[\lforall[x][(\OPrf[\Th{T}](x,\gn{!R_{\Th{T}}}) \lif  \lexists[z][(z < x \land \ORefut[\Th{T}](z,\gn{!R_{\Th{T}}}))])].\]\end{proof}\begin{prob}Two sets $A$ and $B$ of natural numbers are said to be\emph{computably inseparable} if there is no !!{decidable} set~$X$such that $A \subseteq X$ and $B \subseteq \Complement{X}$($\Complement{X}$ is the complement, $\Nat \setminus X$, of~$X$). Let$\Th{T}$ be a consistent !!{axiomatizable} extension of $\Th{Q}$.Suppose $A$ is the set of G\"odel numbers of !!{sentence}s provablein~$\Th{T}$ and $B$ the set of G\"odel numbers of sentencesrefutable in~$\Th{T}$. Prove that $A$ and~$B$ are computablyinseparable.\end{prob}\end{document}

content/incompleteness/incompleteness-provability/godels-paper.tex

% Part: incompleteness% Chapter: incompleteness-provability% Section: godels-paper\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{inc}{inp}{gop}\olsection{Comparison with G\"odel's Original Paper}It is worthwhile to spend some time with G\"odel's 1931paper. The introduction sketches the ideas we have just discussed.Even if you just skim through the paper, it is easy to see what isgoing on at each stage: first G\"odel describes the formal system $P$(syntax, axioms, proof rules); then he defines the primitive recursivefunctions and relations; then he shows that $x B y$ is primitiverecursive, and argues that the primitive recursive functions andrelations are represented in $\Th{P}$. He then goes on to prove theincompleteness theorem, as above. In Section 3, he shows that one cantake the unprovable assertion to be a sentence in the language ofarithmetic. This is the origin of the $\beta$-lemma, which is what wealso used to handle sequences in showing that the recursive functionsare representable in $\Th{Q}$. G\"odel doesn't go so far to isolate aminimal set of axioms that suffice, but we now know that $\Th{Q}$ will dothe trick.  Finally, in Section 4, he sketches a proof of the secondincompleteness theorem.\end{document}

content/incompleteness/incompleteness-provability/provability-conditions.tex

% Part: incompleteness% Chapter: incompleteness-provability% Section: provability-conditions\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{inc}{inp}{prc}\olsection{The \usetoken{S}{derivability} Conditions for $\Th{PA}$}Peano arithmetic, or $\Th{PA}$, is the theory extending $\Th{Q}$ withinduction axioms for all !!{formula}s. In other words, one adds to $\Th{Q}$axioms of the form\[(!A(0) \land \lforall[x][(!A(x) \lif !A(x'))]) \lif \lforall[x][!A(x)]\]for every !!{formula}~$!A$. Notice that this is really a\emph{schema}, which is to say, infinitely many axioms (and it turnsout that $\Th{PA}$ is {\em not} finitely axiomatizable). But since onecan effectively determine whether or not a string of symbols is aninstance of an induction axiom, the set of axioms for $\Th{PA}$ iscomputable. $\Th{PA}$ is a much more robust theory than~$\Th{Q}$. Forexample, one can easily prove that addition and multiplication arecommutative, using induction in the usual way. In fact, most finitarynumber-theoretic and combinatorial arguments can be carried outin~$\Th{PA}$.Since $\Th{PA}$ is computably axiomatized, the !!{derivability}predicate $\Prf[\Th{PA}](x,y)$ is computable and hence representedin~$\Th{Q}$ (and so, in~$\Th{PA}$). As before, we will take$\OPrf[\Th{PA}](x,y)$ to denote the formula representing the relation.Let $\OProv[\Th{PA}](y)$ be the formula$\lexists[x][\Prf[\Th{PA}](x,y)]$, which, intuitively says, ``$y$ is!!{derivable} from the axioms of $\Th{PA}$.''  The reason we need alittle bit more than the axioms of $\Th{Q}$ is we need to know thatthe theory we are using is strong enough to !!{derive} a few basicfacts about this !!{derivability} predicate. In fact, what we need arethe following facts:\begin{enumerate}\item[P1.] If $\Th{PA} \Proves !A$, then $\Th{PA} \Proves  \OProv[\Th{PA}](\gn{!A})$.\item[P2.] For all !!{formula}s $!A$ and $!B$,  \[  \Th{PA} \Proves \OProv[\Th{PA}](\gn{!A \lif !B}) \lif  (\OProv[\Th{PA}](\gn{!A}) \lif \OProv[\Th{PA}](\gn{!B})).  \]\item[P3.] For every !!{formula}~$!A$,  \[  \Th{PA} \Proves \OProv[\Th{PA}](\gn{!A})  \lif \OProv[\Th{PA}](\gn{\OProv[\Th{PA}](\gn{!A})}).  \]\end{enumerate}The only way to verify that these three properties hold is to describethe !!{formula} $\OProv[\Th{PA}](y)$ carefully and use the axioms of$\Th{PA}$ to describe the relevant formal !!{derivation}s. Conditions (1)and~(2) are easy; it is really condition~(3) that requireswork. (Think about what kind of work it entails \dots) Carrying out thedetails would be tedious and uninteresting, so here we will ask you totake it on faith that $\Th{PA}$ has the three properties listedabove. A reasonable choice of $\OProv[\Th{PA}](y)$ will also satisfy\begin{enumerate}\item[P4.] If $\Th{PA} \Proves \OProv[\Th{PA}](\gn{!A})$, then  $\Th{PA} \Proves !A$.\end{enumerate}But we will not need this fact.\begin{digress}Incidentally, G\"odel was lazy in the same way we arebeing now. At the end of the 1931 paper, he sketches the proof of thesecond incompleteness theorem, and promises the details in a laterpaper. He never got around to it; since everyone who understood theargument believed that it could be carried out (he did not need tofill in the details.)\end{digress}\end{document}

content/incompleteness/incompleteness-provability/second-incompleteness-thm.tex

% Part: incompleteness% Chapter: incompleteness-provability% Section: second-incompleteness-thm\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{inc}{inp}{2in}\olsection{The Second Incompleteness Theorem}How can we express the assertion that $\Th{PA}$ doesn't prove its ownconsistency? Saying $\Th{PA}$ is inconsistent amounts to saying that$\Th{PA} \Proves \eq[0][1]$. So we can take the consistency statement$\OCon[\Th{PA}]$ to be the !!{sentence} $\lnot\OProv[\Th{PA}](\gn{\eq[0][1]})$, and then the following theorem doesthe job:\begin{thm}\ollabel{thm:second-incompleteness} Assuming $\Th{PA}$ is consistent, then $\Th{PA}$ does not !!{derive}$\OCon[\Th{PA}]$.\end{thm}It is important to note that the theorem depends on the particularrepresentation of $\OCon[\Th{PA}]$ (i.e., the particularrepresentation of $\OProv[\Th{PA}](y)$). All we will use is that therepresentation of $\OProv[\Th{PA}](y)$ satisfies the three!!{derivability} conditions, so the theorem generalizes to any theorywith !!a{derivability} predicate having these properties.It is informative to read G\"odel's sketch of an argument, since thetheorem follows like a good punch line. It goes like this. Let$!G_\Th{PA}$ be the G\"odel sentence that we constructed in the proofof \olref[1in]{thm:first-incompleteness}. We have shown ``If $\Th{PA}$is consistent, then $\Th{PA}$ does not !!{derive} $!G_\Th{PA}$.'' If weformalize this \emph{in} $\Th{PA}$, we have a proof of\[\OCon[\Th{PA}] \lif \lnot \OProv[\Th{PA}](\gn{!G_\Th{PA}}).\]Now suppose $\Th{PA}$ !!{derive}s $\OCon[\Th{PA}]$. Then it !!{derive}s $\lnot\Prov[\Th{PA}](\gn{!G_\Th{PA}})$. But since $!G_\Th{PA}$ is a G\"odelsentence, this is equivalent to $!G_\Th{PA}$. So $\Th{PA}$ !!{derive}s$!G_\Th{PA}$.But: we know that if $\Th{PA}$ is consistent, it doesn't !!{derive}$!G_\Th{PA}$!{}  So if $\Th{PA}$ is consistent, it can't !!{derive}$\OCon[\Th{PA}]$.To make the argument more precise, we will let $!G_\Th{PA}$ be theG\"odel sentence for~$\Th{PA}$ and use the !!{derivability} conditions(P1)--(P3) to show that $\Th{PA}$ !!{derive}s $\OCon[\Th{PA}] \lif!G_\Th{PA}$. This will show that $\Th{PA}$ doesn't !!{derive}$\OCon[\Th{PA}]$. Here is a sketch of the proof, in~$\Th{PA}$. (Forsimplicity, we drop the $\Th{PA}$ subscripts.)\begin{align}& !G \liff \lnot \OProv(\gn{!G}) \ollabel{G2-1}\\& \qquad\text{$!G$ is a G\"odel sentence}\notag \\& !G \lif \lnot \OProv(\gn{!G}) \ollabel{G2-2}\\  & \qquad\text{from \olref{G2-1}} \notag\\& !G \lif  (\OProv(\gn{!G}) \lif \lfalse) \ollabel{G2-3}\\  & \qquad\text{from \olref{G2-2} by logic}\notag\\& \OProv(\gn{    !G \lif    (\OProv(\gn{!G}) \lif \lfalse)  }) \ollabel{G2-4}\\  & \qquad\text{by from \olref{G2-3} by condition P1} \notag\\& \OProv(\gn{!G}) \lif  \OProv(\gn{    (\OProv(\gn{!G}) \lif \lfalse)    }) \ollabel{G2-5}\\  & \qquad\text{from \olref{G2-4} by condition P2} \notag\\& \OProv(\gn{!G}) \lif (\OProv(\gn{\OProv(\gn{!G})}) \lif \OProv(\gn{\lfalse})) \ollabel{G2-6}\\  & \qquad\text{from \olref{G2-5} by condition P2 and logic} \notag\\& \OProv(\gn{!G}) \lif   \OProv(\gn{\OProv(\gn{!G})}) \ollabel{G2-7}\\   & \qquad\text{by P3} \notag\\& \OProv(\gn{!G}) \lif \OProv(\gn{\lfalse}) \ollabel{G2-8}\\  & \qquad \text{from \olref{G2-6} and \olref{G2-7} by logic}\notag\\& \OCon \lif \lnot \OProv(\gn{!G}) \ollabel{G2-9}\\  & \qquad\text{contraposition of \olref{G2-8} and $\OCon \ident \lnot \OProv(\gn{\lfalse})$}\notag \\& \OCon \lif !G \notag\\  & \qquad\text{from \olref{G2-1} and \olref{G2-9} by logic}\notag\end{align}The use of logic in the above just elementary facts from propositionallogic, e.g., \olref{G2-3} uses $\Proves \lnot!A \liff (!A\lif\lfalse)$ and \olref{G2-8} uses $!A \lif (!B \lif !C), !A \lif !B\Proves !A \lif !C$. The use of condition~P2 in \olref{G2-5} and\olref{G2-6} relies on instances of~P2, $\OProv(\gn{!A \lif !B}) \lif(\OProv(\gn{!A}) \lif \OProv(\gn{!B}))$. In the first one, $!A \ident!G$ and $!B \ident \OProv(\gn{!G}) \lif \lfalse$; in the second, $!A\ident \OProv(\gn{G})$ and $!B \ident \lfalse$.The more abstract version of the second incompleteness theorem is as follows:\begin{thm}\ollabel{thm:second-incompleteness-gen} Let $\Th{T}$ be anyconsistent, !!{axiomatized} theory extending $\Th{Q}$ and let$\OProv[\Th{T}](y)$ be any formula satisfying !!{derivability} conditionsP1--P3 for~$\Th{T}$. Then $\Th{T}$ does not !!{derive}~$\OCon[T]$.\end{thm}\begin{prob}Show that $\Th{PA}$ !!{derive}s $!G_{\Th{PA}} \lif \OCon[\Th{PA}]$.\end{prob}\begin{digress}The moral of the story is that no ``reasonable'' consistent theory formathematics can !!{derive} its own consistency statement. Suppose$\Th{T}$ is a theory of mathematics that includes $\Th{Q}$ andHilbert's ``finitary'' reasoning (whatever that may be). Then, thewhole of $\Th{T}$ cannot !!{derive} the consistency statement of$\Th{T}$, and so, a fortiori, the finitary fragment can't !!{derive}the consistency statement of~$\Th{T}$ either. In that sense, therecannot be a finitary consistency proof for ``all of mathematics.''There is some leeway in interpreting the term ``finitary,'' andG\"odel, in the 1931 paper, grants the possibility that something wemay consider ``finitary'' may lie outside the kinds of mathematicsHilbert wanted to formalize. But G\"odel was being charitable; today,it is hard to see how we might find something that can reasonably becalled finitary but is not formalizable in, say, $\Th{ZFC}$,Zermelo--Fraenkel set theory with the axiom of choice.\end{digress}\end{document}

content/incompleteness/incompleteness-provability/lob-thm.tex

% Part: incompleteness% Chapter: incompleteness-provability% Section: lob-thm\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{inc}{inp}{lob}\olsection{L\"ob's Theorem}The G\"odel sentence for a theory~$\Th{T}$ is a fixed point of $\lnot\OProv[\Th{T}](y)$, i.e., !!a{sentence}~$!G$ such that\[\Th{T} \Proves \lnot \OProv[\Th{T}](\gn{!G}) \liff !G.\]It is not !!{derivable}, because if $\Th{T} \Proves !G$, (a) by !!{derivability}condition~(1), $\Th{T} \Proves \OProv[\Th{T}](\gn{!G})$, and (b) $\Th{T}\Proves !G$ together with $\Th{T} \Proves \lnot \OProv[\Th{T}](\gn{!G})\liff !G$ gives $\Th{T} \Proves \lnot \OProv[\Th{T}](\gn{!G})$, and so$\Th{T}$ would be inconsistent.  Now it is natural to ask about thestatus of a fixed point of $\OProv[\Th{T}](y)$, i.e., !!a{sentence}~$!H$such that\[\Th{T} \Proves \OProv[\Th{T}](\gn{!H}) \liff !H.\]If it were !!{derivable}, $\Th{T} \Proves \OProv[\Th{T}](\gn{!H})$ bycondition~(1), but the same conclusion follows if we apply modusponens to the equivalence above. Hence, we don't get that $\Th{T}$ isinconsistent, at least not by the same argument as in the case of theG\"odel sentence. This of course does not show that $\Th{T}$\emph{does} !!{derive}~$!H$.We can make headway on this question if we generalize it a bit. Theleft-to-right direction of the fixed point equivalence,$\OProv[\Th{T}](\gn{!H}) \lif !H$, is an instance of a general schemacalled a \emph{reflection principle}: $\OProv[\Th{T}](\gn{!A}) \lif !A$.It is called that because it expresses, in a sense, that $\Th{T}$ can``reflect'' about what it can !!{derive}; basically it says, ``If $\Th{T}$can !!{derive}~$!A$, then~$!A$ is true,'' for any~$!A$.  This is true forsound theories only, of course, and this suggests that theories willin general not !!{derive} every instance of it.  So which instances can atheory (strong enough, and satisfying the !!{derivability} conditions)!!{derive}?  Certainly all those where $!A$ itself is !!{derivable}. And that'sit, as the next result shows.\begin{thm}\ollabel{thm:lob}Let $\Th{T}$ be !!a{axiomatizable} theory extending $\Th{Q}$, andsuppose $\OProv[\Th{T}](y)$ is a formula satisfying conditions P1--P3 from\olref[2in]{sec}. If $\Th{T}$ !!{derive}s $\OProv[\Th{T}](\gn{!A}) \lif !A$,then in fact $\Th{T}$ !!{derive}s $!A$.\end{thm}Put differently, if $\Th{T} \Proves/ !A$, then $\Th{T} \Proves/\OProv[\Th{T}](\gn{!A}) \lif !A$. This result is known as L\"ob'stheorem.\begin{explain}The heuristic for the proof of L\"ob's theorem is a clever proof thatSanta Claus exists. (If you don't like that conclusion, you are freeto substitute any other conclusion you would like.) Here it is:\begin{enumerate}\item Let $X$ be the sentence, ``If $X$ is true, then Santa Claus  exists.''\item Suppose $X$ is true.\item Then what it says holds; i.e., we have: if $X$ is true, then  Santa Claus exists.\item Since we are assuming $X$ is true, we can conclude that  Santa Claus exists, by modus ponens from (2) and~(3).\item We have succeeded in deriving (4), ``Santa Claus exists,'' from  the assumption~(2), ``$X$ is true.'' By conditional proof, we have  shown: ``If $X$ is true, then Santa Claus exists.''\item But this is just the sentence~$X$. So we have shown that $X$ is  true.\item But then, by the argument (2)--(4) above, Santa Claus exists.\end{enumerate}A formalization of this idea, replacing ``is true'' with ``is!!{derivable},'' and ``Santa Claus exists'' with~$!A$, yields the proof ofL\"ob's theorem. The trick is to apply the fixed-point lemma to the!!{formula}~$\OProv[\Th{T}](y) \lif !A$. The fixed point of thatcorresponds to the sentence~$X$ in the preceding sketch.\end{explain}\begin{proof}[Proof of \olref{thm:lob}]Suppose $!A$ is !!a{sentence} such that $\Th{T}$ !!{derive}s$\OProv[\Th{T}](\gn{!A}) \lif !A$. Let $!B(y)$ be the !!{formula}~$\OProv[\Th{T}](y)\lif !A$, and use the fixed-point lemma to find !!a{sentence}~$!D$such that $\Th{T}$ !!{derive}s $!D \liff !B(\gn{!D})$. Then each of thefollowing is !!{derivable} in $\Th{T}$:\begin{align}  & !D \liff (\OProv[\Th{T}](\gn{!D}) \lif !A) \ollabel{L-1}\\  & \qquad \text{$!D$ is a fixed point of~$!B(y)$}\notag \\  & !D \lif (\OProv[\Th{T}](\gn{!D}) \lif !A) \ollabel{L-2}\\  & \qquad\text{from \olref{L-1}}\notag\\  & \OProv[\Th{T}](\gn{!D \lif (\OProv[\Th{T}](\gn{!D}) \lif !A)}) \ollabel{L-3}\\  & \qquad \text{from \olref{L-2} by condition P1}\notag \\  & \OProv[\Th{T}](\gn{!D}) \lif \OProv[\Th{T}](\gn{\OProv[\Th{T}](\gn{!D}) \lif !A})  \ollabel{L-4}\\  &\qquad \text{from \olref{L-3} using condition P2}\notag \\  & \OProv[\Th{T}](\gn{!D}) \lif (\OProv[\Th{T}](\gn{\OProv[\Th{T}](\gn{!D})}) \lif \OProv[\Th{T}](\gn{!A})) \ollabel{L-5}\\  &\qquad \text{from \olref{L-4} using P2 again} \notag\\& \OProv[\Th{T}](\gn{!D}) \lif \OProv[\Th{T}](\gn{\OProv[\Th{T}](\gn{!D})}) \ollabel{L-6}\\  & \qquad\text{by !!{derivability} condition P3} \notag\\  & \OProv[\Th{T}](\gn{!D}) \lif \OProv[\Th{T}](\gn{!A}) \ollabel{L-7} \\  &\qquad\text{from \olref{L-5} and \olref{L-6}}\notag\\  & \OProv[\Th{T}](\gn{!A}) \lif !A \ollabel{L-8}\\  &\qquad\text{by assumption of the theorem} \notag\\  & \OProv[\Th{T}](\gn{!D}) \lif !A \ollabel{L-9}\\  &\qquad\text{from \olref{L-7} and \olref{L-8}}\notag\\  & (\OProv[\Th{T}](\gn{!D}) \lif !A) \lif !D \ollabel{L-10}\\  & \qquad \text{from \olref{L-1}}\notag \\  & !D \ollabel{L-11}\\  & \qquad\text{from \olref{L-9} and \olref{L-10}}\notag \\  & \OProv[\Th{T}](\gn{!D}) \ollabel{L-12}\\  & \qquad\text{from \olref{L-11} by condition~P1}\notag \\  & !A \qquad\qquad\text{from \olref{L-8} and \olref{L-12}}\notag\end{align}\end{proof}With L\"ob's theorem in hand, there is a short proof of the secondincompleteness theorem (for theories having !!a{derivability} predicatesatisfying conditions P1--P3): if $\Th{T} \Proves\OProv[\Th{T}](\gn{\lfalse}) \lif \lfalse$, then $\Th{T} \Proves \lfalse$.If $\Th{T}$ is consistent, $\Th{T} \Proves/ \lfalse$. So, $\Th{T}\Proves/ \OProv[\Th{T}](\gn{\lfalse}) \lif \lfalse$, i.e., $\Th{T} \Proves/\OCon[\Th{T}]$.  We can also apply it to show that~$!H$, the fixedpoint of $\OProv[\Th{T}](x)$, is !!{derivable}. For since\begin{align*}  \Th{T} & \Proves \OProv[\Th{T}](\gn{!H}) \liff !H\\  \intertext{in particular}    \Th{T} & \Proves \OProv[\Th{T}](\gn{!H}) \lif !H\end{align*}and so by L\"ob's theorem, $\Th{T} \Proves !H$.% Going in the other direction, for homework I% may ask you to work through a short proof of L\"ob's theorem, using% the second incompleteness theorem instead of the fixed-point lemma.\begin{prob}Let $\Th{T}$ be a computably axiomatized theory, andlet $\OProv[\Th{T}]$ be !!a{derivability} predicate for $\Th{T}$. Consider thefollowing four statements:\begin{enumerate}\item If $T \Proves !A$, then $T \Proves \OProv[\Th{T}](\gn{!A})$.\item $T \Proves !A \lif \OProv[\Th{T}](\gn{!A})$.\item If $T \Proves \OProv[\Th{T}](\gn{!A})$, then $T \Proves !A$.\item $T \Proves \OProv[\Th{T}](\gn{!A}) \lif !A$\end{enumerate}Under what conditions are each of these statements true?\end{prob}\end{document}

content/incompleteness/incompleteness-provability/tarski-thm.tex

% Part: incompleteness% Chapter: incompleteness-provability% Section: lob-thm\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{inc}{inp}{tar}\olsection{The Undefinability of Truth}The notion of \emph{definability} depends on having a formal semanticsfor the language of arithmetic.  We have described a set of formulasand sentences in the language of arithmetic. The ``intendedinterpretation'' is to read such sentences as making assertions aboutthe natural numbers, and such an assertion can be true or false. Let$\Struct{N}$ be the !!{structure} with domain $\Nat$ and the standardinterpretation for the symbols in the language of arithmetic.  Then$\Sat{N}{!A}$ means ``$!A$ is true in the standard interpretation.''\begin{defn}A relation $R(x_1,\dots,x_k)$ of natural numbers is \emph{definable}in $\Struct{N}$ if and only if there is a formula $!A(x_1,\dots,x_k)$in the language of arithmetic such that for every $n_1,\dots,n_k$,$R(n_1,\dots,n_k)$ if and only if $\Sat{N}{!A(\num n_1,\dots,\num  n_k)}$.\end{defn}Put differently, a relation is definable in $\Struct{N}$ if andonly if it is representable in the theory $\Th{TA}$, where $\Th{TA} =\Setabs{!A}{\Sat{N}{!A}}$ is the set of true sentences ofarithmetic. (If this is not immediately clear to you, you should goback and check the definitions and convince yourself that this is thecase.)\begin{lem}Every computable relation is definable in~$\Struct{N}$.\end{lem}\begin{proof}It is easy to check that the formula representing a relation in$\Th{Q}$ defines the same relation in $\Struct{N}$. \end{proof}Now one can ask, is the converse also true?  That is, is everyrelation definable in~$\Struct{N}$ computable? The answer is no. Forexample:\begin{lem}The halting relation is definable in $\Struct{N}$.\end{lem}\begin{proof}Recall that the Kleene normal form theorem states that every partialcomputable function~$f$ has an index~$e$ such that $f(x) =U(\umin{s}{T(e,x,s)})$ for all $x \in \Nat$, where $U$ and $T$ areprimitive recursive and therefore total. Thus, $f(x)$ is defined(i.e., the computation halts) iff there is an~$s$ such that $T(e,x,s)$holds.Now let $H$ be the halting relation, i.e.,\[H = \Setabs{\tuple{e,x}}{\lexists[s][T(e, x, s)]}.\]Let $!D_T$ define $T$ in $\Struct{N}$. Then\[H = \Setabs{\tuple{e,x}}{\Sat{N}{\lexists[s][!D_T(\num e, \num x, s)]}},\]so $\lexists[s][!D_T(z, x, s)]$ defines~$H$ in $\Struct{N}$. \end{proof}\begin{prob}Show that $Q(n) \defiff n \in \Setabs{\Gn{!A}}{\Th{Q} \Proves !A}$ is  definable in arithmetic.\end{prob}What about $\Th{TA}$ itself? Is it definable in arithmetic? Thatis: is the set $\Setabs{\Gn{!A}}{\Sat{N}{!A}}$ definable inarithmetic? Tarski's theorem answers this in the negative.\begin{thm}\ollabel{thm:tarski}The set of true !!{sentence}s of arithmetic is not definable in arithmetic.\end{thm}\begin{proof} Suppose $!D(x)$ defined it, i.e., $\Sat{N}{!A}$ iff$\Sat{N}{!D(\gn{!A})}$. By the fixed-point lemma, there is a formula$!A$ such that $\Th{Q} \Proves !A \liff \lnot !D(\gn{!A})$, and hence$\Sat{N}{!A \liff \lnot !D(\gn{!A})}$. But then $\Sat{N}{!A}$ if andonly if $\Sat{N}{\lnot !D(\gn{!A})}$, which contradicts the fact that$!D(y)$ is supposed to define the set of true statements ofarithmetic.  \end{proof}Tarski applied this analysis to a more general philosophical notion oftruth. Given any language $L$, Tarski argued that an adequate notionof truth for $L$ would have to satisfy, for each sentence $X$,\begin{quote}`$X$' is true if and only if $X$.\end{quote}Tarski's oft-quoted example, for English, is the sentence\begin{quote}`Snow is white' is true if and only if snow is white.\end{quote}However, for any language strong enough to represent the diagonalfunction, and any linguistic predicate $T(x)$, we can construct asentence $X$ satisfying ``$X$ if and only if not $T(\text{`$X$'})$.''Given that we do not want a truth predicate to declare some sentencesto be both true and false, Tarski concluded that one cannot specify atruth predicate for all sentences in a language without, somehow,stepping outside the bounds of the language. In other words, a thetruth predicate for a language cannot be defined in the languageitself.\end{document}

Source-census fragment evidence

The complete original formula is shown in Read and Explore. These immutable census fragments are retained for traceability.

Census fragment projected-formula-0020669 — source evidence only
<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" data-expression-id="expr-eb56b2300ad56d34" data-source-fragment="incomplete_source_fragment" data-fragment-kind="nested_inline_math_census_prefix"><semantics><mrow><merror><mtext>Source fragment ends at the opening quotation inside the truth predicate.</mtext></merror><mrow><mi>T</mi><mo>(</mo><mtext>‘</mtext></mrow></mrow><annotation encoding="application/x-tex">T(\text{`</annotation></semantics></math>
Census fragment projected-formula-0020670 — source evidence only
<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" data-expression-id="expr-f4fd7f5ee62c4c18" data-source-fragment="incomplete_source_fragment" data-fragment-kind="nested_inline_math_census_suffix"><semantics><mrow><merror><mtext>Source fragment supplies the closing quotation and predicate parenthesis.</mtext></merror><mrow><mtext>’</mtext><mo>)</mo></mrow></mrow><annotation encoding="application/x-tex">&#x27;})</annotation></semantics></math>