The Coq mailing list

[Stefano Berardi <stefano AT di.unito.it>]

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