3 ms·
Sure, but isn't it the case that either your predicates are computable, in which case both a "classical" and a "constructive" proof assistant could evaluate the
by creata 5y ago
Sure, but isn't it the case that either your predicates are computable, in which case both a "classical" and a "constructive" proof assistant could evaluate them, or they're not, in which case neither could evaluate them?
- logicchains 5y agoYep, but one could express a computable predicate classically (e.g. by unnecessarily invoking the axiom of choice in its definition). Using a constructive proof assistant prevents accidentally doing this, and encourages using constructive definitions where possible. It also encourages using computable mathematical formulations (e.g. computable reals vs classical reals).