Adventure Game Studio  Forums
Community => General Discussion => Topic started by: KyriakosCH on 05 May 2021, 07:37

Hi, this is another weird thread by me :)
I feel like presenting some stuff, since they may be of interest, and it will also help me practice. While I am not yet at the level I want to be regarding this, it doesn't hurt (and likely you can't tell anyway ^_^  just a joke, I am sure with a number of programmers here, a few will be familiar with this or at least Turing's work which rests on it).
The following are not even just in medias res, given it is near the end of Goedel's work on formal logic systems. It follows the main idea that if you have any notation in symbols (for example: a=a, or S0), you preserve all the info in the original symbols when you turn them into numbers. Also, it doesn't matter what number you will choose. Eg for the variable "a" you can set (taking this from a specific book, when this arithmetization is used: Hofstadter's "Goedel,Escher, Bach") the number 262, for "=" the number 111, for S (which means "successor; the next natural number) the number 123, and for 0 (in S0) the number 666. Now a=a is also written as 262111262, and S0 is also written as 123666.
A.
1)Let's say we had the formula: a=S0, which just means that a variable (a) is argued to be a specific number, in this case the successor of 0, which is 1 (so a=1). In the new code we used, this statement would become:
262111123666. So we say that 262111123666 is the "Goedel number" of the statement a=S0.
2) But using Godel's procedure, we will now actually replace the variable a, in a=S0, with the Goedel number of the statement... This will turn a=S0 to: SSSS....S (this means you write S 262111123666 times) 0 = S0. In other words it presents the statement that 262111123666=1, which isn't true. It's ok, we aren't yet done (but do notice that if your formula claimed that a is not equal to S0, it would still be correct after the goedelization of the variable a). On to the next part:
3) Our new formula, which we got in step2 when we replaced the variable a with the Goedel number of the formula a=S0, also has a Goedel number. Of course it no longer is 262111123666, since now instead of a variable a, we have that number to the left of the identity. So the new Goedel number of the formula is this instead: 123123123...123 (you write 123 262111123666 times...) 111 123666. It is a monstrous number, but inevitably happens. More crucially, the procedure of replacing twice with the same number (we used 262111123666 both in steps 2 and 3) is important due to ties to enumerable sets (but this isn't for this post; this process is also called diagonalization, due to Cantor). Let's move to the revelation of what we (following Goedel) can do with such substitutions:
B.
In any formal logic system, it is known (has been proven) that certain processes are testable, by which is meant that they can be shown to be true or not, in a finite number of steps. One of those processes is called "proof pairs". Now, proof pairs are easy to understand: they are two numbers, the first being the number of a proof in that logic system, and second being the number of the final statement of that proof (which is also called "the theorem"). Those numbers are Goedel numbers of the entire group of sentences in the proof, and then only the last sentence of the proof. It has been shown that you can test finitely for such pairs, and I won't go more into that now. But notice that to say a pair of Goedel numbers is a proof pair, is the same as to say that the second number in the pair is the Goedel number of the theorem, so (to put it differently) it is to say that there exists a theorem in this system with that number.
1. Goedel wrote a formula which alludes to the nonexistence of a truth pair, between (say) a and a', which moreover inevitably are tied to the goedel number to replace a' in a second formula (like we did for a simple formula, in step A2!), so are tied to a new pair a',a'' (a'' is the second goedelization, like we did in step A3).
2. This is the final step. In step1, above, we got to a second replacement of a variable with the Goedel number of its formula. Now we repeat the process, and replace a (which is the only free variable in the formula; a' and a'' are tied to whatever a is) with the Goedel number of step 1's formula. The final formula we would get... is the famous "G sentence", of Goedel. And what it says is very interesting:
3. The G sentence
This sentence, G, also has (like any other sentence/formula) a Goedel number. The Goedel number of G is (as is to be expected) gotten by the same replacement procedure; any free variable (eg a) is replaced by the number of the entire formula.
But what does the G sentence say, exactly?
It says that there do not exist numbers for a and a', such that they are on the one hand a proof pair, and also a' is the diagonalization of a (in other words, a'' is the Goedel number of the new formula when you replace the variable a with the goedel number of the original formula).
But we already know that there always will be a number which is the Goedel number of ANY formula (it's a simple replacement; can't be disallowed). So it follows that the statement G is that "There is no number a that forms a truth pair with the diagonalization of a').
From this follows (since there is no truth pair a,a') that the sentence just tells us that any sentence which has a Goedel number that was gotten by diagonalizing the formula in part B of this post, is not a theorem in the system.
And this is the end, we have now a sentence in the system that says "This is not a theorem in the system". So what, you might ask. So everything, since by making the system examine its own self (you insert a sentence that actively claims it is not a theorem...) you can only make the system fail:
If your G sentence ends up having a truth pair number with the (likely many) sentences which led to it, then it is by definition a theorem in the system. But itself says that it is not. Hence your system just proved something false.
If your G sentence doesn't have a truth pair number, it is false. But itself claims that it is false, so actually it is true. This means that while the system avoided having proven something against itself,(G isn't a true sentence), it did fail to prove a sentence which actually is true (since G states it is false).
In conclusion, the ability to write a sentence G into a system means that either the system is not consistent (can prove also false things), or that it is not complete (doesn't include all true statements).