What we’ve done so far is the first two steps, and part of the third. In this post<\/a>, we saw the form of the Principia’s logic that we’re using, and how to numerically encode it as a Gödel numbering. We’ve start started on the third point in this post<\/a>, by figuring out just what it means to say that things are encoded arithmetically. Now we can get to the part where we see how to encode meta-mathematical properties in terms of arithmetic properties of the Gödel numbering. In this post, we’re going to build up everything we need to express syntactic correctness, logical validity, and provability in terms of arithmetical properties of Gödel numbers. (And, as a reminder, I’ve been using this translation<\/a> on Gödel’s original paper on incompleteness.)<\/p>\n This is the most complex part of the incompleteness proof. The basic concept of what we’re doing is simple, but the mechanics are very difficult. What we want to do is define a set of predicates about logical statements, but we want those predicates to be expressed as arithmetic properties of the numerical representations of the logical statements.<\/p>\n The point of this is that we’re showing that done in the right way, arithmetic is<\/em> logic – that doing arithmetic on the Gödel numbers is doing logical inference. So what we need to do is build up a toolkit that shows us how to understand and manipulate logic-as-numbers using arithmetic. As we saw in the last post, primitive recursion is equivalent to arithmetic – so if we can show how all of the properties\/predicates that we define are primitive recursive, then they’re arithmetic.<\/p>\n This process involves a lot<\/em> of steps, each of which is building the platform for the steps that follow it. I struggled quite a bit figuring out how to present these things in a comprehensible way. What I ended up with is writing them out as code in a pseudo-computer language. Before inventing this language, I tried writing actual executable code, first in Python and then in Haskell, but I wasn’t happy with the clarity of either one. <\/p>\n Doing it in an unimplemented language isn’t as big a problem as you might think. Even if this was all executable, you’re not going to be able to actually run any of it on anything real – at least not before you hair turns good and gray. The way that this stuff is put together is not what any sane person would call efficient. But the point isn’t to be efficient: it’s to show that this is possible<\/em>. This code is really all about searching; if we wanted to be efficient, this could all be done in a different representation, with a different search method that was a lot faster – but that wolud be harder to understand.<\/p>\n So, in the end, I threw together a simple language that’s easy to read. This language, if it were implemented, wouldn’t really even be Turing complete – it’s a primitive recursive language.<\/p>\n We’ll start off with simple numeric properties that have no obvious connection to the kinds of meta-mathematical statements that we want to talk about, but we’ll use those to define progressively more and more complex and profound properties, until we finally get to our goal.<\/p>\n Almost everything we’re going to do here is built on a common idiom. For anything we want to do arithmetically, we’re going to find a bound – a maximum numeric value for it. Then we’re going to iterate over all of the values smaller than that bound, searching for our target.<\/p>\n For example, what’s the n<\/em>th prime factor of x<\/em>? Obviously, it’s got to be smaller than x<\/em>, so we’ll use x<\/em> as our bound. (A better bound would be the square root of x, but it doesn’t matter. We don’t care about efficiency!) To find the n<\/em>th prime factor, we’ll iterate over all of the numbers smaller than our bound x<\/em>, and search for the smallest number which is prime, which divides x<\/em>, and which is larger than the n-1<\/em>th prime factor of x<\/em>. We’ll translate that into pseudo-code:<\/p>\n Similarly, for extracting values from strings, we need to be able to ask, in general, what's the nth prime number? This is nearly identical to In composing strings of Gödel numbers, we use exponentiation. Given integers x<\/em> and n<\/em>, xn<\/sup><\/em>, we can obviously compute them via primitive recursion. I'll define them below, but in the rest of this post, I'll write them as an operator in the language:<\/p>\n With those preliminaries out of the way, we can get to the point of defining something that's actually about one of the strings encoded in these Gödel numbers. Given a number n<\/em> encoding a string, Given a string, we want to be able to ask how long it is; and given two strings, we want to be able to concatenate them.<\/p>\n We want to be able to build statements represented as numbers from other statements represented as numbers. We'll define a set of functions that either compose new strings from other strings, and to check if a particular string is a particular kind of syntactic element.<\/p>\n That last function contains an error: the translation of Gödel that I'm using says Using what we've defined so far, we're now ready to start defining formulae in the basic Principia logic. Forumlae are strings, but they're strings with a constrained syntax.<\/p>\n All this is doing is expressing the grammar rule in arithmetic form: an elementary formula is a predicate: P(x)<\/em>, where x<\/em> is a variable on level n<\/em>, and P<\/em> is a variable of level x + 1<\/em>.<\/p>\n The next grammar rule that we encode this way says how we can combine elementary formulae using operators. There are three operators: negation, conjunction, and universal quantification.<\/p>\n And now we can start getting complex. We're going to define the idea of a valid sequence<\/em> of formulae. x<\/em> is a valid sequence of formulae when it's formed from a collection of formulae, each of which is either an elementary formula, or is produced from the formulae which occured before it in the sequence using either negation, logical-or, or universal quantification.<\/p>\n In terms of a more modern way of talking about it, the syntax of the logic is a grammar. A formula sequence, in this system, is another way of writing the parse-tree of a statement: the sequence is the parse-tree of the last statement in the sequence.<\/p>\n The next one bugs me, because it seems wrong, but it isn't really! It's a way of encoding the fact that a formula is the result of a well-defined sequence of formulae. In order to ensure that we're doing primitive recursive formulae, we're always thinking about sequences of formulae, where the later formulae are produced from the earlier ones. The goal of the sequence of formula is to produce the last formula in the sequence. What this predicate is really saying is that a formula is a valid formula if there is some sequence of formulae where this is the last one in the sequence.<\/p>\n Rephrasing that in grammatical terms, a string is a formula if there is valid parse tree for the grammar that produces the string.<\/p>\n So, now, can we say that a statement is valid because it's parsed according to the grammar? Not quite. It's actually a familiar problem for people who write compilers. When you parse a program in some language, the grammar doesn't usually specify variables must be declared before they're used. It's too hard to get that into the grammar. In this logic, we've got almost the same problem: the grammar hasn't restricted us to only use bound variables. So we need to have ways to check whether a variable is bound in a Gödel-encoded formula, and then use that to check the validity of the formula.<\/p>\n To do logical inference, we need to be able to do things like replace a variable with a specific infered value. We'll define how to do that:<\/p>\n There are inference operations and validity checks that we can only do if we know whether a particular variable is free at a particular position.<\/p>\n In the original logic, some inference rules are defined in terms of a primitive substitution operator, which we wrote as subst[v\/c](a)<\/em> to mean substitute the value c<\/em> for the variable c<\/em> in the statement a<\/em>. We'll build that up on a couple of steps, using the The next thing we're going to do isn't, strictly speaking, absolutely necessary. Some of the harder stuff we want to do will be easier to write using things like implication, which aren't built in primitive of the Principia logic. To write those as clearly as possible, we'll define the full suite of usual logical operators in terms of the primitives.<\/p>\n The Peano axioms are valid logical statements, so they have Gödel numbers in this system. We could compute their value, but why bother? We know that they exist, so we'll just give them names, and define a predicate to check if a value matches them.<\/p>\n The form of the Peano axioms used in incompleteness are:<\/p>\n Similarly, we know that the propositional axioms must have numbers. The propositional I'll show the translation of the first - the rest follow the same pattern.<\/p>\n Similarly, all of the other axioms are written out in the same way, and we add a predicate The two quantifier axioms are:<\/p>\n We need to define a predicate for the reducibility axiom (basically, the Principia's version of the ZFC axiom of comprehension). The reducibility axiom is a schema: for any predicate Now, the set axiom. In the logic we're using, this is the axiom that defines set equality. It's written as We haven't defined the type-1 set axiom. But we just saw the axiom above, and it's obviously a simple logical statement. That mean that it's got a Gödel number. Instead of computing it, we'll just say that that number is called We've now defined all of the axioms of the logic, so we can now create a general predicate to see if a statement fits into any of the axiom categories:<\/p>\n With all of the axioms expressible in primitive recursive terms, we can start on what it means for something to be provable. First, we'll define what it means for some statement x<\/em> to be an immediate consequence<\/em> of some statements y<\/em> and z<\/em>. (Back when we talked about the Principia's logic, we said that x<\/em> is an immediate consequence of y<\/em> and z<\/em> if either: y is the formula z ⇒ x<\/em>, or if c<\/em> is the formula ∀v.x).<\/p>\n Now, we can use our definition of an immediate consequence to specify when a sequence of formula is a proof figure<\/em>. A proof figure is a sequence of statements where each statement in it is either an axiom, or an immediate consequence of two of the statements that preceeded it.<\/p>\n We can say that x<\/em> is a proof of y<\/em> if x<\/em> is proof figure, and the last statement in x<\/em> is y<\/em>.<\/p>\n Finally, we can get to the most important thing! We can define what it means for something to be provable<\/em>! It's provable if there's a proof for it!<\/p>\n Note that this last one is not<\/em> primitive recursive! There's no way that we can create a bound for this: a proof can be any length.<\/p>\n At last, we're done with these definition. What we've done here is really amazing: now, every logical statement can be encoded as a number. Every proof in the logic can be encoded as a sequence of numbers: if something is provable in the Principia logic, we can encode that proof as a string of numbers, and check the proof for correctness using nothing but (a whole heck of a lot of) arithmetic!<\/p>\n Next post, we'll finally get to the most important part of what Gödel did. We've been able to define what it means for a statement to be provable - we'll use that to show that there's a way of creating a number encoding the statement that something is not<\/em> provable. And we'll show how that means that there is a true statement in the Principia's logic which isn't provable using the Principia's logic, which means that the logic isn't complete.<\/p>\n In fact, the proof that we'll do shows a bit more than that. It doesn't just show that the Principia's logic is incomplete. It shows that any<\/em> consistent formal system like the Principia, any system which is powerful enough to encode Peano arithmetic, must<\/em> be incomplete.<\/p>\n","protected":false},"excerpt":{"rendered":" On to the next part of Gödel’s proof of incompleteness. To refresh your memory, here’s a sketch of the proof: Take a simple logic. We’ve been using a variant of the Principia Mathematica’s logic, because that’s what Gödel used. Show that any statement in the logic can be encoded as a number using an arithmetic […]<\/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-3071","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-Nx","jetpack_sharing_enabled":true,"jetpack_likes_enabled":true,"_links":{"self":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/3071","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=3071"}],"version-history":[{"count":4,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/3071\/revisions"}],"predecessor-version":[{"id":3075,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/3071\/revisions\/3075"}],"wp:attachment":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/media?parent=3071"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/categories?post=3071"},{"taxonomy":"post_tag","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/tags?post=3071"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}Basics<\/h3>\n
\n# divides n x == True if n divides x without remainder.\npred divides(n, x) = x mod n == 0\n\npred isPrime(0) = False\npred isPrime(1) = False\npred isPrime(2) = True\npred isPrime(n) = {\n all i in 2 to n {\n not divides(i, n)\n }\n}\n\nfun fact(0) = 1\nfun fact(n) = n * fact(n - 1)\n<\/pre>\n\nfun prFactor(0, x) = 0\nfun prFactor(n, x) = {\n first y in 1 to x {\n isPrime(y) and divides(y, x) and prFactor(n - 1, x) < y\n }\n}\n\n<\/pre>\nprFactor<\/code> above. The only difference is that we need a different bound. Fortunately, we know that the n<\/em>th prime number can't be larger than the factorial of the previous prime plus 1.<\/p>\n\nfun nthPrime(0) = 0\nfun nthPrime(n) = {\n first y in 1 to fact(nthPrime(n - 1)) + 1 {\n isPrime(y) and y > nthPrime(n - 1))\n }\n}\n\n<\/pre>\n\nfun pow(n, 0) = 1\nfun pow(n, i) = n * pow(n, i - 1)\n\n<\/pre>\n
String Composition and Decomposition<\/h3>\n
item(n, x)<\/code> is the value of the n<\/em>th character of x. (This is slow. This is really<\/em> slow! We're getting to the limit of what a very powerful computer can do in a reasonable amount of time. But this doesn't matter. The point isn't that this is a good way of doing these things: it's that these things are possible<\/em>. To give you an idea of just how slow this is, I started off writing the stuff in this post in Haskell. Compiled with GHC, which is a very good compiler, using item<\/code> to extract the 6th character of an 8 character string took around 10 minutes on a 2.4Ghz laptop. In the stuff that follows, we'll be using this to extract characters from strings that could be hundreds of characters long!)<\/p>\n\nfun item(n, x) = {\n first y in 1 to x {\n divides(prFactor(n, x) ** y, y) and\n not divides(prFactor(n, x)**(y+1), x)\n }\n}\n\n<\/pre>\n\nfun length(x) = {\n first y in 1 to x {\n prFactor(y, x) > 0 and prFactor(y + 1, x) == 0\n }\n}\n\nfun concat(x, y) = {\n val lx = length(x)\n val ly = length(y)\n\n first z in 1 to nthprime(lx + ly)**(x + y) {\n (all n in 1 to lx {\n item(n, z) == item(n, x)\n }) and (all n in 1 to ly {\n item(n + lx, z) == item(n, y)\n })\n }\n}\n\nfun concatl([]) = 0\nfun concatl(xs) = {\n concat(head(xs), concatl(tail(xs)))\n}\n\nfun seq(x) = 2**x\n<\/pre>\n\n# x is a variable of type n.\npred vtype(n, x) = {\n some z in 17 to x {\n isPrime(z) and x == n**z\n }\n}\n\n# x is a variable\npred isVar(x) = {\n some n in 1 to x {\n vtype(n, x)\n }\n}\n\nfun paren(x) =\n concatl([gseq(11), x, gseq(13)])\n\n# given the Gödel number for a statement x, find\n# the Gödel number for not x.\nfun gnot(x) =\n concat(gseq(5), paren(x))\n\n# Create the number for x or y.\nfun gor(x, y) =\n concatl([paren(x), seq(7), paren(y)])\n\n# Create the number for 'forall x(y)'.\nfun gforall(x, y) =\n concatl([seq(9), seq(x), paren(y)])\n\n# Create the number for x with n invocations of the primitive\n# successor function.\nfun succn(0, x) = x\nfun succn(n, x) = concat(seq(3), succn(n - 1, x))\n\n# Create the number n using successor and 0.\nfun gnumber(n) = succn(n, seq(1))\n\n# Check if a statement is type-1.\npred stype_one(x) = {\n some m in 1 to x {\n m == 1 or (vtype(1, m) and x == succn(n, seq(m))\n }\n}\n\n# Check if a statement is type n.\npred fstype(1, x) = stype_one(x)\npred fstype(n, x) =\n some v in 1 to x {\n vtype(n, v) and R(v)\n }\n}\n\n<\/pre>\nR(v)<\/code> without defining R<\/code>. Either I'm missing something, or the translator made an error.<\/p>\nFormulae<\/h3>\n
\npred elFm(x) = {\n some y in 1 to x {\n some z in 1 to x {\n some n in 1 to x {\n stype(n, y) and stype(n+1, z) and x == concat(z, paren(y))\n }\n }\n }\n}\n\n<\/pre>\n\npred op(x, y, z) = {\n x == gnot(y) or\n x == gor(y, z) or\n (some v in 1 to x { isVar(v) and x == gforall(v, y) })\n}\n\n<\/pre>\n\npred fmSeq(x) = {\n all p in 0 to length(x) {\n elFm(item(n, x)) or\n some p in 0 to (n - 1) {\n some q in 0 to (n - 1) {\n op(item(n,x), item(p, x), item(q, x))\n }\n }\n }\n}\n\n<\/pre>\n\npred isFm(x) = {\n some n in 1 to nthPrime(length(x)**2)**(x*length(x)**2) {\n fmSeq(n)\n }\n}\n\n<\/pre>\n\n# The variable v is bound in formula x at position n.\npred bound(v, n, x) = {\n isVar(v) and isFm(x) and\n (some a in 1 to x {\n some b in 1 to x {\n some c in 1 to x {\n x == concatl([a, gforall(v, b), c]) and\n isFm(b) and\n length(a) + 1 ≤ n ≤ length(a) + length(forall(v, b))\n }\n }\n })\n}\n\n# The variable v in free in formula x at position n\npred free(v, n, x) = {\n isVar(v) and isFm(x) and\n (some a in 1 to x {\n some b in 1 to x {\n some c in 1 to x {\n v == item(n, x) and n ≤ length(x) and not bound(v, n, x)\n }\n }\n })\n}\n\npred free(v, x) = {\n some n in 1 to length(x) {\n free(v, n, x)\n }\n}\n\n<\/pre>\n\n# replace the item at position n in x with y.\nfun insert(x, n, y) = {\n first z in 1 to nthPrime(length(x) + length(y))**(x+y) {\n some u in 1 to x {\n some v in 1 to x {\n x == concatl([u, seq(item(n, x)), v]) and\n z == concatl([u, y, v]) and\n n == length(u) + 1\n }\n }\n }\n}\n\n<\/pre>\n\n# freePlace(k, v, k) is the k+1st place in x (counting from the end)\n# where v is free.\nfun freePlace(0, v, x) = {\n first n in 1 to length(x) {\n free(v, n, x) and\n not some p in n to length(x) {\n free(v, p, x)\n }\n }\n}\n\nfun freePlace(k, v, x) = {\n first n in 1 to freePlace(n, k - 1, v) {\n free(v, n, x) and\n not some p in n to freePlace(n, k - 1, v) {\n free(v, p, x)\n }\n }\n}\n\n# number of places where v is free in x\nfun nFreePlaces(v, x) = {\n first n in 1 to length(x) {\n freeplace(n, v, x) == 0\n }\n}\n\n<\/pre>\nfreePlaces<\/code> function that we just defined.<\/p>\n\n# Subst1 replaces a single instance of v with y.\nfun subst'(0, x, v, y) = x\nfun subst1(0k, x, v, y) =\n insert(subst1(k, x, v, y), freePlace(k, v, x), y)\n\n# subst replaces all instances of v with y\nfun subst(x, v, y) = subst'(nFreePlaces(v, x), x, v, y)\n<\/pre>\n
\n# implication\nfun gimp(x, y) = gor(gnot(x), y)\n\n# logical and\nfun gand(x, y) = gnot(gor(gnot(x), gnot(y)))\n\n# if\/f\nfun gequiv(x, y) = gand(gimp(x, y), gimp(y, x))\n\n# existential quantification\nfun gexists(v, y) = not(gforall(v, not(y)))\n<\/pre>\n
Axioms<\/h3>\n
\n
\nconst pa1 = ...\nconst pa2 = ...\nconst pa3 = ...\n\npred peanoAxiom(x) =\n (x == pa1) or (x == pa2) or (x == pa3)\n<\/pre>\n
\naxioms are:<\/p>\n\n
\n# Check if x is a statement that is a form of propositional\n# axiom 1: y or y => y\npred prop1Axiom(x) =\n some y in 1 to x {\n isFm(x) and x == imp(or(y, y), y)\n }\n}\n\npred prop2Axiom(x) = ...\npred prop3Axiom(x) = ...\npred prop4Axiom(x) = ...\npred propAxiom(x) = prop2Axiom(x) or prop2Axiom(x) or\n prop3Axiom(x) or prop4Axiom(x)\n<\/pre>\nisAxiom<\/code> to check if something is an axiom. Next is quantifier axioms, which are complicated, so I'll only write out one of them - the other follows the same basic scheme.<\/p>\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)")
\nquantifier_axiom1_condition(z, y, v) = {\n not some n in 1 to length(y) {\n some m in 1 to length(z) {\n some w in 1 to z {\n w == item(m, z) and bound(w, n, y) and free(v, n, y)\n }\n }\n }\n}\n\npred quantifier1Axiom(x) = {\n some v in 1 to x {\n some y in 1 to x {\n some z in 1 to x {\n some n in 1 to x {\n vtype(n, v) and stype(n, z) and\n isFm(y) and\n quantifier_axiom1_condition(z, y, v) and\n x = gimp(gforall(v, y), subst(y, v, z))\n }\n }\n }\n }\n}\n\nquanitifier_axiom2 = ...\nisQuantifierAxiom = quantifier1Axiom(x) or quantifier2Axiom(x)\n<\/pre>\n
\npred reduAxiom(x) =\n some u in 1 to x {\n some v in 1 to x {\n some y in 1 to x {\n some n in 1 to x {\n vtype(n, v) and\n vtype(n+1, u) and\n not free(u, y) and\n isFm(y) and\n x = gexists(u, gforall(v, gequiv(concat(seq(u), paren(seq(v))), y)))\n }\n }\n }\n }\n}\n\n<\/pre>\n
\nfun typeLift(n, x) = {\n first y in 1 to x**(x**n) {\n all k in 1 to length(x) {\n item(k, x) ≤ 13 and item(k, y) == item(k, v) or\n item(k, x) > 13 and item(k, y) = item(k, x) * prFactor(1, item(k, x))**n\n }\n }\n}\n\n<\/pre>\nsa1<\/code>. Now we can define a predicate to check if something is a set axiom:<\/p>\n\nval sa1 = ...\npred setAxiom(x) =\n some n in 1 to x {\n x = typeLift(n, sa)\n }\n}\n\n<\/pre>\n\npred isAxiom(x) =\n peanoAxiom(x) or propAxiom(x) or quantifierAxom(x) or\n reduAxiom(x) or setAxiom(x)\n<\/pre>\n
Proofs and Provability!<\/h3>\n
\npred immConseq(x, y, z) = {\n y = imp(z, x) or\n some v in 1 to x {\n isVar(v) and x = forall(v, y)\n }\n}\n\n<\/pre>\n\npred isProofFigure(x) = {\n (all n in 0 to length(x) {\n isAxiom(item(n, x)) or\n some p in 0 to n {\n some q in 0 to n {\n immConseq(item(n, x), item(p, x), item(q, x))\n }\n }\n }) and\n length(x) > 0\n}\n\n<\/pre>\n\npred proofFor(x, y) =\n isProofFigure(x) and\n item(length(x), x) == y\n<\/pre>\n
\npre provable(x) =\n some y {\n proofFor(y, x)\n }\n}\n\n<\/pre>\n