FOM: 'Logical parsimony' of intuitionistic mathematics

[wtait@ix.netcom.com]

Torkel Franzen writes

> After all, intuitionistic predicate logic contains any
>number of logical distinctions that correspond to nothing in
>mathematical knowledge or reasoning. 

I'm not convinced of this. The constructive distinction between \exists 
and \neg \forall \neg, though these are equivalent,is important because 
the axiom of choice in the form

(*) \forall x \exists y A(x,y) \implies \exists F \forall x A(x, F(x))

is a consequence of the constructive meaning of the logical constants. 
But I would add that this conception of the logical constants is not 
wedded to the constructive conception of mathematics. 

It is interesting that, if we translate (*) into the \exists -less 
fragment of logic, writing \exists as \neg \forall \neg, it is not 
derivable in that fragment. So there are propositions of the 
conjunction/universal quantifier fragment of logic which are not 
derivable in that fragment but are derivable in logic with \exists. (So 
Gentzen's program to formulate the rules of inference for a particular 
logical constant using no other constants, fails.)