Hacker News new | past | comments | ask | show | jobs | submit login

Thank you for the links!

As stated in Tom Leinster's paper that you link to, both ZFC and Lawvere set theory are first-order theories:

"In logical terminology, both axiomatizations [i.e., ZFC and Lawvere set theory] are simply first-order theories."

This means that with both theories, we cannot categorically define important concepts such as the natural numbers, due to the compactness theorem and its consequence, the upward Löwenheim-Skolem theorem that hold in first-order logic:

https://en.wikipedia.org/wiki/Categorical_theory

https://en.wikipedia.org/wiki/L%C3%B6wenheim%E2%80%93Skolem_...

Also, the downward Löwenheim-Skolem theorem leads to Skolem's paradox, because ZFC proves (as we expect from a set theory) Cantor's theorem, and at the same time we know that if ZFC is consistent, then it has a countable model:

https://en.wikipedia.org/wiki/Skolem%27s_paradox

So, even the rather basic notion of countability is relative.

As long as you stay within first-order predicate logic, a theory of sets will run into such issues.

From what I see, such issues are often "resolved" when working with ZFC by stating explicitly that a very specific (i.e., the "intended") model is meant, with the caveat that, from a logical perspective, we do not even know whether the theory is consistent and hence whether such a model in fact exists.

Thus, even though ostensibly working "in" ZFC, a meta-logical statement about the intended models seems often necessary that cannot be formulated in first-order logic because with first-order predicate logic, we cannot control the cardinality of infinite models.

Do other considered set theories offer any improvements over ZFC in these specific respects?




Your remarks bring me close to the border of my limited knowledge of model theory so I must be careful with my response.

I believe the answer to your question:

> Do other considered set theories offer any improvements over ZFC in these specific respects?

is "no", and that you essentially answer this yourself with the following paraphrasing of Löwenheim–Skolem:

> As long as you stay within first-order predicate logic, a theory of sets will run into such issues.

So if we opt Lawvere set theory I think we just do the same thing as if we had opted for ZCF, i.e., just assume we have a model (perhaps provided by some higher order logical system).

However in my opinion, we do have a theory with a much more intuitive set of axioms.


Only speaking about arithmetic rather than full set theory: in (full) second order arithmetic theory all models of the natural number N are isomorphic (in a unique way). The big drawback is that this theory is completely undecidable, so we usually interpret it in first order logic set theory where it becomes incomplete. By Godel, you cannot have an arithmetic theory with decidable proofs and completeness.

In set theory one has to be careful that you can have models which are not transitive models. So Löwenheim-Skolem implies that if you have a model, you have a countable model. But you may not have a transitive countable model. However you do have a transitive version of Löwenheim-Skolem, by Mostowski collapsing lemma: "there exists a transitive model" <=> there exists a countable transitive model".




Registration is open for Startup School 2019. Classes start July 22nd.

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact

Search: