The Coq mailing list

[roconnor AT theorem.ca]

On Mon, 4 Sep 2006, Pierre Casteran wrote:

> Hello,
>
> If you work with the Development version of Coq , you may load the 
> Logic.ClassicalEpsilon module,
> which  asserts classical logic for Prop (by requiring Logic.Classical) and 
> declares an axiom (the one called lift_ex
> in Benjamin's message).

I wonder, wouldn't classical reasoning be better done in Coq by defining 
classical disjunction as ~(~A/\~B) and classical existantial as ~forall 
x,~(A x) rather than adding excluded middle as an axiom?  One could add a 
tactic that reduces a goal from (... |- P) to (... |- ~~P) whenever P does 
not contain constructive disjunctions or constructive existential 
quantifiers (or more generally, whenever P is a Harrop formula).

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''