## Gödel's Language
### Or: The God of recursion
### Or: The El of self-reference
### Or: Downstream of the side remark
### Or: Finally a built-in Number Type
### Or: The Second Definition
0: Ok so, to really understand Gödel's definition, it's not enough to just talk about it.
1: Coming from someone who talks as much as you do, that's saying a---
0: Talking wasn't Gödel's style. So in this file we're gonna stop talking and shut up and be curt.
1: Great! Let's be---
0: No talking.
It's time to be curt, and speak the language of Gödel.
_(Narrator: The file falls silent, as the surrounding format becomes monospaced...)_
```python
# =================================
# Gödel's Definition of Computation
#
# The built-in functions of μ-lang.
# =================================
and_gödel_said = """
We now insert a parenthetic consideration that for the
present has nothing to do with the formal system P.
"""
# 1: What's P?
# 0: Principia Mathematica.
# 1: The crazy Russell book no one reads?
# 0: Yeah.
# 1: How am I supposed to follow this if I don't know
# anything about that system?
# 0: He just said it has nothing to do with that.
# Just be quiet and follow me.
and_gödel_said += """
First we give the following definition:
A number-theoretic function φ(x₁, x₂, …, xₙ) is said to
be recursively defined in terms of the number-theoretic
functions ψ(x₁, x₂, …, xₙ₋₁) and μ(x₁, x₂, …, xₙ₊₁) if
φ(0, x₂, …, xₙ) = ψ(x₂, …, xₙ),
φ(k + 1, x₂, …, xₙ) = μ(k, φ(k, x₂, …, xₙ), x₂, …, xₙ)
hold for all x₂, …, xₙ, k.
"""
# 1: What the hell was all that?
# 0: He's just defining recursion.
# 1: Was that the definition we've been waiting for?
# 0: No, that's just the setup.
and_gödel_said += """
A number-theoretic function φ is said to be recursive
"""
# 0: Here comes the definition.
# 1: Shh, I can't hear it!
and_gödel_said += """
if there is a finite sequence of number-theoretic functions
φ₁, φ₂, …, φₙ that ends with φ and has the property that every
function φₖ of the sequence is recursively defined in terms of
two of the preceding functions, or results from any of the
preceding functions by substitution, or, finally, is a constant
or the successor function x + 1.
"""
# 1: Was that it?
# 0: Yep!
# 1: That didn't even feel like a definition.
# 0: Why not?
# 1: What's a number theoretic function?
# 0: It's simpler than it sounds.
# 1: I have some questions. Can we translate this into something more precise?
# 0: Of course. Follow me.
```
1: Wait why are we outside of the code? I said _more_ precise.
0: Just coming up for some air. Ok, what's the question?
1: I'm not sure what Gödel means.
0: You understand recursion right?
1: Of course Zero, I'm a professional developer.
0: So what's the issue?
1: What's a constant function?
0: Oh c'mon you know what a constant function is.
1: I know what it usually means. I want to know what Gödel means.
0: He just means "constant."
1: Zero don't be dumb.
0: How is this "dumb"?
1: Show me what Gödel means by constant.
0: Here's one:
```python
def constant(n):
return k
```
1: What's $k$.
0: It's a constant.
1: Where did you get it from?
0: What?
1: Is it a constant or a variable?
0: A constant.
1: Ok, which number is it?
0: We haven't decided. It's unspecified.
1: HOW IS THAT NOT A VARIABLE?
0: What's the problem?
1: Do a simpler function. No free constant-y variable-ish things.
0: Ok, here:
```python
def five(n):
return 5
```
1: Where did you get that $5$ from?
0: From the number five. It's five.
1: ZERO DON'T BE DUMB.
0: How can I help?
1: Zero, we just got done with Church's system where we had to implement literally everything, including numbers.
And the implementation of numbers wasn't like "totally obvious."
We had to think for a while.
And when we got a definition we were happy with, numbers like 0 and 1 ended up being _two argument functions._ Or one argument functions that returned one argument functions that returned -- not numbers -- but the first argument applied "number-many-times" to the second one.
That was weird.
And it kinda messed with my head at first.
But once I understood it, I felt like I understood a lot about the mindset of the people like Church and Gödel who create these systems.
In these low level systems, we have to implement everything from scratch.
Like we have literally nothing except what we explicitly build-in when we define the system.
Absolutely nothing else exists. So whenever we want a thing, we have to build it step-by-step, without skipping steps, from the bare bones built-ins of whatever system we're in.
0: What's the question?
1: Well after all that, I don't think it's unreasonable for me to be not-entirely-sure what Gödel means by words like "constant"!
0: Can you ask a more specific question?
1: Is this a constant function in Gödel definition?
```python
def what(n):
return n
```
0: No, that's the identity.
![[one-looks-at-mendelsons-definition-of-recursive-functions-01.png]]
![[one-looks-at-mendelsons-definition-of-recursive-functions-02.png]]
![[one-looks-at-mendelsons-definition-of-recursive-functions-03.png]]
![[one-looks-at-mendelsons-definition-of-recursive-functions-04.png]]
![[one-looks-at-mendelsons-definition-of-recursive-functions-05.png]]
![[one-looks-at-mendelsons-definition-of-recursive-functions-06.png]]
![[one-looks-at-mendelsons-definition-of-recursive-functions-07.png]]
![[one-looks-at-mendelsons-definition-of-recursive-functions-08.png]]
![[one-looks-at-mendelsons-definition-of-recursive-functions-09.png]]
![[one-looks-at-mendelsons-definition-of-recursive-functions-10.png]]
## Gödel's μ-lang (0.0.1)
```python
def zero(n):
# 1: Did you name this function after yourself?
#
# 0: No, Gödel did. This is the zero function.
# Gödel just said "Let's assume the function
# that always returns zero is built in.
#
# 1: What about the function that returns one?
#
# 0: That one we have to implement.
#
# 1: Feels a bit unfair.
#
# 0: It's coming up next. Quit talking and listen.
""" Gödel: zero is built-in """
return 0
def incr(n):
""" Gödel: plus one is built-in """
return n+1
def proj(i, *args):
""" Gödel: picking an arg is built-in """
return args[i]
def comp(f, *hs):
""" Gödel: function composition is built-in """
def g(*args):
xs = (h(*args) for h in hs)
return f(*xs)
return g
def rec(f, g):
""" Gödel: recursion is built-in """
def h(n, *xs):
if n == 0:
return f(*xs)
return g(n-1, h(n-1, *xs), *xs)
return h
def mu(p):
""" unbounded while loops are built-in """
def m(*xs):
n = 0
while True:
if p(n, *xs) == 0:
return n
n += 1
return m
# =========================
# Gödel's Standard Library
#
# Using the μ-lang builtins
# to implement a standard
# library of simple General
# Recursive Functions we'll
# need in order to write a
# compiler that translates
# the formal theory of first
# order (Peano) arithmetic
# into statements about the
# arithmetic of positive
# whole numbers which we can
# then re-express within,
# well, arithmetic. -K.G.
# =========================
def const(k):
return lambda *xs: k
zero = const(0)
one = const(1)
id = lambda x: proj(0, x)
# predecessor
pred = rec(zero, lambda n, y: n)
add_base = id
add_step = lambda n, y, x: incr(y)
add_raw = rec(add_base, add_step)
add = lambda x, y: add_raw(y, x)
mul_base = zero
mul_step = lambda n, y, x: add(y, x)
mul_raw = rec(mul_base, mul_step)
mul = lambda x, y: mul_raw(y, x)
exp_base = one
exp_step = lambda n, y, x: mul(y, x)
exp_raw = rec(exp_base, exp_step)
exp = lambda x, y: exp_raw(y, x)
sub_base = id
sub_step = lambda n, y, x: pred(y)
sub_raw = rec(sub_base, sub_step)
sub = lambda x, y: sub_raw(y, x)
is_zero = rec(one, lambda n, y: zero())
# sign: sign(0) = 0, sign(n) = 1 otherwise
sign = rec(zero, lambda n, y: one())
# leq(x,y) is 1 if x <= y else 0
leq = lambda x, y: is_zero(sub(x, y))
# eq(x,y) is 1 if x == y else 0
eq = lambda x, y: mul(leq(x, y), leq(y, x))
# neq(x,y) : 1 if x != y else 0
neq = lambda x, y: sign(sub(eq(x, y), one()))
# max/min, overriding the python builtins
max = lambda x, y: add(sub(x, y), y)
min = lambda x, y: sub(add(x, y), max(x, y))
def geq(x, y):
return leq(y, x)
def lt(x, y):
return sign(sub(y, x))
def examples():
return {
"pred(0)": pred(0),
"pred(5)": pred(5),
"add(3,4)": add(3, 4),
"mul(3,4)": mul(3, 4),
"exp(2,5)": exp(2, 5),
"sub(7,10)": sub(7, 10),
"sub(10,7)": sub(10, 7),
"is_zero(0)": is_zero(0),
"is_zero(9)": is_zero(9),
"leq(3,7)": leq(3, 7),
"leq(7,3)": leq(7, 3),
"eq(9,9)": eq(9, 9),
"eq(9,8)": eq(9, 8),
}
if __name__ == "__main__":
from pprint import pprint
pprint(examples())
```
1: Wait we never used `comp`.
0: _(Reading back through code.)_ ...dammit.
1: I can't tell if this is allowed.
0: Damn these logic books are so vague.
1: Is it possible to do the same thing using `comp`?
0: Ugh... ok, one sec.
## Gödel's μ-lang (0.0.2)
```python
# =========================
# Gödel's Standard Library
#
# Using the μ-lang builtins
# to implement a standard
# library of simple General
# Recursive Functions we'll
# need in order to write a
# compiler that translates
# the formal theory of first
# order (Peano) arithmetic
# into statements about the
# arithmetic of positive
# whole numbers which we can
# then re-express within,
# well, arithmetic. -K.G.
#
# P.S. This time we make
# sure to actually use the
# comp builtin instead of
# all those lambdas from
# before. -K.G.
# =========================
def const(k):
return lambda *xs: k
# curried version of proj to make
# comp less of a pain to work with
mkproj = lambda i: (lambda *xs: proj(i, *xs))
zero = const(0)
one = const(1)
id = lambda x: proj(0, x)
# predecessor
pred = rec(zero, lambda n, y: n)
add_base = id
add_step = comp(incr, mkproj(1))
add_raw = rec(add_base, add_step)
add = lambda x, y: add_raw(y, x)
mul_base = zero
mul_step = comp(add, mkproj(1), mkproj(2))
mul_raw = rec(mul_base, mul_step)
mul = lambda x, y: mul_raw(y, x)
exp_base = one
exp_step = comp(mul, mkproj(1), mkproj(2))
exp_raw = rec(exp_base, exp_step)
exp = lambda x, y: exp_raw(y, x)
sub_base = id
sub_step = comp(pred, mkproj(1))
sub_raw = rec(sub_base, sub_step)
sub = lambda x, y: sub_raw(y, x)
is_zero = rec(one, comp(zero))
# sign: sign(0) = 0, sign(n) = 1 otherwise
sign = rec(zero, comp(one))
# leq(x,y) is 1 if x <= y else 0
leq = comp(is_zero, sub)
# eq(x,y) is 1 if x == y else 0
eq = comp(mul, leq, comp(leq, mkproj(1), mkproj(0)))
# neq(x,y) : 1 if x != y else 0
neq = comp(sign, comp(sub, one, comp(eq, mkproj(0), mkproj(1))))
# max/min, overriding the python builtins
max = comp(add, comp(sub, mkproj(0), mkproj(1)), mkproj(1))
min = comp(sub, comp(add, mkproj(0), mkproj(1)), comp(max, mkproj(0), mkproj(1)))
def geq(x, y):
return comp(leq, mkproj(1), mkproj(0))(x, y)
def lt(x, y):
return comp(sign, comp(sub, mkproj(1), mkproj(0)))(x, y)
def examples():
return {
"pred(0)": pred(0),
"pred(5)": pred(5),
"add(3,4)": add(3, 4),
"mul(3,4)": mul(3, 4),
"exp(2,5)": exp(2, 5),
"sub(7,10)": sub(7, 10),
"sub(10,7)": sub(10, 7),
"is_zero(0)": is_zero(0),
"is_zero(9)": is_zero(9),
"leq(3,7)": leq(3, 7),
"leq(7,3)": leq(7, 3),
"eq(9,9)": eq(9, 9),
"eq(9,8)": eq(9, 8),
}
if __name__ == "__main__":
for k,v in examples().items():
print(f"{k} = {v!r}")
```
## The Second "First Standard Library"
TODO:
1. Implement these. Should be pretty simple.
2. Notice that they're impractically slow.
3. Optimize them and make them actually useful.
4. Do it with the pure UTF-8 Gödel numbering if possible.
![[godel-collected-works-117.png]]
![[godel-collected-works-118.png]]
![[godel-collected-works-119.png]]
![[godel-collected-works-120.png]]
![[godel-collected-works-121.png]]
![[godel-collected-works-122.png]]
![[godel-collected-works-123.png]]
![[godel-collected-works-124.png]]
![[godel-collected-works-125.png]]
![[godel-collected-works-126.png]]
![[godel-collected-works-127.png]]
![[godel-collected-works-128.png]]
![[godel-collected-works-129.png]]
![[godel-collected-works-130.png]]
![[godel-collected-works-131.png]]
![[godel-collected-works-132.png]]
## Enter Al
1: Why did we define all those functions up there?
0: To see what Gödel was doing, how he defined computation, and why it wasn't convincing.
1: Yes I know but what's the point of doing that?
0: To show that it wasn't convincing!
1: I swear zero, if this was all for nothing I'm gonna---
0: No no, I mean Gödel.
1: What about Gödel?
0: Gödel's definition of computation wasn't convincing to Gödel.
1: Then why did he suggest it?
0: He didn't know he was defining all of computation! He was just defining the function he'd need to parse the hexdumps.
1: And that turned out to be _all of computation?!_
0: In a sense. Mostly because "Is this provable" requires a while loop.
1: So Gödel's definition didn't convince Gödel?
0: Right. But he wasn't really focused on the computation side of the paper. His paper caused enough of a stir for other reasons. I mean, at the time, back in 1931, people didn't know what to do with Gödel's results.
1: What do you mean "didn't know what to do" with them?
0: Well, Hilbert got angry.
![[godel-result-fallout-00.jpg]]
1: Weird reaction.
0: Bertrand Russell sort of gave up on logic.
1: Wow really?
0: Though to be fair I think Wittgenstein sort of Russell'ed Russell.
1: Russell'ed Russell?
0: Yeah, like how Russell did to Frege. Without intending to, he sort of made Frege give up on logic. Wittgenstein sort of did that to Russell. Plus Russell was understandably a bit exhausted after writing one of the most densely technical textbooks of all time.
![[godel-result-fallout-01.jpg]]
0: Anyways, at the time, Gödel wasn't convinced that he had captured all of computation.
1: What convinced Gödel?
0: Someone named Al.
1: Church?
0: Turing!
1: Oooooh!
0: About 32 years after Gödel's paper was first published, he added a note to the end of this paper about Turing.
![[godel-collected-works-136.png]]
0: Here's Steve on the matter.
> Steve Kleene: Well as I say, I don't know how firmly convinced Gödel was that his General Recursive Functions represented all effectively calculable functions.
>
> Gerald Sacks: He seemed very skeptical.
>
> Steve Kleene: I think he was skeptical. And it may well be that Turing's presentation was what brought Gödel around.
0: Perfect timing. Next file.
1: Turing time?
0: Turing time.
1: Hooray! We're finally at the programming.
0: This was all progra---
1: Get moving!
0: You're dumb.
1: Shut up and get in here.
goto: [[lost+found/5/1]]