The basic building blocks of the logic are variables. Already this is a bit different from what you’re probably used to in a logic. When we think of logic, we usually consider predicates to be a fundamental thing. In this logic, they’re not. A predicate is just a shorthand for a set, and a set is represented by a variable.<\/p>\n
Variables are stratified<\/em>. Again, it helps to remember where Russell and Whitehead were coming from when they were writing the Principia. One of their basic motivations was avoiding self-referential statements like Russell’s paradox. In order to prevent that, they thought that they could create a stratified logic, where on each level, you could only reason about objects from the level below. A first-order predicate would be a second-level object could only reason about first level objects. A second-order predicate would be a third-level object which could reason about second-level objects. No predicate could ever reason about itself or anything on its on level. This leveling property is a fundamental property built into their logic. The way the levels work is:<\/p>\n Using variables, we can form simple atomic expressions, which in Gödel’s terminology are called signs<\/em>. As with variables, the signs are divided into stratified levels: <\/p>\n Once you have signs, you can assemble the basic signs into formulae. Gödel explained how to build formulae in a classic logicians form, which I think is hard to follow, so I’ve converted it into a grammar:<\/p>\n That’s the entire logic! It’s tiny, but it’s enough. Everything else from predicate logic can be defined in terms of combinations of these basic formulae. For example, you can define logical “and” in terms of negation and logical “or”: (a ∧ b) ⇔ ¬ (¬ a ∨ ¬ b)<\/em>.<\/p>\n With the syntax of the system set, the next thing we need is the basic axioms of logical inference in the system. In terms of logic the way I think of it, these axioms include both “true” axioms, and the inference rules defining how the logic works. There are five families of axioms.<\/p>\n So, now, finally, we can get to the numbering. This is quite clever. We’re going to use the simplest encoding: for every possible string of symbols in the logic, we’re going to define a representation as a number. So in this representation, we are not<\/em> going to get the property that every natural number is a valid formula: lots of natural numbers won’t be. They’ll be strings of nonsense symbols. (If we wanted to, we could make every number be a valid formula, by using a parse-tree based numbering, but it’s much easier to just let the numbers be strings of symbols, and then define a predicate over the numbers to identify the ones that are valid formulae.)<\/p>\n We start off by assigning numbers to the constant symbols:<\/p>\n Variables will be represented by powers of prime numbers, for prime numbers greater that 13. For a prime number p<\/em>, p<\/em> will represent a type one variable, p2<\/sub><\/em> will represent a type two variable, p3<\/sup><\/em> will represent a type-3 variable, etc.<\/p>\n Using those symbol encodings, we can take a formula written as symbols x1<\/sub>x2<\/sub>x3<\/sub>…xn<\/sub><\/em>, and encode it numerically as the product 2x1<\/sub><\/sup>3x2<\/sub><\/sup>5x2<\/sub><\/sup>…pn<\/sub>xn<\/sub><\/sup><\/em>, where pn<\/sub><\/em> is the n<\/em>th prime number.<\/p>\n For example, suppose I wanted to encode the formula: ∀ x1<\/sub> (y2<\/sub>(x1<\/sub>)) ∨ x2<\/sub>(x1<\/sub>)<\/em>.<\/p>\n First, I’d need to encode each symbol:<\/p>\n The formula would thus be turned into the sequence: [9, 17, 11, 361, 11, 17, 13, 7, 289, 11, 17, 13, 13]. That sequence would then get turned into a single number 29<\/sup> 317<\/sup> 511<\/sup> 7361<\/sup> 1111<\/sup> 1317<\/sup> 1713<\/sup> 197<\/sup> 23289<\/sup> 2911<\/sup> 3117<\/sup> 3713<\/sup> 4113<\/sup>, which according to Hugs is the number (warning: you need to scroll to see it. a lot!):<\/p>\n 1,821,987,637,902,623,701,225,904,240,019,813,969,080,617,900,348,538,321,073,935,587,788,506,071,830,879,280,904,480,021,357,988,798,547,730,537,019,170,876,649,747,729,076,171,560,080,529,593,160,658,600,674,198,729,426,618,685,737,248,773,404,008,081,519,218,775,692,945,684,706,455,129,294,628,924,575,925,909,585,830,321,614,047,772,585,327,805,405,377,809,182,961,310,697,978,238,941,231,290,173,227,390,750,547,696,657,645,077,277,386,815,869,624,389,931,352,799,230,949,892,054,634,638,136,137,995,254,523,486,502,753,268,687,845,320,296,600,343,871,556,546,425,114,643,587,820,633,133,232,999,109,544,763,520,253,057,252,248,982,267,078,202,089,525,667,161,691,850,572,084,153,306,622,226,987,931,223,193,578,450,852,038,578,983,945,920,534,096,055,419,823,281,786,399,855,459,394,948,921,598,228,615,703,317,657,117,593,084,977,371,635,801,831,244,944,526,230,994,115,900,720,026,901,352,169,637,434,441,791,307,175,579,916,097,240,141,893,510,281,613,711,253,660,054,258,685,889,469,896,461,087,297,563,191,813,037,946,176,250,108,137,458,848,099,487,488,503,799,293,003,562,875,320,575,790,915,778,093,569,309,011,025,000,000,000.<\/p>\n Next, we’re going to look at how you can express interesting mathematical properties in terms of numbers. Gödel used a property called primitive recursion as an example, so we’ll walk through a definition of primitive recursion, and show how Gödel expressed primitive recursion numerically.<\/p>\n","protected":false},"excerpt":{"rendered":" The first step in Gödel’s incompleteness proof was finding a way of taking logical statements and encoding them numerically. Looking at this today, it seems sort-of obvious. I mean, I’m writing this stuff down in a text file – that text file is a stream of numbers, and it’s trivial to convert that stream of […]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"_jetpack_memberships_contains_paid_content":false,"footnotes":"","jetpack_publicize_message":"","jetpack_publicize_feature_enabled":true,"jetpack_social_post_already_shared":true,"jetpack_social_options":{"image_generator_settings":{"template":"highway","default_image_id":0,"font":"","enabled":false},"version":2}},"categories":[90,33,292],"tags":[],"class_list":["post-3061","post","type-post","status-publish","format-standard","hentry","category-incompleteness-logic","category-logic","category-type-theory"],"jetpack_publicize_connections":[],"jetpack_featured_media_url":"","jetpack_shortlink":"https:\/\/wp.me\/p4lzZS-Nn","jetpack_sharing_enabled":true,"jetpack_likes_enabled":true,"_links":{"self":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/3061","targetHints":{"allow":["GET"]}}],"collection":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/comments?post=3061"}],"version-history":[{"count":4,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/3061\/revisions"}],"predecessor-version":[{"id":3065,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/3061\/revisions\/3065"}],"wp:attachment":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/media?parent=3061"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/categories?post=3061"},{"taxonomy":"post_tag","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/tags?post=3061"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}\n
\n
\n elementary_formula → signn+1<\/sub>(signn<\/sub>)\n formula → ¬(elementary_formula)\n formula → (elementary_formula) or (elementary_formula)\n formula → ∀ signn<\/sub> (elementary_formula)\n<\/pre>\n
\n
\n
\n
\n
](http:\/\/l.wordpress.com\/latex.php?latex=%5Cforall%20v%28a%29%20%5CRightarrow%20%5Ctext%7Bsubst%7D%5Bv%2Fc%5D%28a%29&bg=FFFFFF&fg=000000&s=0 "\\forall v(a) \\Rightarrow \\text{subst}[v\/c](a)")
\n 
\n 
\n
\n Symbols<\/th>\n Numeric Representation<\/th>\n<\/tr>\n \n 0<\/td>\n 1<\/td>\n<\/tr>\n \n succ<\/td>\n 3<\/td>\n<\/tr>\n \n ¬<\/td>\n 5<\/td>\n<\/tr>\n \n ∨<\/td>\n 7<\/td>\n<\/tr>\n \n ∀<\/td>\n 9<\/tr>\n \n (<\/td>\n 11<\/td>\n<\/tr>\n \n )<\/td>\n 13<\/td>\n<\/tr>\n<\/table>\n \n