There is not one set theory, there are many. The author doesn't like Zermelo–Fra... | Hacker News

Hacker Newsnew | past | comments | ask | show | jobs | submit

		hackandthink on Sept 1, 2023 \| parent \| context \| favorite \| on: Types versus sets (and what about categories?) (20... There is not one set theory, there are many. The author doesn't like Zermelo–Fraenkel set theory which is fine. And semantics in ZF set theory is for some theories not possible or intuitive. Semantics in category theory sets (Topos) is usually the way to go (1). "Topoi behave much like the category of sets" (2) Lawvere, a renowned category theorist, wrote a book "SETS FOR MATHEMATICS", which describes different kinds of sets (topoi). (1) https://ncatlab.org/nlab/show/relation+between+type+theory+a... (2) https://en.wikipedia.org/wiki/Topos

discarded1023 on Sept 1, 2023 [–]

The author, Larry Paulson, may or may not like ZF but he has a ton of experience in doing formal proofs in it.

https://isabelle.in.tum.de/website-Isabelle2020/dist/library...

hackandthink on Sept 1, 2023 | [–]

Thanks, did not know.

Maybe this is the reason for his dislike. Would like to hear more about Larry Paulson's experience.

(maybe it was no fun at all)

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