[FOM] Some informative questions about intuitionistic logic and mathematics

[giovanni sambin]

At 9:11 +0200 2-11-2005, Arnon Avron wrote:
>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?


The so-called double-negation interpretation, or Goedel-Gentzen
translation of the 30s, which sends a formula A to a formula A*,
allows one to prove that:
  Gamma|- Delta is provable in classical logic
if and only if
Gamma*|- Delta* is provable in intuitionistic logic,
actually, in minimal logic (Gamma* is of course A1*,...,An*
if Gamma=A1,...An)
(for a proof, see e.g. Troelstra-van Dalen, Constructivism in
mathematics, an introduction, vol. 1, North-Holland 1988, pp. 57-59)

When I explain this to students I say: the intuitionist can
understand what the classicist says, including his proofs,
but not conversely (unless one adds an extra modality).


>(Obviously,a
>negative answer to question 1 entails a negative one to question 2).

I don't understand this.

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

a subset D of N is decidable (in the intuitionistic sense) if
               D(n) v ~D(n) holds for all n.
It is hard to understand the meaning of this classically, since its
double-negation interpretation would be ~(~~D(n) & ~D(n)), which
is logically true.
That is, when the classicist says D(n) v ~D(n), the intuitionist
understands ~(~~D(n) & ~D(n)), which for him is quite different
from D(n) v ~D(n).
For the classicist, it is of course impossible to understand the
difference between D(n) v ~D(n) and ~(~~D(n) & ~D(n)), since they
are logically equivalent (classically).

In conclusion, an intuitionist says that the classicist has no
real disjunction (as well as no real existential quantifier),
but only their negative counterpart.

Giovanni Sambin