Should Type Theory (HoTT) Replace (ZFC) Set Theory as the Foundation of Math?

#1

Post by westurner » Thu, Feb 27, 2025, 3:43 AM UTC

Should Type Theory (HoTT) Replace (ZFC) Set Theory as the Foundation of Math?
link.springer.com

Re: Should Type Theory (HoTT) Replace (ZFC) Set Theory as the Foundation of Math?

#2

Post by b9r5 » Thu, Feb 27, 2025, 3:56 AM UTC

In a practical sense, hasn't type theory already replaced ZFC in the foundations of math? Lean is what working mathematicians currently use to formally prove theorems, and Lean is based on type theory rather than ZFC.

Re: Should Type Theory (HoTT) Replace (ZFC) Set Theory as the Foundation of Math?

#3

Post by [deleted] » Thu, Feb 27, 2025, 4:55 AM UTC

[deleted]

Re: Should Type Theory (HoTT) Replace (ZFC) Set Theory as the Foundation of Math?

#4

Post by fithisux » Thu, Feb 27, 2025, 5:27 AM UTC

Still, both should be taught.

Re: Should Type Theory (HoTT) Replace (ZFC) Set Theory as the Foundation of Math?

#5

Post by westurner » Thu, Feb 27, 2025, 5:28 PM UTC

b9r5 wrote: post #2

In a practical sense, hasn't type theory already replaced ZFC in the foundations of math? Lean is what working mathematicians currently use to formally prove theorems, and Lean is based on type theory rather than ZFC.

But HoTT is removed from lean core?

From https://news.ycombinator.com/item?id=42440016#42444882 :

> /? Hott in lean4 https://www.google.com/search?q=hott+in+lean4

https://github.com/forked-from-1kasper/ground_zero :

> Lean 4 HoTT Library

Re: Should Type Theory (HoTT) Replace (ZFC) Set Theory as the Foundation of Math?

#6

Post by westurner » Fri, Feb 28, 2025, 4:37 AM UTC

"Should Type Theory Replace Set Theory as the Foundation of Mathematics?" (2023) https://link.springer.com/article/10.1007/s10516-023-09676-0