A COMMON AXIOM SET FOR CLASSICAL AND INTUITIONISTIC PLANE GEOMETRY

We describe a first order axiom set which yields the classical first o rder Euclidean geometry of Tarski when used with classical logic, and yields an intuitionistic (or constructive) Euclidean geometry when use d with intuitionistic logic. The first order language has a single six place atomic predicate and no function symbols. The intuitionistic sy stem has a computational interpretation in recursive function theory, that is, a realizability interpretation analogous to those given by Kl eene for intuitionistic arithmetic and analysis. This interpretation s hows the unprovability in the intuitionistic theory of certain ''nonco nstructive'' theorems of the classical geometry. (C) 1998 Elsevier Sci ence B.V. All rights reserved.