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

[triska]

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?

[soberhoff]

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.

[triska]

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.

[soberhoff]

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.

[triska]

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.

[soberhoff]

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.

[skybrian]

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.

[soberhoff]

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.

[skybrian]

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.

[soberhoff]

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.