{"id":204,"date":"2015-05-16T04:25:38","date_gmt":"2015-05-16T04:25:38","guid":{"rendered":"http:\/\/aristotle2digital.blogwyrm.com\/?p=204"},"modified":"2021-11-25T21:11:22","modified_gmt":"2021-11-26T02:11:22","slug":"godels-theorem-general-notions","status":"publish","type":"post","link":"https:\/\/aristotle2digital.blogwyrm.com\/?p=204","title":{"rendered":"G\u00f6del\u2019s Theorem \u2013 General Notions"},"content":{"rendered":"<style>\ntable, th, td {<br \/>\nborder: 1px solid black;<br \/>\nborder-collapse: collapse;<br \/>\n}<br \/>\nth { text-align: center !important; }<br \/>\n<\/style>\n<p>As I mentioned in <a href=\"http:\/\/aristotle2digital.blogwyrm.com\/2015\/05\/09\/turing-godel-and-the-universe\/\">last week\u2019s blog<\/a>, I was encouraged by Casti\u2019s chapter on the Halting Theorem and questions of undecidability in logic and computing.\u00a0 In fact, I was inspired enough that I resolved have another go at studying G\u00f6del\u2019s theorem.<\/p>\n<p>To give some background, many years ago I came across \u2018G\u00f6del, Escher, and Bach: An Eternal Golden Braid\u2019 by Douglas Hofstadter. While I appreciate that his work is considered a classic, I found it difficult and ponderous.\u00a0\u00a0 Its over 700 pages of popularized work did little to nothing to really sink home G\u00f6del\u2019s theorem and the connections to Turing and Church.\u00a0 What\u2019s more, Hofstadter seems to say (it\u2019s difficult to tell exactly as he mixes and muddles many concepts) that G\u00f6del\u2019s work supports his ideas that consciousness can emerge from purely mechanistic means at the lowest level.\u00a0 This point always seemed dodgy to me.\u00a0 Especially since Hofstadter left me with the impression that G\u00f6del\u2019s theorem showed a fundamental lack in basic logic not an emergent property.<\/p>\n<p>For this go around, I decided that smaller was better and picked up the slim work entitled \u2018G\u00f6del\u2019s Theorem\u2019 by Nagel and Newman.\u00a0 What a difference a serious exposition makes.\u00a0 Nagel and Newman present all the essential flavor and some of the machinery that G\u00f6del used in a mere 102 pages.<\/p>\n<p>Note that formal logic is not one of my strong suits and the intellectual terrain was rocky and difficult.\u00a0 Nonetheless, Nagel and Newman\u2019s basic program was laid out well and consisted of the following points.<\/p>\n<p>To start, the whole thing was initiated by David Hilbert, whose <a href=\"http:\/\/en.wikipedia.org\/wiki\/Hilbert%27s_second_problem\">Second Problem<\/a>, challenged the mathematical community to provide absolute proof of the consistency of a formal system (specifically arithmetic) based solely on its structure.\u00a0 This idea of absolute proof stands in contrast to a relative proof where the system is question is put into relation to another system, whose validity and consistency is accepted.\u00a0 If the relation between the two is faithful, then the consistency of the second system carries over or is imparted to the first.<\/p>\n<p>Hilbert was unsatisfied by the relative approach as it depended on some system being accepted at face value as being consistent and finding such a system was a tricky proposition.<\/p>\n<p>The preferred way to implement an absolute proof is to start by stripping away all meaning from the system and to deal only with abstract symbols and a mechanistic way of manipulating these symbols using well-defined rules.\u00a0 The example that Nagel and Newman present is the sentential calculus slightly adapted from the \u2018Principia Mathematica\u2019 by Whitehead and Russell.\u00a0 The codification of the formal logic system depends on symbols that fall into two classes: variables and constant signs.\u00a0 Variables, denoted by letters, stand for statements.\u00a0 For example, \u2018p\u2019 could stand for \u2018all punters kick the football far\u2019.\u00a0 There are six constant signs with the mapping<\/p>\n<div style=\"background-color: #ff6666; border: solid 1px black;\">\n<table>\n<tbody>\n<tr>\n<td width=\"312\">~<\/td>\n<td width=\"312\">Not<\/td>\n<\/tr>\n<tr>\n<td width=\"312\">$\\vee$<\/td>\n<td width=\"312\">Or<\/td>\n<\/tr>\n<tr>\n<td width=\"312\">$\\supset$<\/td>\n<td width=\"312\">If\u2026 Then\u2026<\/td>\n<\/tr>\n<tr>\n<td width=\"312\">$\\cdot$<\/td>\n<td width=\"312\">And<\/td>\n<\/tr>\n<tr>\n<td width=\"312\">(<\/td>\n<td width=\"312\">Left-hand punctuation<\/td>\n<\/tr>\n<tr>\n<td width=\"312\">)<\/td>\n<td width=\"312\">Right-hand punctuation<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<\/div>\n<p>The idea is then to map all content-laden statements, like \u2018If either John or Tim are late then we will miss the bus!\u2019, to formal statements like ( (J $\\vee$ T ) $\\supset$ B) with all meaning and additional fluff removed.\u00a0 Two rules for manipulating the symbols, the Rule of Substitution and the Rule of Detachment, are adopted and four axioms are used as starting points.<\/p>\n<p>In using this system, one has to sharpen one\u2019s thinking to be able to distinguish between statements in the system (mathematical statements like \u20182 &gt; 1\u2019) from statements about the system (meta-mathematical statements like \u20182&gt;1\u2019 is true or that the \u2018&gt;\u2019 symbol is an infix operator).\u00a0 One must also be careful to note the subtle differences between the symbol \u20180\u2019, the number 0, and the concept of zero meaning nothing.<\/p>\n<p>The advantage of this approach is that the proofs are cleaner, especially when there are many symbols.\u00a0 The disadvantage is that it takes time and effort to be able to work in this language.<\/p>\n<p>The consistency of the formal system is shown when there is at least one formal statement (or formula) that cannot be derived from the axioms.\u00a0 The reason for this is complicated and I don\u2019t have a good grasp on it but it goes something like this.\u00a0 The following formula \u2018p $\\supset$ (~ p $\\supset$ q)\u2019 can be derived in the sentential calculus.\u00a0 If the statements S and ~S are both deducible then any statement you like can be derived from the axioms (via the Rules of Substitution and Detachment) and the system is clearly inconsistent.\u00a0 In the words of Nagel and Newman:<\/p>\n<div style=\"background-color: #ff6666; border: solid 1px black;\">\u2018The task, therefore, is to show that there is at least one formula that cannot be derived from the axioms.\u2019 [p51]<\/div>\n<p>For the sentential calculus, they point out that the formula \u2018p $\\vee$ q\u2019 fits the bill since it is a formula, it doesn\u2019t follow from the axiom.\u00a0 Thus this system is consistent. Note that there is no truth statement attached to this formula.\u00a0 The observation simply means that \u2018p $\\vee$ q\u2019 can\u2019t be obtained from the axioms by a mechanical manipulation.\u00a0 They present this argument in their chapter titled \u2018An Example of a Successful Absolute Proof of Consistency\u2019.<\/p>\n<p>Well despite that lofty achievement, they go on to show how G\u00f6del took a similar approach and mostly ended any hope for a proof of absolute consistency in formal systems with a great deal more complexity.\u00a0 G\u00f6del used as his symbols the numerals and as his rules the basic operations of arithmetic and, in particular, the arithmetic of prime numbers. Using an ingenious mapping from of the variables and constant symbols to numbers, he not only could encode the structure of the formal system itself, he could also encode statements about the formal system as well (meta-mathematics).\u00a0 In the language of Hofstadter, these are self-referential statements, although Nagel and Newman don\u2019t use this term.<\/p>\n<p>Using this approach, G\u00f6del was able to prove that there is no absolute proof of consistency.\u00a0 At best, the system can say about itself that it is either incomplete or inconsistent.\u00a0 If the system is incomplete, there are true statements that are not part of the axioms and that cannot be derived from them.\u00a0 Enlarging the set of axioms to include them doesn\u2019t work since they presence begets new unprovable truths. If the system is inconsistent, then everything is \u2018true\u2019 as discussed above.<\/p>\n<p>Nagel and Newman leave the reader with come final thoughts that are worth contemplation.\u00a0 On the hope that Hilbert\u2019s program can be successfully completed they have this to say<\/p>\n<div style=\"background-color: #ff6666; border: solid 1px black;\">\u2018These conclusions show that the prospect of finding for every deductive system an absolute proof of consistency that satisfies the <a href=\"http:\/\/en.wikipedia.org\/wiki\/Finitism\">finitistic<\/a> requirement\u2019s of Hilbert\u2019s proposal, though not logically impossible, is most unlikely.\u2019<\/div>\n<p>They also comment on the possibility of proving consistency from an outside-looking-in approach using meta-mathematical techniques when they say<\/p>\n<div style=\"background-color: #ff6666; border: solid 1px black;\">\u2018[W]hether an all-inclusive definition of mathematical or logical truth can be devised, and whether, as G\u00f6del himself appears to believe, only a thoroughgoing philosophical \u2018realism\u2019 of the ancient Platonic type can supply an adequate definition, are problems still under debate\u2026\u2019<\/div>\n<p>Finally, they have this to say about artificial intelligence (although that term wasn\u2019t in vogue at the time they published<\/p>\n<div style=\"background-color: #ff6666; border: solid 1px black;\">\u2018[T]he brain appears to embody a structure of rules of operation which is far more powerful than the structure of currently conceived artificial machines.\u00a0 There is no immediate prospect of replacing the human mind by robots.\u2019<\/div>\n<p>And there you have it. A whirlwind tour of G\u00f6del\u2019s theorem with a surprise appearance of the philosophy from antiquity and the ideas about artificial intelligence.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>As I mentioned in last week\u2019s blog, I was encouraged by Casti\u2019s chapter on the Halting Theorem and questions of undecidability in logic and computing.\u00a0 In fact, I was inspired&#8230; <a class=\"read-more-button\" href=\"https:\/\/aristotle2digital.blogwyrm.com\/?p=204\">Read more &gt;<\/a><\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[1],"tags":[],"class_list":["post-204","post","type-post","status-publish","format-standard","hentry","category-uncategorized"],"_links":{"self":[{"href":"https:\/\/aristotle2digital.blogwyrm.com\/index.php?rest_route=\/wp\/v2\/posts\/204","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/aristotle2digital.blogwyrm.com\/index.php?rest_route=\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/aristotle2digital.blogwyrm.com\/index.php?rest_route=\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/aristotle2digital.blogwyrm.com\/index.php?rest_route=\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/aristotle2digital.blogwyrm.com\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=204"}],"version-history":[{"count":0,"href":"https:\/\/aristotle2digital.blogwyrm.com\/index.php?rest_route=\/wp\/v2\/posts\/204\/revisions"}],"wp:attachment":[{"href":"https:\/\/aristotle2digital.blogwyrm.com\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=204"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/aristotle2digital.blogwyrm.com\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=204"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/aristotle2digital.blogwyrm.com\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=204"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}