Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Incompleteness ex Machina – proving Gödel's theorems in terms of algorithms [pdf]

scottaaronson.com

Post reply on HN
Print view View original

21–30 of 33 posts

Re: Incompleteness ex Machina – proving Gödel's theorems in terms of algorithms [pdf]

#21

Post by soberhoff »

soberhoff wrote: post #20
skybrian wrote: post #19

Earlier quoted context omitted.

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 d…

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.

Re: Incompleteness ex Machina – proving Gödel's theorems in terms of algorithms [pdf]

#22

Post by salthound »

rocqua wrote: post #11
neokantian wrote: post #6

Earlier quoted context omitted.

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…

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). Specifically we have: this formula https://wikimedia.org/api/rest_v1/media/math/render/svg/67e2...

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.

Re: Incompleteness ex Machina – proving Gödel's theorems in terms of algorithms [pdf]

#23

Post by skybrian »

soberhoff wrote: post #20
skybrian wrote: post #19

Earlier quoted context omitted.

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 d…

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.

Re: Incompleteness ex Machina – proving Gödel's theorems in terms of algorithms [pdf]

#24

Post by imh »

neokantian wrote: post #6
imh wrote: post #2

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…

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?"

Re: Incompleteness ex Machina – proving Gödel's theorems in terms of algorithms [pdf]

#25

Post by rocqua »

salthound wrote: post #22
rocqua wrote: post #11

Earlier quoted context omitted.

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). Specifically we have: this formula https://wikimedia.org/api/rest_v1/media/math/render/svg/67e2...

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.

Wow, I thought it was required to have second order logic for godel to apply, but this seems to be a first order logic that is still undecidable.

Re: Incompleteness ex Machina – proving Gödel's theorems in terms of algorithms [pdf]

#26

Post by ratmice »

rocqua wrote: post #25
salthound wrote: post #22

Earlier quoted context omitted.

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.

Wow, I thought it was required to have second order logic for godel to apply, but this seems to be a first order logic that is still undecidable.

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...

Re: Incompleteness ex Machina – proving Gödel's theorems in terms of algorithms [pdf]

#27

Post by triska »

soberhoff wrote: post #18
triska wrote: post #17

Earlier quoted context omitted.

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,…

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.

Re: Incompleteness ex Machina – proving Gödel's theorems in terms of algorithms [pdf]

#28

Post by soberhoff »

triska wrote: post #27
soberhoff wrote: post #18

Earlier quoted context omitted.

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 m…

Sorry, I was out of town for a while.

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.

Re: Incompleteness ex Machina – proving Gödel's theorems in terms of algorithms [pdf]

#29

Post by triska »

soberhoff wrote: post #28
triska wrote: post #27

Earlier quoted context omitted.

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 m…

Sorry, I was out of town for a while. 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. T…

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:

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.

Re: Incompleteness ex Machina – proving Gödel's theorems in terms of algorithms [pdf]

#30

Post by soberhoff »

triska wrote: post #29
soberhoff wrote: post #28

Earlier quoted context omitted.

Sorry, I was out of town for a while. 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. T…

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 go…

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.

Post reply on HN