[FOM] Some informative questions about intuitionistic logic and mathematics

[Arnon Avron]

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