How does Godel manifest in Type theory?

Stream: maths

[Abhimanyu Pallavi Sudhir]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Abhimanyu Pallavi Sudhir]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Abhimanyu Pallavi Sudhir]

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

Or is that question just meaningless noise?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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