[FOM] FOM Digest, Vol 37, Issue 24. Lagnese's question

[John Bell]

Giovanni Lagnese asks:

Is there a logic in which "not ((exists x) not P(x))" is 
> equivalent to 
> "(forall x) P(x)", but "not ((forall x) not P(x))" is not 
> equivalent to 
> "(exists x) P(x)"?

If the term "logic" is replaced by "intuitionistic theory", the answer to
Lagnese's question is (if I'm not mistaken) "yes".

Let L be the intuitionistic first-order language with one unary predicate
symbol P. Let T be the theory in L with the single axiom (Ax) (Px or not
Px).
Then, in T, from not (Ex)not Px, one infers   (Ax) not not Px, whence Ax Px
(the reverse implication being automatic). On the other hand the sentence
not (Ax) not Px  -->  (Ex)Px is not derivable in T. This is shown by the
following topological model M of T.

Domain: Set N of natural numbers
Algebra of truth values: Complete Heyting algebra H of open sets in the
one-point compactification N* of the discrete space N.
Interpretation of Pn: {n}

Write [p] for the truth value of a sentence p of L under this
interpretation. Then since each {n} is clopen in N, and hence in N*, it
follows that [(Ax) (Px or not Px)] = N*, the top element of H. So M is a
model of T. 

Also [(Ex)Px] = union of the interpretations of the Pn = N
        [not (Ax) not Px] = interior of the closure of the union of the
interpretations of the Pn = N*

So [not (Ax) not Px] is not contained in [(Ex)Px], and accordingly the
sentence 
not (Ax) not Px  -->  (Ex)Px does not hold in M.

-- John Bell

Professor John L. Bell
Department of Philosophy
University of Western Ontario
London, Ontario
Canada N6A 3K7
 
http://publish.uwo.ca/~jbell