"I find baring the law of the excluded middle an unnecessarily restrictive basis for logic" I agree that it doesn't seem to make sense in that case. However, t

"I find baring the law of the excluded middle an unnecessarily restrictive basis for logic" I agree that it doesn't seem to make sense in that case. However, there are practical use for constructive proofs, for instance, program extraction. Consider a proposition such that "for all list L, there is a list L' such that L' is sorted and L' is a permutation of L". From a constructive proof of that proposition, you can extract a sorting algorithm. This works basically because the constructive proof has to exhibit a witness. That's the kind of things you can do with the Coq proof assistant. "you may not be able to prove that Anne is married or prove that Anne is unmarried, but can't you prove by that Anne is either married or unmarried, by the definition of marriege?" You can't prove it in constructive logic. You can always add an axiom of the form "for all x, x is married or x is not married". However, if you do that, your proof won't be constructive anymore (unless you provide a decision procedure together with your axiom).