<div class="xblock xblock-public_view xblock-public_view-vertical" data-usage-id="block-v1:MITx+24.118x+2T2020+type@vertical+block@f2c7dc12f8b54955b8507a51751c4b10" data-graded="False" data-runtime-class="LmsRuntime" data-course-id="course-v1:MITx+24.118x+2T2020" data-block-type="vertical" data-request-token="25f39d94fe3e11ee8e0c026cc65ec0d9" data-has-score="False" data-runtime-version="1" data-init="VerticalStudentView">
<h2 class="hd hd-2 unit-title">Outline of the Proof</h2>
<div class="vert-mod">
<div class="vert vert-0" data-id="block-v1:MITx+24.118x+2T2020+type@video+block@5e1a9a4e4e0d4d988e22780f88f466f5">
<div class="xblock xblock-public_view xblock-public_view-video xmodule_display xmodule_VideoBlock" data-usage-id="block-v1:MITx+24.118x+2T2020+type@video+block@5e1a9a4e4e0d4d988e22780f88f466f5" data-graded="False" data-runtime-class="LmsRuntime" data-course-id="course-v1:MITx+24.118x+2T2020" data-block-type="video" data-request-token="25f39d94fe3e11ee8e0c026cc65ec0d9" data-has-score="False" data-runtime-version="1" data-init="XBlockToXModuleShim">
<script type="json/xblock-args" class="xblock-json-init-args">
{"xmodule-type": "Video"}
</script>
<h3 class="hd hd-2">Video: the Basic Proof</h3>
<div
id="video_5e1a9a4e4e0d4d988e22780f88f466f5"
class="video closed"
data-metadata='{"end": 0.0, "speed": null, "ytTestTimeout": 1500, "publishCompletionUrl": "/courses/course-v1:MITx+24.118x+2T2020/xblock/block-v1:MITx+24.118x+2T2020+type@video+block@5e1a9a4e4e0d4d988e22780f88f466f5/handler/publish_completion", "ytApiUrl": "https://www.youtube.com/iframe_api", "showCaptions": "true", "streams": "1.00:8YgBZWF5D1I", "poster": null, "saveStateEnabled": false, "start": 0.0, "completionPercentage": 0.95, "transcriptAvailableTranslationsUrl": "/courses/course-v1:MITx+24.118x+2T2020/xblock/block-v1:MITx+24.118x+2T2020+type@video+block@5e1a9a4e4e0d4d988e22780f88f466f5/handler/transcript/available_translations", "autoplay": false, "transcriptLanguages": {"en": "English"}, "autohideHtml5": false, "transcriptTranslationUrl": "/courses/course-v1:MITx+24.118x+2T2020/xblock/block-v1:MITx+24.118x+2T2020+type@video+block@5e1a9a4e4e0d4d988e22780f88f466f5/handler/transcript/translation/__lang__", "ytMetadataEndpoint": "", "generalSpeed": 1.0, "lmsRootURL": "https://openlearninglibrary.mit.edu", "autoAdvance": false, "completionEnabled": false, "savedVideoPosition": 0.0, "saveStateUrl": "/courses/course-v1:MITx+24.118x+2T2020/xblock/block-v1:MITx+24.118x+2T2020+type@video+block@5e1a9a4e4e0d4d988e22780f88f466f5/handler/xmodule_handler/save_user_state", "captionDataDir": null, "sources": [], "transcriptLanguage": "en", "recordedYoutubeIsAvailable": true, "prioritizeHls": false, "duration": 0.0}'
data-bumper-metadata='null'
data-autoadvance-enabled="False"
data-poster='null'
tabindex="-1"
>
<div class="focus_grabber first"></div>
<div class="tc-wrapper">
<div class="video-wrapper">
<span tabindex="0" class="spinner" aria-hidden="false" aria-label="Loading video player"></span>
<span tabindex="-1" class="btn-play fa fa-youtube-play fa-2x is-hidden" aria-hidden="true" aria-label="Play video"></span>
<div class="video-player-pre"></div>
<div class="video-player">
<div id="5e1a9a4e4e0d4d988e22780f88f466f5"></div>
<h4 class="hd hd-4 video-error is-hidden">No playable video sources found.</h4>
<h4 class="hd hd-4 video-hls-error is-hidden">
Your browser does not support this video format. Try using a different browser.
</h4>
</div>
<div class="video-player-post"></div>
<div class="closed-captions"></div>
<div class="video-controls is-hidden">
<div>
<div class="vcr"><div class="vidtime">0:00 / 0:00</div></div>
<div class="secondary-controls"></div>
</div>
</div>
</div>
</div>
<div class="focus_grabber last"></div>
<h3 class="hd hd-4 downloads-heading sr" id="video-download-transcripts_5e1a9a4e4e0d4d988e22780f88f466f5">Downloads and transcripts</h3>
<div class="wrapper-downloads" role="region" aria-labelledby="video-download-transcripts_5e1a9a4e4e0d4d988e22780f88f466f5">
<div class="wrapper-download-transcripts">
<h4 class="hd hd-5">Transcripts</h4>
<ul class="list-download-transcripts">
<li class="transcript-option">
<a class="btn btn-link" href="/courses/course-v1:MITx+24.118x+2T2020/xblock/block-v1:MITx+24.118x+2T2020+type@video+block@5e1a9a4e4e0d4d988e22780f88f466f5/handler/transcript/download" data-value="srt">Download SubRip (.srt) file</a>
</li>
<li class="transcript-option">
<a class="btn btn-link" href="/courses/course-v1:MITx+24.118x+2T2020/xblock/block-v1:MITx+24.118x+2T2020+type@video+block@5e1a9a4e4e0d4d988e22780f88f466f5/handler/transcript/download" data-value="txt">Download Text (.txt) file</a>
</li>
</ul>
</div>
</div>
</div>
</div>
</div>
<div class="vert vert-1" data-id="block-v1:MITx+24.118x+2T2020+type@video+block@5f2dd9de94f1488c8e5a31b3e6aabd8f">
<div class="xblock xblock-public_view xblock-public_view-video xmodule_display xmodule_VideoBlock" data-usage-id="block-v1:MITx+24.118x+2T2020+type@video+block@5f2dd9de94f1488c8e5a31b3e6aabd8f" data-graded="False" data-runtime-class="LmsRuntime" data-course-id="course-v1:MITx+24.118x+2T2020" data-block-type="video" data-request-token="25f39d94fe3e11ee8e0c026cc65ec0d9" data-has-score="False" data-runtime-version="1" data-init="XBlockToXModuleShim">
<script type="json/xblock-args" class="xblock-json-init-args">
{"xmodule-type": "Video"}
</script>
<h3 class="hd hd-2">Video: How to Prove the Lemma</h3>
<div
id="video_5f2dd9de94f1488c8e5a31b3e6aabd8f"
class="video closed"
data-metadata='{"end": 0.0, "speed": null, "ytTestTimeout": 1500, "publishCompletionUrl": "/courses/course-v1:MITx+24.118x+2T2020/xblock/block-v1:MITx+24.118x+2T2020+type@video+block@5f2dd9de94f1488c8e5a31b3e6aabd8f/handler/publish_completion", "ytApiUrl": "https://www.youtube.com/iframe_api", "showCaptions": "true", "streams": "1.00:B9IDBn3UTQA", "poster": null, "saveStateEnabled": false, "start": 0.0, "completionPercentage": 0.95, "transcriptAvailableTranslationsUrl": "/courses/course-v1:MITx+24.118x+2T2020/xblock/block-v1:MITx+24.118x+2T2020+type@video+block@5f2dd9de94f1488c8e5a31b3e6aabd8f/handler/transcript/available_translations", "autoplay": false, "transcriptLanguages": {"en": "English"}, "autohideHtml5": false, "transcriptTranslationUrl": "/courses/course-v1:MITx+24.118x+2T2020/xblock/block-v1:MITx+24.118x+2T2020+type@video+block@5f2dd9de94f1488c8e5a31b3e6aabd8f/handler/transcript/translation/__lang__", "ytMetadataEndpoint": "", "generalSpeed": 1.0, "lmsRootURL": "https://openlearninglibrary.mit.edu", "autoAdvance": false, "completionEnabled": false, "savedVideoPosition": 0.0, "saveStateUrl": "/courses/course-v1:MITx+24.118x+2T2020/xblock/block-v1:MITx+24.118x+2T2020+type@video+block@5f2dd9de94f1488c8e5a31b3e6aabd8f/handler/xmodule_handler/save_user_state", "captionDataDir": null, "sources": [], "transcriptLanguage": "en", "recordedYoutubeIsAvailable": true, "prioritizeHls": false, "duration": 0.0}'
data-bumper-metadata='null'
data-autoadvance-enabled="False"
data-poster='null'
tabindex="-1"
>
<div class="focus_grabber first"></div>
<div class="tc-wrapper">
<div class="video-wrapper">
<span tabindex="0" class="spinner" aria-hidden="false" aria-label="Loading video player"></span>
<span tabindex="-1" class="btn-play fa fa-youtube-play fa-2x is-hidden" aria-hidden="true" aria-label="Play video"></span>
<div class="video-player-pre"></div>
<div class="video-player">
<div id="5f2dd9de94f1488c8e5a31b3e6aabd8f"></div>
<h4 class="hd hd-4 video-error is-hidden">No playable video sources found.</h4>
<h4 class="hd hd-4 video-hls-error is-hidden">
Your browser does not support this video format. Try using a different browser.
</h4>
</div>
<div class="video-player-post"></div>
<div class="closed-captions"></div>
<div class="video-controls is-hidden">
<div>
<div class="vcr"><div class="vidtime">0:00 / 0:00</div></div>
<div class="secondary-controls"></div>
</div>
</div>
</div>
</div>
<div class="focus_grabber last"></div>
<h3 class="hd hd-4 downloads-heading sr" id="video-download-transcripts_5f2dd9de94f1488c8e5a31b3e6aabd8f">Downloads and transcripts</h3>
<div class="wrapper-downloads" role="region" aria-labelledby="video-download-transcripts_5f2dd9de94f1488c8e5a31b3e6aabd8f">
<div class="wrapper-download-transcripts">
<h4 class="hd hd-5">Transcripts</h4>
<ul class="list-download-transcripts">
<li class="transcript-option">
<a class="btn btn-link" href="/courses/course-v1:MITx+24.118x+2T2020/xblock/block-v1:MITx+24.118x+2T2020+type@video+block@5f2dd9de94f1488c8e5a31b3e6aabd8f/handler/transcript/download" data-value="srt">Download SubRip (.srt) file</a>
</li>
<li class="transcript-option">
<a class="btn btn-link" href="/courses/course-v1:MITx+24.118x+2T2020/xblock/block-v1:MITx+24.118x+2T2020+type@video+block@5f2dd9de94f1488c8e5a31b3e6aabd8f/handler/transcript/download" data-value="txt">Download Text (.txt) file</a>
</li>
</ul>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
<div class="xblock xblock-public_view xblock-public_view-vertical" data-usage-id="block-v1:MITx+24.118x+2T2020+type@vertical+block@b1207fc8594e40b3b93ae50076cd280b" data-graded="False" data-runtime-class="LmsRuntime" data-course-id="course-v1:MITx+24.118x+2T2020" data-block-type="vertical" data-request-token="25f39d94fe3e11ee8e0c026cc65ec0d9" data-has-score="False" data-runtime-version="1" data-init="VerticalStudentView">
<h2 class="hd hd-2 unit-title">The Details</h2>
<div class="vert-mod">
<div class="vert vert-0" data-id="block-v1:MITx+24.118x+2T2020+type@html+block@f6ce2c0c1c2d4bdfaef24ab621449075">
<div class="xblock xblock-public_view xblock-public_view-html xmodule_display xmodule_HtmlBlock" data-usage-id="block-v1:MITx+24.118x+2T2020+type@html+block@f6ce2c0c1c2d4bdfaef24ab621449075" data-graded="False" data-runtime-class="LmsRuntime" data-course-id="course-v1:MITx+24.118x+2T2020" data-block-type="html" data-request-token="25f39d94fe3e11ee8e0c026cc65ec0d9" data-has-score="False" data-runtime-version="1" data-init="XBlockToXModuleShim">
<script type="json/xblock-args" class="xblock-json-init-args">
{"xmodule-type": "HTMLModule"}
</script>
<p><span style="font-family: 'book antiqua', palatino;">We are now in a position to prove our main result.</span></p>
<p style="padding-left: 30px;"><span style="font-family: 'book antiqua', palatino;"><strong>Gödel’s Incompleteness Theorem</strong></span><br /><span style="font-family: 'book antiqua', palatino;">Let <span class="math inline">\(\mathcal{L}\)</span> be a language rich enough for the <a href="/courses/course-v1:MITx+24.118x+2T2020/jump_to_id/2749e3650fb445d19ee671e1194f1e9e" target="[object Object]">Lemma of Section 10.1.2</a> to be provable (for example, <span class="math inline">\(\mathcal{L}\)</span> might be our simple language <span class="math inline">\(L\)</span>). Then no Turing Machine <span class="math inline">\(M\)</span> is such that when run on an empty input:</span></p>
<ol style="padding-left: 60px;">
<li>
<p><span style="font-family: 'book antiqua', palatino;"><span class="math inline">\(M\)</span> runs forever, outputting sentences of <span class="math inline">\(\mathcal{L}\)</span>;</span></p>
</li>
<li>
<p><span style="font-family: 'book antiqua', palatino;">every true sentence of <span class="math inline">\(\mathcal{L}\)</span> is eventually output by <span class="math inline">\(M\)</span>; and</span></p>
</li>
<li>
<p><span style="font-family: 'book antiqua', palatino;">no false sentence of <span class="math inline">\(\mathcal{L}\)</span> is ever output by <span class="math inline">\(M\)</span>.</span></p>
</li>
</ol>
<p><span style="font-family: 'book antiqua', palatino;">The proof proceeds by <em>reductio</em>. </span></p>
<p><span style="font-family: 'book antiqua', palatino;">We will assume that <span class="math inline">\(M\)</span> is a Turing Machine that outputs all and only the true sentences of <span class="math inline">\(\mathcal{L}\)</span>, and show that <span class="math inline">\(M\)</span>’s program can be used as a subroutine to construct a Turing Machine <span class="math inline">\(M^H\)</span> which computes the Halting Function, which is impossible, since the Halting Function is not Turing-computable (as we saw in Chapter 9). </span></p>
<p><span style="font-family: 'book antiqua', palatino;">We will proceed in two steps. First, we will verify that if <span class="math inline">\(M\)</span> existed, it could be used to construct <span class="math inline">\(M^H\)</span>. We will then verify that <span class="math inline">\(M^H\)</span> would compute the Halting Function, if it existed.</span></p>
<h4><span style="font-family: 'book antiqua', palatino;">Step 1</span></h4>
<p><span style="font-family: 'book antiqua', palatino;">Here is how to construct \(M^H\), on the assumption that \(M\) exists. (Assume that \(M^H\)'s input is a sequence of \(k\) ones.)<br /></span></p>
<ul>
<li><span style="font-family: 'book antiqua', palatino;">\(M^H\) starts by running \(M\)'s program as a subroutine. Each time \(M\) outputs a sentence, \(M^H\) proceeds as follows:</span></li>
</ul>
<blockquote>
<ul>
<li><span style="font-family: 'book antiqua', palatino;">If the sentence is "\(\mbox{Halt}(k)\)", \(M^H\) deletes everything on the tape, prints a one, and halts. </span></li>
<li><span style="font-family: 'book antiqua', palatino;">If the sentence is "\(\neg \mbox{Halt}(k)\)", \(M^H\) deletes everything on the tape, and halts. </span></li>
<li><span style="font-family: 'book antiqua', palatino;">Otherwise, \(M^H\) allows \(M\) to keep going.</span></li>
</ul>
</blockquote>
<h4><span style="font-family: 'book antiqua', palatino;">Step 2</span></h4>
<p><span style="font-family: 'book antiqua', palatino;">Let us verify that <span class="math inline">\(M^H\)</span> would compute the Halting Function, if it existed. We will verify, in other words, that <span class="math inline">\(M^H\)</span> outputs a one if the <span class="math inline">\(k\)</span>th Turing Machine halts, and a zero otherwise.</span></p>
<ul>
<li>
<p><span style="font-family: 'book antiqua', palatino;">Suppose, first, that the <span class="math inline">\(k\)</span>th Turing Machine halts given input <span class="math inline">\(k\)</span>. Then our Lemma guarantees that “<span class="math inline">\(\mbox{Halt}(k)\)</span>" is true. Since <span class="math inline">\(M\)</span> will eventually output every true sentence of <span class="math inline">\(\mathcal{L}\)</span>, this means that <span class="math inline">\(M\)</span> will eventually output “<span class="math inline">\(\mbox{Halt}(k)\)</span>". And since <span class="math inline">\(M\)</span> will never output any falsehood, it will never output “<span class="math inline">\(\neg\mbox{Halt}(k)\)</span>". So the construction of <span class="math inline">\(M^H\)</span> guarantees that <span class="math inline">\(M^H\)</span> will output a one.</span></p>
</li>
<li>
<p><span style="font-family: 'book antiqua', palatino;">Now suppose that the <span class="math inline">\(k\)</span>th Turing Machine does not halt given input <span class="math inline">\(k\)</span>. Then our Lemma guarantees that “<span class="math inline">\(\neg \mbox{Halt}(k)\)</span>" is true. Since <span class="math inline">\(M\)</span> will eventually output every true sentence of <span class="math inline">\(\mathcal{L}\)</span>, this means that <span class="math inline">\(M\)</span> will eventually output “<span class="math inline">\(\neg\mbox{Halt}(k)\)</span>". And since <span class="math inline">\(M\)</span> will never output any falsehood, it will never print out “<span class="math inline">\(\mbox{Halt}(k)\)</span>". So <span class="math inline">\(M^H\)</span> will output a zero.</span></p>
</li>
</ul>
<p><span style="font-family: 'book antiqua', palatino;">In summary, we have seen that if <span class="math inline">\(M\)</span> existed, <span class="math inline">\(M^H\)</span> would exist too. And we have seen that <span class="math inline">\(M^H\)</span> would compute the Halting Function, which we know to be impossible. So <span class="math inline">\(M\)</span> cannot exist. </span></p>
<p><span style="font-family: 'book antiqua', palatino;">This completes our proof of Gödel’s Thoerem.</span></p>
<p></p>
</div>
</div>
</div>
</div>
<div class="xblock xblock-public_view xblock-public_view-vertical" data-usage-id="block-v1:MITx+24.118x+2T2020+type@vertical+block@6c20fbcd52b24b669b017e4683dbba78" data-graded="False" data-runtime-class="LmsRuntime" data-course-id="course-v1:MITx+24.118x+2T2020" data-block-type="vertical" data-request-token="25f39d94fe3e11ee8e0c026cc65ec0d9" data-has-score="False" data-runtime-version="1" data-init="VerticalStudentView">
<h2 class="hd hd-2 unit-title">A different formulation of the theorem</h2>
<div class="vert-mod">
<div class="vert vert-0" data-id="block-v1:MITx+24.118x+2T2020+type@html+block@3909ce0d697e44e0a7a511e05a173188">
<div class="xblock xblock-public_view xblock-public_view-html xmodule_display xmodule_HtmlBlock" data-usage-id="block-v1:MITx+24.118x+2T2020+type@html+block@3909ce0d697e44e0a7a511e05a173188" data-graded="False" data-runtime-class="LmsRuntime" data-course-id="course-v1:MITx+24.118x+2T2020" data-block-type="html" data-request-token="25f39d94fe3e11ee8e0c026cc65ec0d9" data-has-score="False" data-runtime-version="1" data-init="XBlockToXModuleShim">
<script type="json/xblock-args" class="xblock-json-init-args">
{"xmodule-type": "HTMLModule"}
</script>
<p><span style="font-family: 'book antiqua', palatino;">In the preceding section we proved that it is impossible to build a Turing Machine that outputs all and only the true statements of a rich enough arithmetical language. </span></p>
<p><span style="font-family: 'book antiqua', palatino;">That is one formulation of Gödel’s Theorem. </span></p>
<p><span style="font-family: 'book antiqua', palatino;">Here is another:</span></p>
<p style="padding-left: 30px;"><span style="font-family: 'book antiqua', palatino;"><strong>Gödel’s Incompleteness Theorem</strong></span><br /><span style="font-family: 'book antiqua', palatino;">No axiomatization of elementary arithmetic (in a rich enough language) can be both consistent and complete.</span></p>
<p><span style="font-family: 'book antiqua', palatino;">In this subsection we’ll see what this means, and how it can be proved on the basis of the version of the result we have been discussing so far (assuming a particular understanding of “complete”).</span></p>
<h4><span style="font-family: 'book antiqua', palatino;">Axiomatization</span></h4>
<p><span style="font-family: 'book antiqua', palatino;">Let me start with the notion of an axiomatization. </span></p>
<p><span style="font-family: 'book antiqua', palatino;">We’ve talked a fair amount about a language in which to express arithmetical claims. But we haven’t said much about how to <em>prove</em> the arithmetical claims that are expressible in that language. </span></p>
<p><span style="font-family: 'book antiqua', palatino;">An <strong>axiomatization</strong> of arithmetic is a system for proving things within an arithmetical language. It consists of two different components: (a) a set of axioms, and (b) a set of rules of inference:</span></p>
<ul>
<li>
<p><span style="font-family: 'book antiqua', palatino;">An <strong>axiom</strong> is a sentence of the language that one chooses to treat as “basic", and on the basis of which other sentences of the language are supposed to be proved. One might, for example, treat “every number has a successor" (in symbols: "<span class="math inline">\(\forall x_1\exists x_2(x_2=x_1+1)\)</span>") as an axiom.</span></p>
</li>
<li>
<p><span style="font-family: 'book antiqua', palatino;">A <strong>rule of inference</strong> is a rule for inferring some sentences of the language from others—a rule which is such as to guarantee that if one uses true sentences as input, one will always get true sentences as output. An example of a rule of inference is <em>modus ponens</em>: the rule that tells us that one can always infer the sentence <span class="math inline">\(\psi\)</span> from the sentences <span class="math inline">\(\phi\)</span> and “if <span class="math inline">\(\phi\)</span>, then <span class="math inline">\(\psi\)</span>".</span></p>
</li>
</ul>
<p><span style="font-family: 'book antiqua', palatino;">In choosing an axiomatization, one is free to pick any list of axioms and rules of inference one likes, as long as one’s list is Turing-computable. (In other words, it must be possible to program a Turing Machine to determine what counts as an axiom and when one sentence follows from another by a rule of inference.)</span></p>
<h4><span style="font-family: 'book antiqua', palatino;">Provability, completeness and consistency</span></h4>
<p><span style="font-family: 'book antiqua', palatino;">Once one has an axiomatization for a given language, one can introduce a notion of provability for that language. </span></p>
<p><span style="font-family: 'book antiqua', palatino;">A sentence <span class="math inline">\(S\)</span> is <strong>provable</strong> on the basis of a given axiomatization if there is a finite sequence of sentences of the language with the following two properties:</span></p>
<ul>
<li>
<p><span style="font-family: 'book antiqua', palatino;">Every member of the sequence is either an axiom, or something that results from previous members of the sequence by applying a rule of inference.</span></p>
</li>
<li>
<p><span style="font-family: 'book antiqua', palatino;">The last member of the sequence is <span class="math inline">\(S\)</span>.</span></p>
</li>
</ul>
<p><span style="font-family: 'book antiqua', palatino;">We can now say what it is for an axiomatization to be complete and consistent. </span></p>
<p><span style="font-family: 'book antiqua', palatino;">For an axiomatization to be <strong>complete</strong> is for every true sentence of the language to be provable on the basis of that axiomatization. </span></p>
<p><span style="font-family: 'book antiqua', palatino;">For it to be <strong>consistent</strong> is for it never to be the case that both a sentence of the language and its negation are provable on the basis of that axiomatization.</span></p>
<p><span style="font-family: 'book antiqua', palatino;">Notice that an arithmetical falsehood can never be proved on the basis of a complete and consistent axiomatization. To see this, suppose for <em>reductio</em> that a complete and consistent axiomatization does entail some false sentence <span class="math inline">\(S\)</span>. Since <span class="math inline">\(S\)</span> is false, its negation must be true. And since the axiomatization is complete, the negation of <span class="math inline">\(s\)</span> must be provable on the basis of that axiomatization. So both a sentence and its negation must be provable on the basis of that axiomatization. So the axiomatization fails to be consistent.</span></p>
<p><span style="font-family: 'book antiqua', palatino;">(Warning: Gödel’s Theorem is sometimes formulated using a slightly different notion of completeness, according to which an axiomatization is complete if it proves every sentence or its negation. The result holds on either characterization of completeness, but the version I use here has the advantage of being easily provable on the basis of our original formulation of the theorem.)</span></p>
<h4><span style="font-family: 'book antiqua', palatino;">The proof</span></h4>
<p><span style="font-family: 'book antiqua', palatino;">Let us now use the claim that no Turing Machine can output all and only arithmetical truths (of a rich enough language) to prove that no axiomatization of arithmetic (in that language) can be both consistent and complete.</span></p>
<p><span style="font-family: 'book antiqua', palatino;">We proceed by <em>reductio</em>. We will assume that we have a consistent and complete axiomatization of arithmetic in a suitable language, and use this assumption to build a Turing Machine that outputs all and only the true sentences of that language. Since we know that there can be no such Turing Machine, our assumption must be false.</span></p>
<p><span style="font-family: 'book antiqua', palatino;">The first thing to note is that it is possible to code each finite sequence of sentences of our arithmetical language as a natural number. To see this, note that one can code each symbol of the language as a natural number. Since each sentence is a finite sequence of symbols, and since we know how to code finite sequences of natural numbers as natural numbers, this means that we can code each sentence as a natural number. And once sentences have been coded as natural numbers, we can repeat the process to code each finite sequence of sentences as a natural number.</span></p>
<p><span style="font-family: 'book antiqua', palatino;">The next observation is that one can program a Turing Machine that outputs all and only the sentences of our language that can be proved on the basis of our axiomatization. The machine proceeds by going through the natural numbers in order. At each stage, the machine determines whether the relevant number codes a sequence of sentences. If it doesn’t, the machine goes on to the next number. If it does, the machine proceeds to determine whether the sequence constitutes a proof. (We know that this is possible because we know that the axioms and inference rules of our system are Turing-computable.) If the sequence does constitute a proof, the machine outputs the last member of the sequence (which is the conclusion of the proof). The machine then goes on to consider the next natural number.</span></p>
<p><span style="font-family: 'book antiqua', palatino;">Notice, finally, that if our axiomatization is consistent and complete, then a Turing Machine that outputs all and only the provable sentences of our arithmetical language must output all and only the true sentences of our arithmetical language. But we have shown this to be impossible for languages like <span class="math inline">\(L\)</span>, which are rich enough to express the Halting Function. We conclude that an axiomatization for such a language cannot be both consistent and complete.</span></p>
<p></p>
</div>
</div>
</div>
</div>
© All Rights Reserved