Notes on GEB

March 01, 2023 All posts

Dictionary

Chapter VIII: Typographical Number Theory:

Chapter XIII: BlooP and FlooP and GlooP:

Chapter IV: The Propositional Calculus

Rules.

The propositional calculus has no axioms only rules. It has a fantasy rule which manufactures new theorems e.g.:

[
    < P & Q >    // premise
    P            // separation
    Q            // separation
    <Q & P>      // joining
]
<< P & Q > -> < Q & P >>

Above churns out a new theorem: If P&Q then Q&P.

Fantasy rule is often called a “Deduction Theorem”.

The important thing is that anything can be “pushed-in” as a premise e.g.:

[
    P
    [
        Q
        P
        ~~P
    ]
    < Q -> ~~P >
]
< P -> < Q -> ~~P >>

Mechanical vs Intelligent Mode

With the propositional calculus one quickly invents shortcuts. If string <Q | ~Q> were needed at some point and <P | ~P> had been derived, we would use <Q | ~Q> as if it was also derived. But it was not, it is something that came from the I-mode instead of the M-mode.

In the same fashion we could also derive a second De Morgan’s rule:

<~x | ~y> and ~<x & y> are interchangeable

and use that as if it was part of the official list of the rules. But once start admitting derived rules as part of PC you lose its formality. If you keep stepping outside a formal system, what is the point of a formal system?

Chapter VIII: Typographical Number Theory

Rules

Examples of expressing number theoretic statements in TNT

Chapter IX: Mumon and Gödel

… the Zen attitude is that words and truth are incompatible, or at least that no words can capture truth.

Doko: I am seeking the truth. In what state of mind should I train myself, so as to find it?

Zen Master: There is no mind, so you cannot put it in any state. There is no truth, so you cannot train yourself for it.

Doko: If there is no mind to train, and no truth to find, why do you have these monks gather before you every day to study Zen and train themselves for this study?

Zen Master: But there is no temple here, so how could the monks gather? I have no tongue, so how could I call them together or teach them?

Doko: Oh, how can you like like this?

Zen Master: But if I have no tongue to talk to others, how can I lie to you?

Doko: I cannot follow you. I cannot understand you.

Zen Master: I cannot understand myself,

Dualistic, verbal thinking is the enemy. Humans naturally categorize/verbalize. Words can’t fully capture the thing they talk about. Therefore truths made from those words are impossible. Zen tries to break us from our dualistic nature, which falsely provides us with sense of something being “true”.

Chapter XIII: BlooP and FlooP and GlooP

Odd number function in BlooP:

DEFINE PROCEDURE ``ODD?`` [N]:
BLOCK 0: BEGIN
    OUTPUT <= NO
    IF REMAINDER[N,2] = 0, THEN
    QUIT BLOCK 0;
    OUTPUT <= YES
BLOCK 0: END

Expressibility and Representability

Summation is expressible in pq-system, because every instance of a+b=c predicate can be translated into it. Summation is also represented in pq-system, because every instance of a+b=c predicate that is true (2+4=6) is a theorem, and every instance that is false (2+4=20) is a non-theorem.

If a BlooP test can be written for some property of natural numbers, then that property is represtend in TNT.

What does it mean for some NT property to be represented in TNT? For instance we can say “b is odd”, in TNT notation that would translate to ~∃a:SS0*a = b. Once b is provided, it would result in a decidable string. By decidable string we mean that if we were to apply inference rules in reverse we would be guaranteed to arrive at something that can’t be reduced any further an is either an axiom or not. For instance, roughly something like this:

~∃a:SS0*a = SSS0    // b = SSS0, can be any number
∀a:~(SS0*a) = SSSO  // interchange
~(SS0*SS0) = SSS0   // specificiation
~(SSSS0) = SSS0     // multiplication (for argument we have this rule in TNT)
~(S0)=0             // drop S x 3
...
reduces to Axiom 1 (∀a:~Sa=0) or something that is not an axiom of TNT

would be equivalent in BlooP to a program ODD?[b], which gives either YES/NO given b.

There exists a function Bluediag[N] = 1 + BlueProgram{#N}[N], where BlueProgram are all 1-param functions written in BlooP. Bluediag that can be defined by humans (calculable), but can’t be defined in BlooP (computable in BlooP), since either:

(1) Bluediag[X] = BlueProgram{#X}[X] // given that Bluediag has index #X in the list of BluePrograms

or

(2) Bluediag[X] = 1 + BlueProgram{#X}{X}

From the two we can only “save” the (2) one from being a falsity, since if (1) is true, both (1) and (2) are false. Therefore, Bluediag is not part of the pool for BlooP functions.

We can add non-bounded loops to BlooP and get a new language called FlooP. With this new language we might hope to be able to define all functions that can be defined using human language. However if we filter out all the terminating functions from computable but non-terminating functions we get a pool of RedPrograms. We can use the same diagonalization approach we used for BlooP, to show that there is a function called Reddiag that does not belong to that pool:

Not sure why Reddiag can’t belong to non-terminating computable functions though… 

Reddiag[N] = 1 + RedProgram{#N}[N]

Chapter XIV: TBA

Proof-pair

Proof-pair: two natural numbers, m and n respectively, form a MIU-proof-pair iff m is the Gödel number of a MIU-system derivation where bottom line is the string with Gödel number n.

For instance, m = 313113111301, n = 301 decoded into MIU:

MI
MII
MIII
MUI

Theorem-number: n is a theorem-number if some value of m exists which forms a proof pair with n.

Translating “MU is a theorem of the MIU-system”:

MIU-PROOF-PAIR{a, a'} // BlooP program & therefore representable in TNT
MU=30=SSSS....S0
∃a:MIU-PROOF-PAIR{a, SSS....S0/a'}

Substitution

A test could be written in BlooP to check if every free variable could be replaced by a' (e.g. SS0) in a Goldel’s number a in order to produce a given input a''. Let’s call this function SUB{a, a', a''}.

Usage example:

a = SSS...S0  // 262,111,262 S's, which in TNT translates to a=a
a' = SS0      // 2
a'' = SS..S0  // 123,123,666,111,123,123,666
SUB{a,a',a''} // YES

Arithmoquining

Quining – operation of preceding some phrase by its quotation: “IS A SENTENCE FRAGMENT” IS A SENTENCE FRAGMENT.

Make TNT statement about itself:

a=SO        // random TNT sentence with one free variable
SSS...SO=SO // left side has 262,111,123,666 S's, which translate to "a=SO" in TNT

This is also the same as SUB{a'', a'', a'} = ARITHMOQUINING{a'',a'}.

Gödel’s sentence G

There is a mathematical formulation of Gödel’s string done by Gödel. There is also an isomorphic version done by Hofstadter, where he briliantly shows how to do the same using natural human language. I am wondering if looking at it from the perspective of a conversation between a human and a machine would be even more intuitive. Let’s say it is a conversation between Achilies and a function called GPT.

GPT: When <something> refers to itself, it is false!

You can give anything to GPT, it will make it refer to itself, will validate it and correctly respond that it is “false”.

Achilies: is running away
GPT: is '"is running away" is running away' a falsity? YES!
Achilies: I suppose the '"is running away" is running away' sentence is a non-sense, so you are correct!

We can throw mathematical statements to GPT too. But how can a math sentence refer/quote itself? This is Gödel’s trick, where you take a string of symbols expressing some open statement in mathematics (e.g. a = 0) and you encode it as a number (e.g. 333,111,000). You can then use that number to replace all free variables inside an open statement resulting in a new string/statement e.g. 333111000=0. This statement has a double meaning. First it has a literal meaning, that can be detected in M-mode (mechanical), where in this case some large number is claimed to be equal to 0, which is obviously false. It can also be interpreted in I-mode (human intelect), where it’s meaning is (a=0)=0. This way we just made a statement a=0 talk about itself. Initially, it said “ is equal to 0", we replaced that with `a=0`, which is the statement itself! After the replacement the statement now says (in I-mode) -- "I am equal to 0". A machine would not know that, since it operates only in the M-mode, but human would, since it operates in both. This type of procedure of making an open mathematical statement talk about itself is called _arithmoquining_.

Achilies: a=0
GPT: is `333111000=0` a falsity? YES!
Achilies: I suppose both `(a=0)=0` and `333111000=0` are false, so you are correct again!

Achilies: Are you yourself false when you refer to yourself?
GPT: When <GPT> refers to itself, it is false!
Achilies: So you are false.
GPT: Correct, I am false.