Waiting for Gödel (2016)

https://www.newyorker.com/tech/annals-of-technology/waiting-for-godel

by keiferski • 6 years ago

28 17 6 years ago

newyorker.com

dang• 6 years ago

Discussed at the time: https://news.ycombinator.com/item?id=12008020

ur-whale• 6 years ago

https://archive.is/IAsgM

KineticLensman• 6 years ago

This Gödel's killing me

smitty1e• 6 years ago

Title alludes to Beckett => https://en.m.wikipedia.org/wiki/Waiting_for_Godot

p0llard4• 6 years ago

There are true statements that are unprovable within the system.

I really don't like this, and it verges on being flat-out incorrect: the first incompleteness theorem does not say this at all. It says that there are sentences (and indeed it constructs one, the so-called Gödel Sentence) that cannot be proven or refuted within the system.

For first-order theories it follows from the contraposition of Gödel's completeness theorem that there exist (classical) models of the theory where this sentence holds and models where it doesn't: the existence of models where the sentence does not hold means that this must be a very different meaning of "true" to the one used in common parlance.

In higher-order logics, which do not have a completeness theorem, it makes sense to talk about true statements which are unprovable: there can exist tautologies, sentences which hold in all models of a theory, which cannot be proven from the axioms of a higher-order theory (and you don't need the incompleteness theorem for this); on the other hand, in a first-order theory all tautologies are provable.

Sentences which cannot be proven or refuted within a theory are said to be logically independent of the theory. Famously, the Axiom of Choice is independent of the axioms of Zermelo–Fraenkel set theory: it's up to mathematicians to decide whether they accept the Axiom of Choice. If they do, they can work in ZF+C; if not, they can work in ZF. Neither system is "more true" from a purely logical perspective, so I really don't like describing logically independent sentences as "true but unprovable": it almost certainly doesn't mean what people think it means.

The first incompleteness theorem could perhaps be stated better for a lay audience as:

    No recursive set of axioms can capture our notion of arithmetic it its entirety.

This is a limitation on how we can use axiom systems to represent mathematical objects: even more informally, we might say:

    Truth is subjective in sufficiently complex systems.

ProfHewitt5• 6 years ago

Incompleteness in the sense of inferential undecidability still must be proven for higher-order strongly-typed theories in computer science.

For an example of such as proof see the following:

https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3459566

ProfHewitt5• 6 years ago

Perhaps a higher-order theory of the ordinals is better than ZFC for the mathematical foundations of computer science.

For example, see the following:

https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3457802

natcombs2• 6 years ago

so I really don't like describing logically independent sentences as "true but unprovable":

I don't see a particular problem with it. It can be "true but unprovable" within a given system. I feel like you may be arguing semantics, but the sentence is still clear and accurate to me, while your lay audience definition is less clear and steps further away from the theorems than necessary

p0llard4• 6 years ago

I feel like you may be arguing semantics

Yeah, I am; it really depends on how you define "true". I prefer this to be interpreted as "true in all models" so sentences are "true" when they are tautological consequences of a theory.

Using this definition, all "true" sentences are provable in first-order logic.

The (usual) Gödel sentence is true in the intended model of arithmetic, but I don't really like this property being referred to as "truth" without qualification.

"true but unprovable" within a given system

Not sure about this: I don't think you can really say something is "true in a system" if it isn't provable. You can only assert its truth by saying it's "true in the intended model" without qualification, or by doing some meta-reasoning in a more powerful system outside the original one.

ProfHewitt5• 6 years ago

In powerful mathematical theories for the foundations of Computer Science the sentence G does not exist.

In fact there is no particular proposition that is known to be inferentially undecidable.

See the following:

https://papers.ssrn.com/abstract=3457802

Konohamaru• 6 years ago

The Axiom of Choice is not an example of Gödel's true-but-unprovable statements, because Gödel's statements are true in all models (as you said) but AoC is NOT true in all models. The Continuum Hypothesis isn't an example either for the same reason.

p0llard4• 6 years ago

Gödel's statements are true in all models

This is wrong, and I said the exact opposite of this: there are non-standard models of PA in which G_F is false.

There is a fundamental difference between Gödel sentences and AoC, which is that the Gödel sentence is Pi_1, which means its independence implies its truth in the standard model.

I'm just not really a fan of unqualified "true" meaning "true in the standard model"; I think if you're doing a course purely on the incompleteness theorems for an audience without much exposure to mathematical logic, using "true to refer to "truth in the standard model" is not a good idea and is likely to lead to misconceptions.

Perhaps the fact that you think G_F is true in all models is evidence in favour of my claim?

ProfHewitt5• 6 years ago

[Gödel 1931] is not applicable to the foundations of computer science for the reasons stated here:

https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3603021

caleb-allen• 6 years ago

Thank you for this link. A few months ago I stumbled across your paper, Common sense for concurrency and strong paraconsistency using unstratified inference and reflection and found it entirely remarkable. I look forward to reading the new paper you linked.

ProfHewitt5• 6 years ago

You are very welcome!

Comments and suggestions for the linked article are greatly appreciated!

Waiting for Gödel (2016)

Related Stories