[FOM] Intuitionistic logic on real line

[Pawel Urzyczyn]

Note: I am sending this message to the Foundations of Mathematics 
list and also to the Types list, hoping that it may be interesting 
to the subscribers of both.

    Intuitionistic predicate logic is not complete for real topology.
    ----------------------------------------------------------------

It is well known that a propositional formula is an intutionistic
tautology if and only if it is true in the Heyting algebra of all
open sets of the real line (or plane). See for instance [1] or [2].
Whether the same holds for first-order logic is mentioned in [2] as 
an open question. The answer to this question turns out to be negative,
as can be seen from the following simple example. To my surprise, 
this fact seems to be not known, at least nobody I asked until now
was aware of the incompleteness.

Here is the example. Write (x) and (Ex), respectively, for the universal 
and existential quantifiers. The formula 

 (*)     (x)[P(x)\/ [not P(x)]] -> (Ex)P(x) \/ (x)[not P(x)]

is true on the real line, but it is not an intuitionistic theorem.

Proof:
Denote by ~B the pseudocomplement of an open set B, and by Int(B) its
interior. Let /\ and \/ denote both finite and infinite intersections
and sums. 

Lemma: Let K be an open connected set contained in the union of B and ~B.
       Then K is either contained in B or in ~B.

Proof: Otherwise K splits into two disjoint clopen sets. 

Claim: Int(/\_t(P_t \/ ~P_t)) is contained in \/_t P_t \/ Int(/\_t ~P_t)
       for any open sets P_t contained in |R.

Let a be in LHS. Then there is an open segment K containing a and itself 
contained in /\_t(P_t \/ ~P_t). Thus, for all n the set K is either 
contained in P_t or in ~P_t (Lemma). If it is in at least one P_t then 
a is in \/_t P_t. Otherwise K is contained in Int(/\_t ~P_t).

It remains to see that (*) is not valid intuitionistically. 
As a counterexample take the algebra of all open sets of rationals.
Let z_n be a decreasing sequence of positive irrational numbers 
with limit zero. Interprete P(n) as {x in Q | x > z_n}.

Remark: As another counterexample one can take Markov's Principle

 (**) (x)[P(x)\/ [not P(x)]] -> [not not (Ex)P(x)] -> (Ex)P(x)

which is implied by (*).

References:
[1] Mints, G., A Short Introduction to Intuitionistic Logic, 
           Kluwer, New York, 2000.
[2] Rasiowa, H., Sikorski, R., The Mathematics of Metamathematics, 
           PWN, Warsaw, 1963.
   
======================================================================
Pawel Urzyczyn                                       urzy at mimuw.edu.pl
Institute of Informatics       http://www.mimuw.edu.pl/~urzy/home.html
University of Warsaw                    direct phone: +48-22-55-444-28
Banacha 2,  room #4280                   main office: +48-22-55-444-01
02-097 Warszawa, Poland                          fax: +48-22-55-444-00
======================================================================