Löwenheim-Skolem

Stream: general

[Kenny Lau]

Is Löwenheim-Skolem true in Lean?

[Kevin Buzzard]

isn't that 2 theorems?

[Kevin Buzzard]

wait this is a theorem about model theory, right? Is model theory in Lean?

[Kevin Buzzard]

Can you formalise your question?

[Kenny Lau]

Is there a countable model of ZFC in Lean?

[Floris van Doorn]

This should be true. It shouldn't matter that the metatheory is type theory instead of set theory to prove Löwenheim-Skolem.
There are students at the university of Pittsburgh who want to formalize forcing in Lean, and want to prove Löwenheim-Skolem along the way: https://github.com/flypitch/flypitch.

[Reid Barton]

oh, this is neat! I wanted to formalize independence of CH too at one point, so I'll definitely check this out

[Kenny Lau]

well there are a lot more sentences in Lean than in classical mathematical logic

[Floris van Doorn]

well there are a lot more sentences in Lean than in classical mathematical logic

Oh, you meant is Lowenheim-Skolem true for Lean as object language.
I thought you were talking about having Lean as meta language, and a regular first-order theory as object language. I have never heard of Lowenheim-Skolem for higher-order logics, but it is probably false for those, right?

[Kevin Buzzard]

Kenny still has not formalised what he means, so we can but conjecture.

[Kenny Lau]

that means we can define r : nat -> nat -> Prop such that the axioms of ZFC (interpreted using Lean) are satisifed with interpreting the membership symbol as r

[Kevin Buzzard]

You want it computable? ;-)

[Kenny Lau]

there's no computable model of ZFC

[Kevin Buzzard]

So you're worried about that the "axiom schemes"?

[Kevin Buzzard]

You should ask Lotte or David Evans. They are actually real life model theorists who are easily accessible to you.

[Kevin Buzzard]

Maybe Mario or Gabriel or one of the other experts that hang around here will just come and tell us the answer though

[Jeremy Avigad]

For higher-order logic with standard semantics, of course, Löwenheim-Skolem is false; we can write down categorical axiomatizations of the reals.
If you think of higher-order logic in a first-order way -- i.e. a model of higher-order logic is just a many-sorted theory (so each type is a sort) with operations for application and lambda abstraction satisfying the requisite comprehension axioms, Löwenheim-Skolem is true. These are sometimes called "Henkin models". I am sure all this will carry over to dependent type theory. The hard part is saying what a model is. But e.g. the usual term model is a countable model.