> 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.)
Perhaps Gödel had a vague notion of what he was up to. Nonetheless, the whole concept of universal computation was still half a decade away and higher level languages several decades. So I think the remark is still essentially accurate. He had to work without all the modern cognitive conveniences such as for-loops and if/else branching.
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.
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.
One thing that seemed a bit surprising to me, especially in light of the paper's strong focus on computation, is that the assumption that the axiomatization is effective is only mentioned in a footnote, and even there it is not explained but we are told to "don't worry about it" if we don't know what that means.
Yet, the code pieces in the paper make critical use of this assumption in that they assume that we can decide (with an algorithm) whether or not a string is a proof. This only works if the axioms are recursive.
So, maybe you could consider adding a short explanation about this to the paper?
Every time I said "either/or" I was making use of the law of the excluded middle. But I didn't add a detailed disclaimer explicitly highlighting this fact either. Should I have? I think it's okay to just take some things for granted.
Though, I admit that I have never spent much thought on non-effective axiomatizations. So I'm open to be educated.
The proofs you present are entirely constructive and work without appealing to the law of the excluded middle! As was also pointed out by Gödel himself about his proofs, they are obtained in an "intuitionistically unobjectionable manner".
When you say "either/or" in the paper, you make case distinctions that are intuitionistically non-contentious, i.e., you say "either F ⊢ G, then contradiction, so F ⊬ G, or F ⊬ G, then contradiction etc.", but the point is that G is explicitly constructed, so this is intuitionistically acceptable.
In contrast, the other assumption I mentioned is used in the paper and in fact essential for its proofs.
I agree in the cases where I argue "suppose, then..." But there are instances where I argue "either this is the case, or this is not the case." Unless there are multiple laws of the excluded middle, that's an application of it.
In any case, that was merely an example. The central point I was making doesn't depend on this.
In the paper, it is assumed — per footnote 1 — that the formal systems under discussion are effectively axiomatized. I assume this means that their theorems are recursively enumerable, is this correct? If so, then this means that determining whether a string is a proof may only be semi-decidable, and may not halt for strings that are not proofs.
However, as I mentioned, in the remainder of the paper, it appears to me that you assume that the theorems are not only recursively enumerable, but in fact recursive. For example, in the proof of Theorem 4 on page 5, the lines stating "if s is a proof ..." seem to assume that this check always terminates, requiring assumptions that the original proof does not and therefore weakening the obtained result.
In my opinion, adding a short explanation about how this can be salvaged (it can!), or at least precisely specifying what is assumed, could improve the presentation.
I'm only assuming that checking whether "does s prove S?" is a recursive property. That's not the same as demanding "is S provable?" to be recursive.
Upon reflection I agree that effective axiomatization isn't actually that difficult to explain. So I've changed the footnote to say: "For the purpose of this discussion every formal system is effectively axiomatized by definition. This basically just boils down to the fact that proofs are computer checkable."
I was initially worried that this might raise the question what non-effective axiomatizations are all about. That's not a can of worms I want to open. But I think this should be fine.
Thank you for adding this! Still, it is not so straight-forward to conclude, from just the premise that the system is effectively axiomatized (i.e., its theorems are recursively enumerable), that "does s prove S" is a recursive property.
In my opinion, if the assumption is that "proofs are computer checkable" (i.e., "does s prove S" is a recursive property, which is what is required in the paper), then it would be good to either state that as the key assumption, or state for example that this follows via Craig's theorem from the assumption that the system is effectively axiomatized:
Interestingly, from this theorem it follows that such a system can be re-axiomatized so that "S is a theorem" is even a primitive recursive property. In fact, when Gödel wrote "rekursiv" around 1930, he meant the class of functions that we now call primitive recursive. Because of Craig's theorem, we know that primitive recursive, recursive, and recursively enumerable can be used interchangeably in the definition of effective axiomatization, but without such a theorem, it would be a leap to conclude one from the other.
I don't see why there's a theorem required here. Let our formal system be effectively axiomatized. Then by definition its axioms are a recursive set. So I can just check a proof by starting at the top and verifying that every line is either an axiom or follows from a line above via an inference rule. Both of these two checks are recursive. Hence, proof checking is recursive.
Also, the Wikipedia article doesn't say that Craig's Theorem proves recursively enumerable axiomatizations equivalent to (primitive) recursive axiomatizations. I would find it very surprising if this was a consequence. It only says that a recursively enumerable set of formulas (e.g. the provable sentences in Peano arithmetic, not merely its axioms) can be given a (primitive) recursive axiomatization. That's a very much weaker claim.
"Let our formal system be effectively axiomatized. Then by definition its axioms are a recursive set."
"effectively axiomatized" means that the theorems are recursively enumerable. It does not immediately follow that the axioms are a recursive set. However, by Craig's theorem, we can then re-axiomatize so that the axioms are a recursive set, even a primitive recursive set!
You are of course right about the consequences: In the post above, I meant to say that due to this theorem, it makes no difference whether we require the axioms to be recursively enumerable, recursive, or primitive recursive. But still, without this theorem, it would be a leap to conclude from "the system is effectively axiomatized" that "s
is a proof of S" is recursive.
"If T is effectively axiomatized, in the sense that there is an algorithm for deciding whether or not a given sentence is an axiom of T,..."
In Computability: Turing, Gödel, Church and Beyond Martin Davis even makes the definition "T is axiomatizable if it has an axiom set that is computable" on page 42.
And that's also the definition Shoenfield gives on page 125 of Mathematical Logic.
Besides, "effective" has always been a synonym for "computable", "recursive", or "decidable" whenever I've encountered it in this context.
Also, I must insist that "it makes no difference whether we require the axioms to be recursively enumerable, recursive, or primitive recursive." is not what Craig's Theorem says. This is dangerously close to claiming that recursively enumerable sets are recursive which is plainly untrue. If recursively enumerable axioms (not just recursively enumerable theorems) are indeed interchangeable with recursive axioms, then I'd like to hear more about that.
Yes, you are right: This is not what Craig's theorem says! It is enough to assume that the theorems are recursively enumerable. From this, it follows that there is an axiomatization where the axioms are recursive.
The key point is that I would find it a worthwhile addition to the paper to somehow make clear that "s proves S" is assumed to be decidable. Since you have done this: Thank you!
Thank you for this. Since reading Gödel, Escher, Bach, I've always wondered about how to think of a "dishonest" but consistent formal system. Can we really say it lies? Or is it just describing something similar but weirdly different from natural numbers?
It's nice to know that you don't need it; it's just a sideshow.
You can call it "similar but weirdly different" in the same sense that the people who are subject to propaganda live in similar but weirdly different realities. What is true depends on your viewpoint.
When a formal system says: "this computation halts after some number of steps", then under the default interpretation that means that after say 10000 steps the computation really halts. But in the "similar but weirdly different" reality where transfinite numbers exist the above claim can still be considered true if it runs indefinitely. One simply has to entertain the idea that "some number of steps" might mean a transfinite number of steps.
In other words, yes, we can say that the formal system lies provided we accept that what is and what isn't a lie depends on the viewpoint.
Yes, nonstandard models of arithmetic are what I was thinking of. I don't know much about them, but here is my intuition:
It's a bit odd to think that nearly all "natural" numbers are so large that we can never calculate them, even in principle (because it would take more bits than exist in the universe). Even constructive proofs can describe calculations that could never actually be carried out. The boundary between what I might call "practical" numbers and the larger natural numbers is fuzzy (since it depends on technology), but maybe admitting transfinite numbers exist among the very large naturals would be a way of dealing with it? A way of saying "induction takes us beyond anything we can really know; here be dragons".
And similarly, there are programs that in practice would never halt (because not enough time in the universe), even though theoretically they do.
I don't suppose that's very useful, though, so nice to know it can be avoided.
I feel like I didn't argue this as clearly as I could have. Let me make one more addition.
Throughout the discussion I'm making the tacit assumption that there is one standard viewpoint to which we adhere. That's the "normal" world. Numbers are finite and halting programs halt after finitely many steps. It is from this fixed viewpoint that I'm declaring certain claims to be lies. They are not lies in some grand universal sense.
I realize that the word "lie" usually also entails an accusation of deliberate deception. But that's immaterial here. Formal systems don't have intentions. They simply make claims.
I 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.
It should be noted that the special sauce that makes arithmetic really difficult is induction.
Induction isn't just reasoning about computation, (i.e simple equations). Instead it is reasoning about reasoning about equations (i.e. reasoning about all equations).
But it should be pointed out that induction is essentially unrelated to Gödel's theorem.
For example, Robinson Arithmetic is a finitely axiomatized theory whose axioms contain only one existential quantifier, but just like full (Peano) arithmetic, it is subject to Gödel's incompleteness theorems.
From the other side of the fence, another thing to look at would be the decidability of presburger, and skolem arithmetic, the following paper then goes over the extensions of these, which render the result undecidable.
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.2.21...
Thanks for the answer! Out of curiosity what about systems we can prove able to "do" basic arithmetic, ignoring whether they can talk about it?
I'm imagining the difference between a system that can show "P(n)" for any n, rather than a system that can show "P(n) for any n."
It seems like the former must come with a proof about the system. The quantifiers "for any n" have to come somewhere. If they aren't embedded within the system, do we still end up with a system that must be able to express "This sentence is not provable?"
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).
1. Encode the propositions of your formal system in ascii (or whatever encoding you like)
2. Observe that the resulting bit patterns can be interpreted as numbers, and so the rules of inference of your formal system can be expressed as mathematical operations on those numbers
3. Profit
Goedel had to invent all of that from scratch. On top of that, he had to describe how to actually carry out step 2 without the benefit of a programming language. All he had to work with was raw math. So his encoding was very different from ascii, or anything you are familiar with, because it was "optimized to run on raw math" rather than a digital computer.
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.
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.)
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.
I'd like to mention that this article is currently slated for publication in the Bulletin of the European Association for Theoretical Computer Science. A revised draft can be found at: https://github.com/SOberhoff/incompleteness_ex_machina/relea...
I haven't handed it over yet, so we'll have to see about further changes.
One thing that seemed a bit surprising to me, especially in light of the paper's strong focus on computation, is that the assumption that the axiomatization is effective is only mentioned in a footnote, and even there it is not explained but we are told to "don't worry about it" if we don't know what that means.
Yet, the code pieces in the paper make critical use of this assumption in that they assume that we can decide (with an algorithm) whether or not a string is a proof. This only works if the axioms are recursive.
So, maybe you could consider adding a short explanation about this to the paper?
Though, I admit that I have never spent much thought on non-effective axiomatizations. So I'm open to be educated.
When you say "either/or" in the paper, you make case distinctions that are intuitionistically non-contentious, i.e., you say "either F ⊢ G, then contradiction, so F ⊬ G, or F ⊬ G, then contradiction etc.", but the point is that G is explicitly constructed, so this is intuitionistically acceptable.
In contrast, the other assumption I mentioned is used in the paper and in fact essential for its proofs.
In any case, that was merely an example. The central point I was making doesn't depend on this.
However, as I mentioned, in the remainder of the paper, it appears to me that you assume that the theorems are not only recursively enumerable, but in fact recursive. For example, in the proof of Theorem 4 on page 5, the lines stating "if s is a proof ..." seem to assume that this check always terminates, requiring assumptions that the original proof does not and therefore weakening the obtained result.
In my opinion, adding a short explanation about how this can be salvaged (it can!), or at least precisely specifying what is assumed, could improve the presentation.
I'm only assuming that checking whether "does s prove S?" is a recursive property. That's not the same as demanding "is S provable?" to be recursive.
Upon reflection I agree that effective axiomatization isn't actually that difficult to explain. So I've changed the footnote to say: "For the purpose of this discussion every formal system is effectively axiomatized by definition. This basically just boils down to the fact that proofs are computer checkable."
I was initially worried that this might raise the question what non-effective axiomatizations are all about. That's not a can of worms I want to open. But I think this should be fine.
In my opinion, if the assumption is that "proofs are computer checkable" (i.e., "does s prove S" is a recursive property, which is what is required in the paper), then it would be good to either state that as the key assumption, or state for example that this follows via Craig's theorem from the assumption that the system is effectively axiomatized:
https://en.wikipedia.org/wiki/Craig%27s_theorem
Interestingly, from this theorem it follows that such a system can be re-axiomatized so that "S is a theorem" is even a primitive recursive property. In fact, when Gödel wrote "rekursiv" around 1930, he meant the class of functions that we now call primitive recursive. Because of Craig's theorem, we know that primitive recursive, recursive, and recursively enumerable can be used interchangeably in the definition of effective axiomatization, but without such a theorem, it would be a leap to conclude one from the other.
Also, the Wikipedia article doesn't say that Craig's Theorem proves recursively enumerable axiomatizations equivalent to (primitive) recursive axiomatizations. I would find it very surprising if this was a consequence. It only says that a recursively enumerable set of formulas (e.g. the provable sentences in Peano arithmetic, not merely its axioms) can be given a (primitive) recursive axiomatization. That's a very much weaker claim.
"effectively axiomatized" means that the theorems are recursively enumerable. It does not immediately follow that the axioms are a recursive set. However, by Craig's theorem, we can then re-axiomatize so that the axioms are a recursive set, even a primitive recursive set!
You are of course right about the consequences: In the post above, I meant to say that due to this theorem, it makes no difference whether we require the axioms to be recursively enumerable, recursive, or primitive recursive. But still, without this theorem, it would be a leap to conclude from "the system is effectively axiomatized" that "s is a proof of S" is recursive.
"If T is effectively axiomatized, in the sense that there is an algorithm for deciding whether or not a given sentence is an axiom of T,..."
In Computability: Turing, Gödel, Church and Beyond Martin Davis even makes the definition "T is axiomatizable if it has an axiom set that is computable" on page 42.
And that's also the definition Shoenfield gives on page 125 of Mathematical Logic.
Besides, "effective" has always been a synonym for "computable", "recursive", or "decidable" whenever I've encountered it in this context.
Also, I must insist that "it makes no difference whether we require the axioms to be recursively enumerable, recursive, or primitive recursive." is not what Craig's Theorem says. This is dangerously close to claiming that recursively enumerable sets are recursive which is plainly untrue. If recursively enumerable axioms (not just recursively enumerable theorems) are indeed interchangeable with recursive axioms, then I'd like to hear more about that.
The key point is that I would find it a worthwhile addition to the paper to somehow make clear that "s proves S" is assumed to be decidable. Since you have done this: Thank you!
It's nice to know that you don't need it; it's just a sideshow.
When a formal system says: "this computation halts after some number of steps", then under the default interpretation that means that after say 10000 steps the computation really halts. But in the "similar but weirdly different" reality where transfinite numbers exist the above claim can still be considered true if it runs indefinitely. One simply has to entertain the idea that "some number of steps" might mean a transfinite number of steps.
In other words, yes, we can say that the formal system lies provided we accept that what is and what isn't a lie depends on the viewpoint.
It's a bit odd to think that nearly all "natural" numbers are so large that we can never calculate them, even in principle (because it would take more bits than exist in the universe). Even constructive proofs can describe calculations that could never actually be carried out. The boundary between what I might call "practical" numbers and the larger natural numbers is fuzzy (since it depends on technology), but maybe admitting transfinite numbers exist among the very large naturals would be a way of dealing with it? A way of saying "induction takes us beyond anything we can really know; here be dragons".
And similarly, there are programs that in practice would never halt (because not enough time in the universe), even though theoretically they do.
I don't suppose that's very useful, though, so nice to know it can be avoided.
Throughout the discussion I'm making the tacit assumption that there is one standard viewpoint to which we adhere. That's the "normal" world. Numbers are finite and halting programs halt after finitely many steps. It is from this fixed viewpoint that I'm declaring certain claims to be lies. They are not lies in some grand universal sense.
I realize that the word "lie" usually also entails an accusation of deliberate deception. But that's immaterial here. Formal systems don't have intentions. They simply make claims.
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)
Induction isn't just reasoning about computation, (i.e simple equations). Instead it is reasoning about reasoning about equations (i.e. reasoning about all equations).
Specifically we have: this formula https://wikimedia.org/api/rest_v1/media/math/render/svg/67e2...
For example, Robinson Arithmetic is a finitely axiomatized theory whose axioms contain only one existential quantifier, but just like full (Peano) arithmetic, it is subject to Gödel's incompleteness theorems.
I'm imagining the difference between a system that can show "P(n)" for any n, rather than a system that can show "P(n) for any n."
It seems like the former must come with a proof about the system. The quantifiers "for any n" have to come somewhere. If they aren't embedded within the system, do we still end up with a system that must be able to express "This sentence is not provable?"
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).
1. Encode the propositions of your formal system in ascii (or whatever encoding you like)
2. Observe that the resulting bit patterns can be interpreted as numbers, and so the rules of inference of your formal system can be expressed as mathematical operations on those numbers
3. Profit
Goedel had to invent all of that from scratch. On top of that, he had to describe how to actually carry out step 2 without the benefit of a programming language. All he had to work with was raw math. So his encoding was very different from ascii, or anything you are familiar with, because it was "optimized to run on raw math" rather than a digital computer.