'G' is for Gödel-Gentzen

'G' is for Gödel-Gentzen Translation.

Okay, this is going to feel a little ... weird.

Cue Morpheus marlinspiking Neo through the spine to reinject him into the Matrix.

So, what is 'true' and what is 'false'?

In Latin-based languages there is only 'non' but there is no word for 'yes.' You'd think there is, but the most common one: 'Si' is from 'sic' 'this.' And the alternative 'Oc' (from history: "The people who say 'Oc'") is 'hoc' 'this,' too.

There is no 'yes' in Latin, just 'no.'

In mathematics, there is no 'no' only instances, but not 'not something.'

I mean, there is, but there isn't.

You weirded out yet?

The problem is logic. 

There are universals: 'For every x, ...'

And existentials: 'There is some x that, ...'

But no 'non's.

So, if there're aren't 'non-exististentials,' then we can't really formulate 'not' with any authority.

So we can't say, 'That person is not Julia.'

We can say who she is, but we can't identify her by who she isn't.

So what to do? If 'not' really is the absence of something, and mathematics models what is, then how do you model what isn't?

Some logics just assume 'not' into existence ...

... You see the problem? You're creating a 'nothing' or a 'voider' or some such. How do you create something that isn't?

But some logics do exactly that: 'not' 'false' 'no' they all ... 'exist' in these logics.

From antiquity, too: classical logic admits 'not' into theory and use 'not' to prove these theories.

There it is. (Or more precisely: there it isn't!) (So if it isn't there, then where is it? Nowhere, right?)

(My head hurts.)

So, okay, some logics admit 'not.' And, since some of these logics are from antiquity, there's a lot of foundational work based in these logics that are extremely useful, practical, all that.

It'd be a shame to throw all that away.

But here's the problem. A lot of recent developments have started to question everything, about everything, because, after all, a set of rules or assumptions limit you to a set of world-views. Questioning these views allows you to open new avenues to explore.

So, classical logic admits 'not,' but a more recent logic, Intuitionistic logic, does not allow 'not.'

So what? Intuitionistic logic can go take a hike, right?

Well, the thing is, it's called Intuitionistic logic for a reason, and that is, this logic is a closer model to what our intuitions show us to be the 'real world,' whatever that may be. In particular, Intuitionistic logic is a very good descriptor of type theory that is heavily used in computer science, and, furthermore, (or, 'so, therefore,') statements of Intuitionistic logic have a direct mapping into (some) computer programming languages.

Again, so what?

The 'so what' is this: a statement of Intuitionistic logic has the strength of veracity to it. It can be proved. If you can map that down to a piece of a computer program, then you know, for sure, that that piece of code is correct, and verifiably so (that is, if your mapping is sound, and there are ways to prove the soundness of a mapping, as well, so we got ya covered there, too).

The same cannot be said for classical logic. Because we make the (axiomatic) assumption of 'not,' we get into weird circularities of the types when we try to map statements of classical logic down to computer program fragments.

BUT!

(Logic is ... hard. It's very dogged in exhausting all possible paths an argument can take.

Argument: "I can't take anymore!"

Logic: "Well, tough!"

Logic is just so ... unsympathetic!

The contrapositive statement: when somebody's being sympathetic? ... or sincere? They are not being logical. So you're getting somebody to agree with you, and a shoulder to cry on, but is somebody saying 'aw, that's okay, really!' what you really need? Or would brutal honesty get you out of the fix you're in?)

(But I digress.)

(As always.)

So, what do we do? We have all this neat stuff in classical logic, but we can't use it. We have a logic we can use in Intuitionistic Logic, but do we have to reinvent the wheel to use it?

A conundrum.

Then, along came a little guy by the name of Gödel, following up on some really interesting work that Gentzen did. Gentzen was able to prove things about arithmetic (both 'primitively recursive' and 'first-order') using something called construction, that is by not using 'not.' But by constructing the proof for every number (the 'ordinals') in the arithmetic (and since number is ... 'infinite,' there are a lot of them). This is called using constructive theory or 'ordinal analysis.'

He invented the thing.

Gödel used ordinal analysis (along with his own genius innovations) to disprove the Principia Mathematic system was consistent, but he also used Gentzen's work to provide a mapping between classical logic and intuitionistic logic.

You see, classic logic has three axioms, that is, three statements we accept as 'true' or foundational to the logic:

1. p -> (q -> p)   If you have a p, then q implies p is true

2. (p -> (q -> r)) -> ((p -> q) -> r) urgh. You read it.

3. ¬¬p -> p      "not-not p" implies p (if you don't have a not-p, then you have p)

We can live with the first two in intuitionistic logic, but the third one uses 'not,' and so can't be handled directly in that logic.

So, here's the thing, '¬' or 'not' is really just a short-hand for saying

¬p == p -> ⊥

That is 'p implies "bottom"' where ⊥ or 'bottom' is an unprovable statement in the logic: false, fail, void, icky-poo. More rigorously: a type that ... isn't, and this is known as an 'uninhabited type.'

You know: that.

So ¬¬p can also be said thus: (p -> ⊥) -> ⊥

And then there are two other translation functions from classical logic to intuitionistic logic that Gödel provides:

⊥^⊥ -> ⊥

(p -> q)^⊥ -> (p^⊥ -> q^⊥)

That's great, but it really doesn't get us anything, because we are still in classical logic, so we need a translator from classical logic to intuitionistic logic, and we use ⊥ as a superscript ...

... zzzzzz, whoopsie, continuing this convo in the next entry ... *blush*