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

Waiting for Gödel (2016)

newyorker.com

Post reply on HN
Print view View original

11–19 of 19 posts

Re: Waiting for Gödel (2016)

#11

Post by [deleted] »

ProfHewitt wrote: post #8
p0llard wrote: post #6

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

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

[deleted]

Re: Waiting for Gödel (2016)

#12

Post by p0llard »

natcombs wrote: post #10
p0llard wrote: post #6

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

> 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

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

Re: Waiting for Gödel (2016)

#13

Post by natcombs »

p0llard wrote: post #12
natcombs wrote: post #10

Earlier quoted context omitted.

> 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

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

Thanks for the response. After reading it I think I may be less clear than in my initial reply now.

Question: Can a sentence be provably true in one arithmetic system but not another?

If so that means there are provably true sentences which exist, but not provably true with the axioms that I have at my disposal right now?

Re: Waiting for Gödel (2016)

#14

Post by p0llard »

natcombs wrote: post #13
p0llard wrote: post #12

Earlier quoted context omitted.

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

Thanks for the response. After reading it I think I may be less clear than in my initial reply now. Question: Can a sentence be provably true in one arithmetic system but not another? If so that means there are provably true sentences which exist, but not provably true with the axioms that I have at my disposal right now?

> Question: Can a sentence be provably true in one arithmetic system but not another?

The answer is yes!

    ZFC |- AC
but

    ZF |/- AC
and both ZFC and ZF can encode arithmetic.

But there's an issue here: no-one really talks about the "truth" of the Axiom of Choice as though it's a concrete thing: it's a very controversial axiom, and although most mathematicians accept it, quite a few don't. Constructivist mathematicians don't accept it, and it's provably equivalent to the law of the excluded middle, so it can't be used in intuitionistic logics.

Now you might counter and say that AC isn't the Gödel sentence for ZFC, and the Gödel sentence for PA is true in the intended model. But that's a different matter from whether it's provable from an axiomatic foundation. The reason I think this matters is because mathematicians work with proofs! Most mathematicians aren't working in foundations, and rely on proofs to the extent that they don't even consider the truth of statements which cannot be proven.

> If so that means there are provably true sentences which exist, but not provably true with the axioms that I have at my disposal right now?

The issue is that provability is completely contingent on the set of axioms you use: provability isn't a universal notion. Of course if you add something which is unprovable (such as the Gödel sentence) to PA, you get a new system which can prove more things: but this system has its own unprovable Gödel sentence.

I'd also question what you mean by "provably true": a sentence is provable from a theory when there exists a derivation in some proof calculus of the sentence starting from the axioms of the theory. "True" is much harder to pin down, and we wouldn't usually say "provably true". "True" can mean "true in the intended model", "true in all models", or even just "provable from a set of axioms".

The Gödel sentence is "true but unprovable" only in the sense that it is true in the intended model: it is not a tautology.

I think most people who have had a brief exposure to mathematics would consider "true in all models" (i.e. tautological truth) to be what is meant by "true", so I don't like it being used to mean "true in the intended model" without qualification.

Re: Waiting for Gödel (2016)

#15

Post by caleb-allen »

ProfHewitt wrote: post #7

[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

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.

Re: Waiting for Gödel (2016)

#16

Post by ProfHewitt »

caleb-allen wrote: post #15
ProfHewitt wrote: post #7

[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

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.

You are very welcome!

Comments and suggestions for the linked article are greatly appreciated!

Re: Waiting for Gödel (2016)

#17

Post by ProfHewitt »

p0llard wrote: post #6

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

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

Re: Waiting for Gödel (2016)

#18

Post by Konohamaru »

p0llard wrote: post #6

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

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.

Re: Waiting for Gödel (2016)

#19

Post by p0llard »

Konohamaru wrote: post #18
p0llard wrote: post #6

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

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.

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

Post reply on HN