3 ms·
But doesn't Mizar void the argument that we need a new foundation as set theory has not been conducive to mechanized proofs?
by cscurmudgeon 12y ago
But doesn't Mizar void the argument that we need a new foundation as set theory has not been conducive to mechanized proofs?
- tel 12y agoI don't think the argument is that it's impossible to mechanize proofs outside of HoTT---just that it's prettier and perhaps better there.
- cscurmudgeon 12y ago"Prettier" is subjective.
- tel 12y agoAbsolutely. Never claimed otherwise.
- jesuslop 12y agoI think this is right (not an HoTT expert), it voids it. I'd say that what type theory brings in, that didn't come for free in set theory (ZFC or Mizar's Tarski-Grodendiek extension), is the Curry-Howard correspondence that has the slogan "propositions as types, proofs as programs". With that correspondence you can see the same thing as a program (in a typed lambda calculus depending of the type theory of interest), or as a proof in a corresponding logic.