[FOM] Some informative questions about intuitionistic logic and mathematics

[Wim van Gessel]

Arnon Avron wrote:

>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}?
>  
>
If I am not mistaken the answer must be 'no'.
Intuitionistic propositional logic can be modeled by any
complete Heyting algebra, and in particular by any
finite distributive lattice. The simplest nontrivial case is
the partial ordering {0, p, 1} where 0 is bottom ('false'),
1 is top ('true'), and p lies in between. The usual connectives
are then unambiguously determined.
In this instance it is easy to check that an operation @ as
described in the quote is impossible: the second condition
implies that 0 and 1 must be interchanged, so by the first
condition p must be mapped to itself, which violates the
second condition.

Regards, -- Wim van Gessel