Friday, June 7, 2013

Mappings and the arithmetization of meta-mathematics

In an earlier post, we discussed mappings in general and then described Gödel numbering, which is a mapping between the set of well-formed formulas (wff's) in a formal system and the set of positive integers.

In part B of section VII, Nagel and Newman describe a more interesting mapping used in Gödel's proof. In this mapping, the domain is the set of meta-mathematical statements about structural properties of wff's, while the co-domain is the set of wff's. This post describes how this mapping enabled Gödel to arithmetize meta-mathematics.

Let's use the letter F to refer to the formal system used in Gödel's proof. Recall that, thanks to Gödel numbering, each wff in F maps to a positive integer. Therefore, each meta-level statement about wff's and their relationships is also a statement about positive integers (Gödel numbers) and their relationships.

As a simple example, let's consider the following definition:
A universally quantified wff is a wff of F that starts with the universal quantifier, that is, a wff of the form ∀x (...) or ∀y (...) or ...
This definition is part of meta-mathematics because it talks about a structural property of wff's of F, that is, how they are built out of the alphabet symbols. So, any wff of the form ∀x (...) with the ellipse filled in, is part of mathematics (it is a wff inside F), while the definition above is part of meta-mathematics (it is outside of F and about some of the wff's of F).

For instance, recall the wff:

∀x ¬ ( x = f(x) ) )

This wff is a universally quantified wff since it satisfies the definition given above. The Gödel number of this wff is:

29 × 317 × 511 × 75 × 1111 × 1317 × 1715 × 193 × 2311 × 2917 × 3113 × 3713 × 4113

What is common between this Gödel number and the Gödel number of all other universally quantified wff's?

Since the first prime in each Gödel number is always 2 and its power is the Gödel number of the first symbol in the wff (namely 9), all universally quantified wff's have 29 (= 512) as their first factor.

Moreover, all of the remaining terms in the product (i.e., the Gödel number) are primes larger than 2, and thus odd numbers. Therefore, we just showed the following equivalence:

(a) a wff w in F is universally quantified

if and only if

(b) the Gödel number of w is divisible by 512 
but is not divisible by any even integer larger than 512

The next step is to realize that the numerical properties of being "divisible by some integer," of being "even," and of being "larger than 512" are all representable by wff's in F.

In conclusion, statement (b) above can be represented by some wff in F. So, the meta-mathematical statement (a) is true if and only if the wff expressing the mathematical statement (b) is true under the intended interpretation of F.

More generally, Gödel proved that EVERY meta-mathematical statement about the structural properties of wff's can be mapped to some wff in F. This is the so-called arithmetization of meta-mathematics, that is, a mapping from the set of meta-mathematical statements to the set of mathematical (and more precisely arithmetical) statements in the formal system F.

This mapping is important because it means that proving any meta-mathematical statement about the structural properties of formulas can be reduced to proving wff's within the formal system F. In other words, this mapping reduces meta-level reasoning to reasoning within the formal system.

So, coming back to our example, proving that some formula w is universally quantified reduces to proving in F the wff that represents the statement (b) above.

Furthermore, this mapping established by Gödel is not limited to reducing structural properties of wff's to numerical properties (of Gödel numbers). It extends to relationships among two or more wff's.

So Gödel proved that EVERY meta-mathematical statement about structural relationships between two wff's w1 and w2 can be mapped to some wff in F, and that this wff represents a specific (numerical) relationship between the Gödel numbers of w1 and w2.

Let's define some notation that will make the rest of this post easier to follow.
  • If w is any wff (or sequence of wff's) in F, let Φ(w) denote the Gödel number of w. 
  • If w1 and w2 are two wff's in F, let Prefix(w1,w2) denote the meta-mathematical statement "the wff w1 is a prefix of the wff w2," that is, the wff w1 not only appears inside (as a substring of) wff w2, but it appears right at the beginning of w2. So for example:
Prefix( (0=0) , (0=0) ∨ (f(0)=0) ) is true,


Prefix( (0=0) , (f(0)=0) ∨ (0=0) ) is false.

Keep in mind that Prefix(w1,w2) is a meta-mathematical statement. It states a structural relationship between two wff's in F. But according to Gödel's mapping, this meta-mathematical statement is mapped to a numerical relationship between Φ(w1) and Φ(w2). In fact, Nagel and Newman use that example because the numerical relationship is trivial.

Recall that the Gödel number of a wff is a product of prime powers, where the primes appear in increasing order starting at 2. Therefore,  Prefix(w1,w2) is true if and only if Φ(w1) evenly divides Φ(w2), or equivalently, Φ(w2) is a multiple of Φ(w1). Again, the numerical relationship of "x being a multiple of y" is easily represented within F itself.

One fascinating property that follows from Gödel's arithmetization of meta-mathematics is the fact that the formal system F is capable to describing itself! More specifically, it can represent numerical relationships that, when translated into meta-mathematical statements, express facts about F.

The examples of meta-mathematical statements and corresponding numerical relationships given above are trivial and uninteresting, except for the fact that they are simple enough that we can specify them fully in terms of easily understood arithmetical properties. But Gödel proved that any meta-mathematical statement about structural relationships between wff's of F and sequences of wff's of F can be expressed in F.

Now we turn our attention to a crucial meta-mathematical statement whose corresponding numerical relationship is really complex. The good news is that we do not need to fully specify this numerical relationship here. We just need to know that it exists, as Gödel proved in his paper (and I cannot wait to see what Peter Smith has to say about this proof!).

Since the property of completeness of a formal system has everything to do with its capabilities and limitations in terms of which wff's it can and cannot prove, let us focus on the following meta-mathematical statement:

(c) the sequence of wff's s is a proof in F of the wff w

Since each wff (and each sequence of wff's) in F has a unique Gödel number, we can use Gödel's mapping to conclude that statement (c) is equivalent to

(d) the numbers Φ(s) and Φ(w) are related to each other through 
a (complex but well-defined) numerical relationship 

Even though the numerical relationship mentioned in (d) is far from trivial (unlike "being divisible by"), Gödel proved that it can be represented by some wff in F. Let's denote this wff by


In other words:
(c) is true 

if and only if

the wff ProofOf(Φ(s),Φ(w)) is true in the intended interpretation of F

Keep in mind that (c) is a meta-mathematical statement about the purely structural properties of wff's (namely whether the sequence s is formal proof of w), whereas ProofOf(Φ(s),Φ(w)) is a mathematical statement within F about the numbers Φ(s) and Φ(w).

The key property of Gödel's mapping is that these two statements have the same truth value: they are either both true or both false. 

Following Nagel and Newman's lead, let's conclude this post with one more piece of notation that we'll need later. 

Recall the concept of substitution, by which a numerical expression n (e.g., f(f(0)) or f(y)) replaces each and every free occurrence of a numerical variable x in some wff w. Let's call w' the wff resulting from this substitution and write:

(e) w' = substitute(n,x,w)

to mean

(e') w' is the wff obtained by substituting n 
for each free occurrence of x in the wff w

Note that (e') is a meta-mathematical statement that describes a purely syntactical relationship between two wff's w and w', a numerical expression n and a numerical variable x. 

In (e'), w and w' are wff's in F. x is one of the basic signs, namely, a numerical variable in the alphabet of F (any other numerical variable can be used in place of x). Finally, n is an expression in F representing a number. For example, n could be the numerical expression f(f(f(f(f(0))))) representing the number 5. Note that n is not the number 5, or any number, for that matter; it is an expression that denotes a number.

As before, using Gödel's mapping, (e') gets mapped to a numerical relationship among the numbers Φ(w), Φ(w'), Φ(x) = 17 and the number that n denotes. Again, this numerical relationship is complex, but it exists and can be represented by a wff in F. Let's denote this wff:

Φ(w') = Sub(n,17,Φ(w))

whose English interpretation is:

Φ(w') is the Gödel number of the wff obtained by substituting 
the numerical expression n for each free occurrence of 
the variable with Gödel number 17 in the wff w

In conclusion, we have described Gödel's arithmetization of meta-mathematics, that is, a mapping from the set of meta-mathematical statements about the structural properties of wff's in F to the set of wff's in F, where F is a formal system for arithmetic.

In particular, we have highlighted the two following structural relationships:
  • the structural relationship between a wff w and a formal proof of w
  • the structural relationship between a wff w and the wff resulting from substituting in w a numerical expression for a free numerical variable
resulting in the following two associations:

meta-mathematical statementmathematical proposition in F

the sequence s is a proof of w

ProofOf( Φ(s) , Φ(w) )

meta-mathematical numerical expressionmathematical/numerical variable in F

the Gödel number of the wff
obtained by substituting n for
the free variable x in the wff w
Sub( n , 17 , Φ(w) )

No comments:

Post a Comment