'H' is G++

'H' is 'G'++

(Mathematical humor ... gotta love it!)

(although the symbol '++' to signify 'Mathematical Humor' is an egregious misnomer, as the 'auto-increment' operator is not mathematical in any sense at all! How do you auto-increment the number 4 to become the number 5? You don't!)

(So there.)

(Not that I'm digressing or anything, but ...)

(continuing right along from the previous post, la-di-dah, as if I didn't fall asleep right on my laptop, or anything like that) ... to get there, but now we enhance Gödel translation functions, instead of translating ⊥ (the uninhabited type), we instead choose some (arbitrary) type, k, to be translated and then to do our translation:

k^⊥ -> k

(p -> q)^k -> (p^k -> q^k)

The beauty of this is that k, our arbitrary type, can be anything we choose, be it integers or person-objects, or whatever unit of logic we are having the conversation about.

We can now lift the conversation from classical logic to intuitionistic logic, because we now have a translation for 'not' that intuitionistic logic can deal with, and that is:

¬p == p -> ⊥

Now, translating from intuitionistic logic to executable (programming) code, that's been covered in the literature by other articles, ... maybe I'll take that under 'i' for intuitionistic logic or 't' for program translation, but not here.

Epilogue

As promised, the Gödel numbering.

There's actually many ways to skin this Schödinger's cat. One of them, not Gödel's, is to recode what is a 'number.'

For example, in the programming language Forth, at base 36, every number, and letter, is a number!

0 is 0

1 is 1

...

9 is 9

A is 10

B is 11

...

Z is 36

There it is: base thirty-six. In base thirty-six, the number 'number' is

foldr (\c sum -> sum * 36 + ord c - ord 'a' + 10) 0 "number"

or 1656644207.

Huh. A pretty big number.

So one encoding is to assign primitive functions to numbers (which now include letters) and when we string them together we have an unique number for each formula,

So, if we give

B

the value

B = \x y z -> x(yz)

And

C

the value

C = \x y z -> xzy

and

I

the value

I = \x -> x

and

K

the value

K = \x y -> x

and

M

the value

M = \x -> xx

and

S

the value

S = \x y z -> xy(xz)

We can actually write statements of truth using these letters, like:

SKK

or

M(KBC(SI)(KSK))

or

... anything else

(you see a problem, however: I did have to use open and close parentheses, so those two symbols must also be introduced as numbers).

And the above formula are actually numbers as well as being formulae, that is statements of truth, that can be reasoned about.

That's one numbering; the alphabet-soup that Combinator logic is.

Another is even simpler, reducing down to the simplest pair of combinators (including parenthesization (that, actually, is a word, regardless of what my stupid spell-checker says.) (stupid spell-checker)), and for that we have the iota programming language, or just ι to its friends.

Programs look like this in ι:

1011110110111101

Needless to say, that, too, can be reduced to a number which can be reasoned about.

Gödel went in neither of these directions, or, instead of looking at a functional/lambda approach, he chose to represent mathematical logic in ordinal form, and instead of using combinators to eliminate variable-representation from his statements, he also represented logical variables in his enumerated set of symbols,(1) choosing a basic set of logical symbols to represent as numbers, so each number became, not a function, but a statement of truth.

He would encode a statement of truth by it's (lexical) ordering, so:

¬¬p

if ¬ were encoded as 1 and 'p' were encoded as 2 would be represented as powers of primes:

2¹ * 3¹ * 5²

And by the fundamental theorem of algebra, the resulting number, for an unique input statement would yield an unique number.

Coolness!

But how do you represent numbers here?

Gödel used Peano numbers, which, like the Roman numerals, are unary:

z = 0

sz = 1

ssz = 2

sssz = 3

... you get the point

So if 'z' is 3 and 's' is 4

Then the number 12 is 12 s's followed by a 'z' which is

2³ * 3³ * 5³ * .... * 41⁴ 

which is number so big that if I had a dollar for every 's' in its resulting Peano representation, ... well, I'd have a lot of dollars!(2)

Well, so using simple logic symbols (that created very, very, ... very big numbers) (bigger than infinity + 1, even!) (Okay, now I have to go to confession), Gödel was able to create a predicate that determined if a formula was determinable in Principia Mathematica, he named it det(f) ... I suppose because 'Gertrude' was taken, already, so he had to settle for 'det.'

It also could be because 'det' implies 'determinable,' and not because of unrequited love, but mathematicians' hearts are always breaking over a girl named Agatha (just ask one of the world's most famous mathematicians, I'm sure you've heard his name: Brahms. Johannes to his buddies) or Gertrude or Millicent or Chrysanthemum.

Ah, Chrysanthemum!

But I digress.

So, but what happens when you run a formula that never returns through det?

For example, the formula M is \x -> x x, so the formula M M reduces as follows:

M M -> (\x -> x x) M -> substitute M in x gets you M M -> (\x -> x x) M -> substitute ... forever.

M M gets you M M and when you try to reduce that it gets you M M.

M is known as the looping function. It gives you loops, functionally, or drives you loopy.

Either one. Or both.

So, the point is that det(M M) is ...

There is no answer to that.

And that's the problem, because now you have a case were det itself is ... wait for it.

Not det.

det is not det.

That's like saying p = ¬p or 5 isn't 5 anymore.

That's inconsistent.

Once Gödel had that, he encoded det as a Gödel number (it was 'rather' large)(like: infinity + 2)(... but not) and then showed that ¬ det(det) was true inside the Principia Mathematica, and using only the axioms and rules that the Principia Mathematica allowed.

The Principia Mathematica, a system Russell created and worked so hard to show was complete and consistent ...

Well, Gödel showed that it was inconsistent, and showed it entirely within the Principia Mathematica framework.

That show, that proof, was named Gödel's Incompleteness Theorem (again, because Gertrude was taken, at the time), and has forever changed the tenor and tone of the conversation of mathematics since.

Meta-epilogue: 'H' is for Hilbert

Now I was going to go on a rant about how ++ is just plain bad in every sense of the word. Once you can change the number 5 into the number 6, then you have just opened up a box that you can never close again.

In Category Theory a function has identity and composition, but if you can change something, anything, like, the function, then what does identity mean? ('I' is for isomorphism. But later, not now).

Identity loses its meaning in the face of mutability, and provable properties about your theories and your system at large go out the window.

But I not going to talk about 'H' is for G++ and how mutability is just plain bad, bad, bad.

I'm not.

I'm going to talk a little bit about Hilbert.

Okay, so this dude was on fire. He basically invented mathematical logic, as a concept, and stood up before the whole world and held in his hands the only set of unsolved problems in math (there were 23 of them) and he shook his fist and said the famous last words: "We must know. We will know!"

Then he died. Then Gödel proved mathematics inconsistent, intrinsically so.

Not only that, Gödel, and others using his work, showed at least three of the problems were unsolvable. It wasn't that the solution was hard to get to without computers or supercomputers (that they didn't have at the time) nor even quantum computers ('Q' is for qubit) (later! later!) but they were intrinsically unsolvable because of Gödel's incompleteness theorem.

Bam.

Poor Hilbert!

I mean, he died brimming with hope. He had his words carved on his gravestone: "We must know. We will know."

And now, we will never, ever will know.

'H' is for Hilbert. He thought we were big enough to conquer all of mathematics.

But they did name Hilbert-space after him. So he does have that going for him.

-----

Endnotes:

(1) This smacks of coding in the good old days of FORTRAN where you could have any integral variable you wanted, insofar it was named either 'i' or 'j' or 'k' ... what? You want more variables? Go write a different program! Jeez! Why would anybody want a variable named something else than i, j, or k, anyway!

(2) 1154720154130223108008498916387587352955801000 of them, in fact! I'd buy that for a dollar!