3 ms·
The problem is not whether HoTT is easier than ZF. The problem is that ZF is impossible to be used in a proof assistant because it uses classical logic. HoTT us
by 4ad 12y ago
The problem is not whether HoTT is easier than ZF. The problem is that ZF is impossible to be used in a proof assistant because it uses classical logic. HoTT uses intuitionistic logic where all proofs are constructive.
- tel 12y agoNon-constructive proofs aren't problematic for theorem provers---they just have no computable interpretation. You can just assert the Law of Excluded Middle if you like whenever and all of the programs "downstream" will still be checkable. You can even technically provide computable semantics to Pierce's law via call/cc.