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

11–20 of 33 posts

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

#11

Post by rocqua »

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…

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

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

#12

Post by soberhoff »

Author here.

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.

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

#13

Post by soberhoff »

NotAnEconomist wrote: post #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 Ru…

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.

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

#14

Post by triska »

soberhoff wrote: post #12

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

That's a very nice writeup, thank you a lot!

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?

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

#15

Post by soberhoff »

triska wrote: post #14
soberhoff wrote: post #12

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

That's a very nice writeup, thank you a lot! 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 a…

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.

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

#16

Post by lisper »

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?

Nowadays it's pretty simple:

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.

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

#17

Post by triska »

soberhoff wrote: post #15
triska wrote: post #14

Earlier quoted context omitted.

That's a very nice writeup, thank you a lot! 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 a…

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.

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

#18

Post by soberhoff »

triska wrote: post #17
soberhoff wrote: post #15

Earlier quoted context omitted.

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

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.

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

#19

Post by skybrian »

soberhoff wrote: post #12

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

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.

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

#20

Post by soberhoff »

skybrian wrote: post #19
soberhoff wrote: post #12

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

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.

Post reply on HN