Post #1868053

2026-04-25 19:40 UTC

I propose that &quot;universe of discourse&quot; is more interesting and appropriate than &quot;foundations&quot;. Do we want to talk about sets? Do we want to talk about types? Do we want to talk about whatever we have in our minds? I propose that ZFC, MLTT, and also HoTT/UF, are *not* foundations. They are universes of discourse. They are things we want to talk about, rather than &quot;foundations&quot;.

Replies (2)

@rg9119@mathstodon.xyz 2026-04-25 20:24

@MartinEscardo@mathstodon.xyz I quite regularly recommend Penelope Maddy's paper "What do we want a foundation to to: comparing set-theoretic, category-theoretic, and univalent approaches" is the most stimulating piece on the concept of "foundations" I've read to date. I don't agree with all the conclusions, but I agree that "There isn’t a unified concept of ‘foundation’; there are only mathematical jobs reasonably classified as ‘foundational’." I suspect your "universe of discourse" most closely aligns with Maddy's "Generous Arena", though I can imagine ways the alignment is not perfect. https://faculty.sites.uci.edu/pjmaddy/files/2023/09/What-do-we-want-a-foundation-to-do.pdf

Open ##2926165
@ibrahimtencer@mathstodon.xyz 2026-04-25 20:25

@MartinEscardo@mathstodon.xyz we are the foundations

Open ##2926166