Incompleteness ex Machina – proving Gödel's theorems in terms of algorithms [pdf]
1–10 of 33 posts
Re: Incompleteness ex Machina – proving Gödel's theorems in terms of algorithms [pdf]
#2I never understood the step about how a system that can do basic arithmetic can express the "I am not provable in F" sentence. Does anyone have an ELI30 version of that?
Re: Incompleteness ex Machina – proving Gödel's theorems in terms of algorithms [pdf]
#3> Godel was programming the integers. That is that. And he didn’t even know it at the time; truly impressive.
It seems strange to say that Godel didn't know it at the time -- Godel's work was part of the effort to mechanize logic, Hilbert's program, and the axiomatization effort started in response to contradictory calculus theorems, and followed Frege, Russel, Whitehead, et al.
Or rather, Godel's work showed that Russel's efforts to create a consistent and complete foundation for mathematics was fundamentally insufficient. Turing extended this work, by providing an explicit model of a calculating machine, to show that no algorithm could effectively determine the truth -- even without providing a proof -- locking the door on Hilbert's program that Godel had slammed shut.
Regardless, the entire point of Godel's work was exploring the relationship between our ability to "reason" and our ability "calculate" or "perform rote tasks".
(Missing details of the narrative aside -- it was a really good read.)
Re: Incompleteness ex Machina – proving Gödel's theorems in terms of algorithms [pdf]
#4I never understood the step about how a system that can do basic arithmetic can express the "I am not provable in F" sentence. Does anyone have an ELI30 version of that?
[deleted]
Re: Incompleteness ex Machina – proving Gödel's theorems in terms of algorithms [pdf]
#5I never understood the step about how a system that can do basic arithmetic can express the "I am not provable in F" sentence. Does anyone have an ELI30 version of that?
I’m not a mathematician, but the ELI30 version I got was that certain logical statements are labeled by certain number, such that doing arithmetic with those numbers corresponds to basic logical operations. So true statements about the number labels equal equivalent statements about the logical statements labeled by those numbers. So like, if 1 represents some logical statement and 2 represents some logical statement, and 3 represents another, then 1+2=3 is the same as saying that the two logical statements labeled by 1 and 2, when combined, produce the logical statement labeled by 3.
This idea is called Gödel numbering, and Wikipedia says “In formal number theory a Gödel numbering is a function which assigns to each symbol and formula of some formal language a unique natural number called a Gödel number (GN). ... A Gödel numbering can be interpreted as an encoding where a number is assigned to each symbol of a mathematical notation, and a stream of natural numbers can then represent some form or function.” That seems to sort of gel with what I heard, although it implies that maybe arthimetic operations like +, or -, aren’t actually involved. It might be more like 1 is a statement, and 2 is a statement, such that 12 is a combination of those two statements.
The point is that then you encode “this statement is not proveable” into numbers and show that you get a numerical contradiction (like 1=3 or something).
Re: Incompleteness ex Machina – proving Gödel's theorems in terms of algorithms [pdf]
#6I never understood the step about how a system that can do basic arithmetic can express the "I am not provable in F" sentence. Does anyone have an ELI30 version of that?
It is not about systems that can "do" basic arithmetic but that can "talk about" basic arithmetic.
The mere execution of basic arithmetic does not require the capability of manipulating propositions of basic arithmetic.
Doing basic arithmetic:
12 * ( 5 + 8 ) --> 12 * 13 --> 156
Talking about basic arithmetic:
a * ( b + c ) == a * b + a * c
The formal language needed to describe basic arithmetic is much more powerful than a simple execution engine, such as a stack engine, that can merely carry out basic arithmetic.
For example, I must be able to express that for all natural numbers x and y, if x = y, then y = x. The result could look like this:
∀ x,y ∈ N: x=y ⇔ y=x
Hence, this language must be able to express all Dedekind-Peano's axioms as well as every proposition provable from these axioms, along with their formal proofs.
In that sense, the Gödel numbering system is the "bytecode" of quite a serious programming (or at least, specification) language. (https://en.wikipedia.org/wiki/G%C3%B6del_numbering)
Re: Incompleteness ex Machina – proving Gödel's theorems in terms of algorithms [pdf]
#7> Godel was programming the integers. That is that. And he didn’t even know it at the time; truly impressive. It seems strange to say that Godel didn't know it at the time -- Godel's work was part of the effort to mechanize logic, Hilbert's program, and the axiomatization effort started in response to contradictory calculus theorems, and followed Frege, Russel, Whitehead, et al. Or rather, Godel's work showed that Ru…
Any chance OP is referring to "integer programming" (aka discrete optimization), which came about 20 years later?
Re: Incompleteness ex Machina – proving Gödel's theorems in terms of algorithms [pdf]
#8> Godel was programming the integers. That is that. And he didn’t even know it at the time; truly impressive. It seems strange to say that Godel didn't know it at the time -- Godel's work was part of the effort to mechanize logic, Hilbert's program, and the axiomatization effort started in response to contradictory calculus theorems, and followed Frege, Russel, Whitehead, et al. Or rather, Godel's work showed that Ru…
Any chance OP is referring to "integer programming" (aka discrete optimization), which came about 20 years later?
No. Integer programming in the operations research sense is "just" solving linear optimization problems with the constraint that the solution variables need to be integer.
In particular, IP doesn't really involve the multiplicative structure of the integers, which is crucial for how Gödel proved his results.
Also, I'd point out that while there's significant overlap between integer programming and discrete optimization, they're not the same thing. Integer programming is one tool used in discrete optimization among many.
Re: Incompleteness ex Machina – proving Gödel's theorems in terms of algorithms [pdf]
#9I never understood the step about how a system that can do basic arithmetic can express the "I am not provable in F" sentence. Does anyone have an ELI30 version of that?
The general idea is that if you have a logical system that can reason about numbers, if you figure out a way to encode the operators of the system itself as numbers, you can reason about the system itself within the system.
Re: Incompleteness ex Machina – proving Gödel's theorems in terms of algorithms [pdf]
#10> Godel was programming the integers. That is that. And he didn’t even know it at the time; truly impressive. It seems strange to say that Godel didn't know it at the time -- Godel's work was part of the effort to mechanize logic, Hilbert's program, and the axiomatization effort started in response to contradictory calculus theorems, and followed Frege, Russel, Whitehead, et al. Or rather, Godel's work showed that Ru…
Any chance OP is referring to "integer programming" (aka discrete optimization), which came about 20 years later?
Adding to atq2119's answer, integer programming is merely NP-complete. You really need full Turing computability to get the incompleteness results. The set of provable consequences of Peano arithmetic is RE-complete, and we know that NP != RE, so you definitely can't give an integer program that verifies that a formula is provable from PA, which is a necessary ingredient.