The Coq mailing list

[Benjamin Werner <benjamin.werner AT inria.fr>]

A more elementary proof is showing that  ~(A/\B)->(~A\/~B)
can be derived from the scheme (A->B)\/(B->A) (for any A and B).

This scheme is well-known to be weaker than EM. For instance,
it is valid in any linear (totally ordered) Heyting Algebra.



However, I am indeed a little worried that more and more coq-club
messages look like students looking for solutions to their homeworks.

Should we have a policy of answering only to people who are either
known or have presented themselves ?


Best,

Benjamin




Le 27 nov. 07 à 17:31, Stefano Berardi a écrit :

> Wan Hai wrote:
>
> > Dear All.
> > I have two questions:
> > 1) Can "~(A/\B)->(~A\/~B)" be proved without using classical logic,
> > such as A\/~A ? This can be easily proved using "forall A:Prop, A\/ 
> > ~A"
> > 2) Does "~(A/\B)->(~A\/~B)" have the same power of "A \/ ~A"? Or say,
> > (forall A B:Prop, ~(A/\B)->(~A\/~B)) -> (forall A:Prop, A\/~A) ?
> > For question 1, I think the answer is no. For question 2, I have
> > worked on it for several hours, but haven't worked it out.
> > Can someone give me a clue?
> > Thanks a lot!
>
> related questions are adressed in a LICS2004 paper "An Arithmetical  
> Hierarchy of the Law of Excluded Middle and Related Principles". The  
> answer is that (forall A B:Prop, ~(A/\B)->(~A\/~B)) is an  
> intermediate principle between intuitionistic and classical logic.
>
> (1) Indeed, (forall A B:Prop, ~(A/\B)->(~A\/~B)) is false in the  
> standard realization model of second order arithmetic, this is why  
> (1) is false.
>
> (2) (forall A B:Prop, ~(A/\B)->(~A\/~B)) is true in the realization  
> model in which a map f can depend on A,B:Prop, but all maps of the  
> model are bounded by some recursive map. In this model, however,
>
> Exists x.A(x,y) v ~Exists x.A(x,y)
>
> is false, because in general there is no bound recursive in y on  
> some x such that A(x,y). Therefore
>
> (forall A B:Prop, ~(A/\B)->(~A\/~B)) -> (forall A:Prop, A\/~A)
>
> is false in this model, hence not provable intuitionistic logic.
>
> Stefano
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>         http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club