[FOM] Some informative questions about intuitionistic logic and mathematics

[Todd Wilson]

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

The answer to this question is no.  A definable operation A |-> @A in
the language of propositional intuitionistic logic with the properties
you specify would give, algebraically, a Heyting algebra term operation
@(x) such that, for any Heyting algebra H,

     @(@(x)) = x   and    x /\ @(x) = 0   for all x in H.

If we take H to be the free Heyting algebra on one generator (also known
as the "Rieger-Nishimura Lattice"), and let p be that generator, then
the second equation implies @(p) <= -p, and since -p is an atom in H, we
must have either @(p) = 0 or @(p) = -p.  In the first case, it follows
that @ is the constantly 0 function, which, with @(@(x)) = x,
contradicts the non-triviality of H.  In the second case, it follows
that -(-p) = p, which is again false.

> 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).

As I pointed out in my earlier post to this thread, there are several
translations from classical to intuitionistic logic that perserve
consequence.  However, these translations also act on propositional
variables.  For example, Godel's negative translation is

     N(p) = --p,  for propositional variables p
     N(x /\ y) = N(x) /\ N(y),  for formulas x, y ...
     N(x \/ y) = --(N(x) \/ N(y)) = -(-N(x) /\ -N(y))
     N(x -> y) = N(x) -> N(y)
     N(false) = false

The result is:  Gamma |- x is classically provable iff N(Gamma) |- N(x)
is intuitionistically provable, where N(Gamma) means apply N to all
formulas in Gamma.  In my previous post, I informally suggested that
this translation provides a way for the intuitionist to understand
claims made by the classical mathematician, by more or less replacing
a classical bare statement of truth with an intuitionistic statement 
that the negation is absurd.

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

Algebraically, if C is a subset of a Heyting algebra such that x \/ -x
holds (is equal to the top element) for each x in C, then the 
sub-Heyting algebra generated by C is actually a Boolean algebra, 
obeying such other laws as

     -(x /\ y) = -x \/ -y   and   x -> y = -x \/ y.

Although not hard to prove, it is not a triviality.

Todd Wilson                               A smile is not an individual
Computer Science Department               product; it is a co-product.
California State University, Fresno                 -- Thich Nhat Hanh