3 ms·
>that's thrown at their face is that they have to give up law of excluded middle, non-constructive logic and what not This is just outright false. You can intr
by ImprobableTruth 6y ago
>that's thrown at their face is that they have to give up law of excluded middle, non-constructive logic and what not
This is just outright false. You can introduce it as an Axiom. In Coq this is literally just
Axiom classic : forall P:Prop, P \/ ~ P.
I wouldn't make such patronizing statements without being very sure that I know what I was talking about.
Also, mathematicians aren't the be-all and end-all. Theorem proving is also very relevant for CS, so it's not the end of the world if mathematicians keep using pen and paper for all eternity.
- kmill 6y agoPlus, it's a theorem in Lean: https://github.com/leanprover/lean/blob/master/library/init/classical.lean#L69 https://github.com/leanprover/lean/blob/master/library/init/... (Lean has a somewhat different type theory from Coq, where propositions in Prop have the property that all proofs of a property are defined to be equal. It turns out this along with functional extensionality (that two functions are equal iff their evaluations are all equal) is enough to get LEM, but only in Prop. Outside Prop there's a stronger commitment to constructibility. Still, every definition and lemma has some program backing it.)
- ImprobableTruth 6y agoI wouldn't really say that it has a different type theory, just that it has proof irrelevance and functional extensionality build into the kernel as axioms. But yeah, it's a good way to show that you definitely don't have to give up LEM.