Zulip Chat Archive

Stream: general

Topic: Set-theoretic proofs in type theory

Kristaps Balodis (Jun 24 2023 at 18:42):

Soft/philosophical question, but is there any sort of formal way to compare set theoretic and type theoretic foundations?
For example, suppose I "prove" the cohomology of spheres is what we all know it to be it is in Lean. Technically, I have not really proved the classical theorem though, as its originally defined for topological spaces defined as sets, and what I've proved in Lean is about types. However, the proof is "essentially the same".

I know in HoTT we define "sets" to be of a certain h-level, because they ought to behave "the same", but do we have any formal way of comparing ZFC sets to these? Or more generally, any formal (canonical?) way to turn statements about types into statements about ZFC sets or vice-versa?

Henrik Böving (Jun 24 2023 at 18:46):

As I understand #leantt does kind of go into this direction?

Jason Rute (Jun 27 2023 at 02:04):

Technically a proof in ZFC is a proof for any model of set theory. In Lean you can construct such models. Similarly, a proof in Lean is for any model of Lean. While type theoretic models can be very advanced topos-like models, when you add the axiom of choice they look more like models some sort of set theory. Specifically (I think) Mario’s thesis shows that if you built types the obvious way out of sets in a model of ZFC plus infinitely many large cardinals, then you get a model of Lean.

For example, this shows that you can’t say prove the continuum hypothesis in Lean because we know there is a model of Lean where both the continuum hypothesis holds and one where it doesn’t (by just starting with a model of ZFC plus infinitely many large cardinals where CH does and one where it does not hold).

So there is not really a need to make a big deal of if the math is the same unless you are worried about say the existence of universes—which ZFC can’t prove but Lean can (and ZFC plus large cardinals also can). For all the practical stuff it works out the same.

Scott Morrison (Jun 27 2023 at 02:20):

(And the general point, that it's perhaps dubious to argue that "the classical theorem" should refer to "the theorem interpreted in ZFC" in the first place, if only on the basis that many perfectly honest mathematicians have no idea what ZFC actually says.)

Martin Dvořák (Jun 27 2023 at 06:48):

What is a model of Lean?

I know the word "model" in the sense that every theory in the first-order logic has some pack of models (if the theory is inconsistent, it has 0 models; if the theory is complete, it has 1 model; ...). However, Lean doesn't live inside the first-order logic. What does the word "model" mean then?

Trebor Huang (Jun 27 2023 at 09:38):

Tangential note: I think you meant "categorical" for the 1 model part. Complete simply means every statement is either provable or its negation is.

Martin Dvořák (Jun 27 2023 at 09:40):

[there was a false statement]

Martin Dvořák (Jun 27 2023 at 09:42):

[there was a redundant statement]

Reid Barton (Jun 27 2023 at 09:43):

What's your favorite example of a complete theory?

Martin Dvořák (Jun 27 2023 at 09:44):

For example, the theory of a group extended with the axiom "has exactly two elements" is complete.

Reid Barton (Jun 27 2023 at 09:45):

OK how about an example with an infinite model?

Reid Barton (Jun 27 2023 at 09:46):

(https://en.wikipedia.org/wiki/L%C3%B6wenheim%E2%80%93Skolem_theorem)

Martin Dvořák (Jun 27 2023 at 09:54):

Oh, I was wrong!

Is "complete theory" a syntactic notion but "categorical theory" a semantic notion?

Pedro Sánchez Terraf (Jun 27 2023 at 11:42):

Martin Dvořák said:

Is "complete theory" a syntactic notion but "categorical theory" a semantic notion?

Exactly. Complete talks about proofs, and there are very few categorical first-order theories (having just one model). On the other hand, “categorical in power $\kappa$ ” is much more frequent (cf. Morley's theorem).

Martin Dvořák (Jun 27 2023 at 12:01):

What is the semantic counterpart of a complete theory in FOL? Do I understand it right that a first-order theory is complete iff [this is a meta-theoretic claim] all its models are elementary equivalent, i.e., no sentence in FOL can distinguish between them? A special case is a categorical theory...

Pedro Sánchez Terraf (Jun 27 2023 at 12:25):

Martin Dvořák said:

Do I understand it right that a first-order theory is complete iff [this is a meta-theoretic claim] all its models are elementary equivalent, i.e., no sentence in FOL can distinguish between them?

That's correct, yes.

Martin Dvořák (Jun 27 2023 at 12:26):

Back to the topic: What is a model of Lean?

Floris van Doorn (Jun 27 2023 at 12:35):

Mario's thesis (#leantt?) describes a set-theoretic model of Lean.

Kevin Buzzard (Jun 27 2023 at 13:05):

We need to run mathport on Mario's thesis and then update the linkifier.

Jason Rute (Jun 27 2023 at 13:10):

Models in general refer to semantic interpretations of syntactic proof systems. Even for FOL there are many kinds of models like Boolean valued models or models where equality is an equivalence relation. Models for basic type theories are often categories where types are interpreted as objects in the category and functions are arrows. The model of Lean’s type theory is more or less the category Set in category theory (but with universes and Prop so it is a bit more complicated). As for models with soundness and completeness I think the following holds: toposes are models for intuitionistic higher order logic, Cartesian closed infinity categories are models for Martin Lof type theory with one universe, (infinity, 1)-toposes are models of homotopy type theory with one universe. (I could be misremembering. @Reid Barton would know better.) Since intutionistic type theory is computational, there are also computational models. Basically certain programming languages can be models of Martin Lof type theory.