FOM: 'Logical parsimony' of intuitionistic mathematics
wtait at ix.netcom.com
Tue Feb 10 10:56:40 EST 1998
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.)
More information about the FOM