[FOM] Some informative questions about intuitionistic logic and mathematics

[Lew Gordeew]

Arnon Avron wrote on Wed, 2 Nov 2005 09:11:43 +0200: 
> 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}?

No. For otherwise we could prove in the intuitionistic logic all classical
axioms with respect to that "negation" @. Consequently, we could prove in
the intuitionistic logic all negation-free classical tautologies. However,
there are known purely implicational, and hence negation-free, classical
tautologies which are not provable intuitionistically - a contradiction.
 
> 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).

See above.

> 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"?

Yes. Because basic recursion theory is easily formalized using
intuitionistic logic. Constructive Analysis is also intuitionistically
formalizable; this requires some care though.
 
> 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?

Decidable (undecidable) relations are meant as in the ordinary recursion
theory (modulo natural translations/interpretations - see above).
 
> 5) Does an intuitionistically-undecidable predicate
> intuitionistically-exist?

Yes, of course (see above).

Regards,
LG

-- 
Telefonieren Sie schon oder sparen Sie noch?
NEU: GMX Phone_Flat http://www.gmx.net/de/go/telefonie