[FOM] Some informative questions about intuitionistic logic and mathematics
Arnon Avron
aa at tau.ac.il
Wed Nov 2 02:11:43 EST 2005
I have several qustions to intuitionists (the first two - also
to nonintuitionists who might know the answers). The first two
were already asked in my posting on comparing the power of logics
(from October 22), but so far I have not got any reply.
1) Is there a definable (in the same way implication is definable
in classical logic in terms of disjunction and negation) unary
connective @ of intuitionistic logic such that for every A, B we have
that A and @@A intuitionistically follow from each other,
and B intuitionistically follows from the set {A, at A}?
2) Can one define in intuitionistic logic counterparts of the
classical connectives so that the resulting translation
preserves the consequence relation of classical logic? (Obviously,a
negative answer to question 1 entails a negative one to question 2).
3) In several postings it was emphasized that LEM applies
in intuitionistic logic to "decidable" relations. Is there
an intuitionist definition of "decidable" according to which
this claim conveys more than a trivial claim of the form "A implies A"?
4) Some postings mentioned also "undecidable" relations (or predicates).
What is the definition of "undecidable" here? is a relation P
intuitionistically undecidable if there is procedure that produces
a proof of absurdity from a procedure that given any x either provides
a proof of P(x) or a procedure that carries any proof of P(x) to
a proof of absurdity?
5) Does an intutionistically-undecidable predicate intutionistically-exist?
Arnon Avron
More information about the FOM
mailing list