Zulip Chat Archive

Stream: maths

Topic: How does Godel manifest in Type theory?


view this post on Zulip Abhimanyu Pallavi Sudhir (Sep 09 2020 at 05:13):

In PA with FOL, Godel's incompleteness theorem manifests in a rather nice way -- the Godel statement, while true in the standard model of , is not true in some non-standard models, because it can just have a non-standard Godel number and be "provable" in these models, because non-standard numbers allow you to have a stupid definition of a "proof".

In SOL, you don't have non-standard models of , so instead you either actually have semantic truths that are syntactically unprovable, or you don't have a computable proof-checker (I have trouble wrapping my head around this too, but it's fine for now I guess).

How does it manifest in Type theory? Are undecidable statements like N = Z an incompleteness of the first sort (there are models in which it is true, and models in which it is false) or of the second sort (it is true/false in all models, but we can't prove it within Lean)?

view this post on Zulip Mario Carneiro (Sep 09 2020 at 06:03):

N = Z is an undecidability of the first sort, but this is a much more boring kind of undecidability result than Godel incompleteness

view this post on Zulip Mario Carneiro (Sep 09 2020 at 06:05):

I think undecidability is always of the first sort (SOL models are kind of a lie)

view this post on Zulip Abhimanyu Pallavi Sudhir (Sep 09 2020 at 06:13):

I think undecidability is always of the first sort

Do you just mean that logics that don't have a completeness theorem are a "lie"?

SOL models are kind of a lie

Can you elaborate?

(I really want to believe this because I cannot understand SOL models at all, lol.)

view this post on Zulip Kevin Buzzard (Sep 09 2020 at 06:14):

We could have defined Z to literally be N (a type alias) and then defined a new zero, one, addition and multiplication on it. Then N=Z would be provable

view this post on Zulip Mario Carneiro (Sep 09 2020 at 06:15):

The definition of a SOL model is hamstrung by the requirement that the second order variables must represent all subsets of the base type. This makes it possible to prove that SOL models are always standard, but there are models that are "as good as" SOL models but where the second order variables range over a smaller subcollection of subsets, for example those defined by a formula, and these can be nonstandard even though you can't tell them apart by a formal theory

view this post on Zulip Mario Carneiro (Sep 09 2020 at 06:16):

In short, SOL models commit you to some kind of "infinite knowing" that seems implausible to me

view this post on Zulip Abhimanyu Pallavi Sudhir (Sep 09 2020 at 06:21):

And those models with missing subsets aren't actually models of SOL?

Or is that question just meaningless noise?

view this post on Zulip Mario Carneiro (Sep 09 2020 at 06:23):

They aren't actually SOL models, because the definition excludes them, but not because they can act as models in every other respect

view this post on Zulip Mario Carneiro (Sep 09 2020 at 06:25):

https://en.wikipedia.org/wiki/Second-order_logic#Semantics mentions the distinction between "standard semantics", where second order variables must range over the full powerset, and "Henkin semantics" where second order variables can be in a subset

view this post on Zulip Mario Carneiro (Sep 09 2020 at 06:25):

You get categorical models in the standard semantics, and a completeness theorem for Henkin semantics


Last updated: May 10 2021 at 07:15 UTC