The undecidability of intuitionistic theories of algebraically closed fields and real closed fields

Let T be a set of axioms for a classical theory TC (e.g. abelian groups, linear order, unary function, algebraically closed fields, etc.). Suppose we regard T as a set of axioms for an intuitionistic theory TH (more precisely, we regard T as axioms in Heyting's predicate calculus HPC).Question. Is TH decidable (or, more generally, if X is any intermediate logic, is TX decidable)? In [1] we gave sufficient conditions for the undecidability of TH. These conditions depend on the formulas of T (different axiomatization of the same TC may give rise to different TH) and on the classical model theoretic properties of TC (the method did not work for model complete theories, e.g. those of the title of the paper). For details see [1]. In [2] we gave some decidability results for some theories: The problem of the decidability of theories TH for a classically model complete TC remained open. An undecidability result in this direction, for dense linear order was obtained by Smorynski [4]. The cases of algebraically closed fields and real closed fields and divisible abelian groups are treated in this paper. Other various decidability results of the intuitionistic theories were obtained by several authors, see [1], [2], [4] for details.One more remark before we start. There are several possible formulations for an intuitionistic theory of, e.g. fields, that correspond to several possible axiomatizations of the classical theory. Other formulations may be given in terms of the apartness relation, such as the one for fields given by Heyting [5]. The formulations that we consider here are of interest as these systems occur in intuitionistic mathematics. We hope that the present methods could be extended to the (more interesting) case of Heyting's systems [5].

Download Full-text

ON THE CLASSIFICATION OF CENTRALLY FINITE ALTERNATIVE DIVISION RINGS SATISFYING ALGEBRAIC CLOSURE CONDITIONS

Journal of Algebra and Its Applications ◽

10.1142/s0219498812500880 ◽

2012 ◽

Vol 11 (05) ◽

pp. 1250088

Author(s):

RICCARDO GHILONI

Keyword(s):

Algebraic Closure ◽

Real Closed Field ◽

Closed Field ◽

Real Closed Fields ◽

Division Rings ◽

Closed Fields ◽

Closure Conditions ◽

The One ◽

Algebraically Closed Fields

In this paper, we prove that the rings of quaternions and of octonions over an arbitrary real closed field are algebraically closed in the sense of Eilenberg and Niven. As a consequence, we infer that some reasonable algebraic closure conditions, including the one of Eilenberg and Niven, are equivalent on the class of centrally finite alternative division rings. Furthermore, we classify centrally finite alternative division rings satisfying such equivalent algebraic closure conditions: up to isomorphism, they are either the algebraically closed fields or the rings of quaternions over real closed fields or the rings of octonions over real closed fields.

Download Full-text

A class of connected theories of order

Journal of Symbolic Logic ◽

10.2307/2275406 ◽

1994 ◽

Vol 59 (2) ◽

pp. 534-542

Author(s):

Alan S. Stern ◽

Stanisław S. Świerczkowski

Keyword(s):

Linear Order ◽

Maximal Element ◽

Disjoint Union ◽

General Notion ◽

Real Closed Fields ◽

Ordered Fields ◽

Closed Fields ◽

Finite Sequences

In 1962 Jan Mycielski proposed a very general notion of interpretability [M1]. This led to the question whether a given theory could be interpreted in the disjoint union of two theories, without being interpretable in any of them. He argued that in such a case it would be presumably simpler to study each of these theories separately, and hence conjectured that this situation can never occur for any of the well-known theories of mathematics. This conjecture has now been verified for the following theories (see [MPS], [P], [S1, 2]): ELO (endless, i.e., without maximal element, linear order), Th(〈ℚ, ≤〉), Th(〈ω, ≤〉) and all sequential theories (those which can code finite sequences of elements of their models). The latter include PA, ZF, GB and Th(〈ω,+,·〉). In view of these confirmations it became ever more plausible that the conjecture is valid also for RCF (real closed fields), i.e., for Th(〈ℝ,≤,+,·,0,1〉). In the present paper we show that Mycielski's conjecture is valid for a class of theories which includes RCF and OF (ordered fields).We consider only theories with equality and without function symbols. Interpretations will be meant local, multidimensional, and with parameters, as defined in [M1], [M2] and surveyed in [MPS] (for a recent definition see also [S2]). We shall write T0 ≪ T1 to say that T0 is interpretable in T1 (or that T1 interprets T0), and this will mean that for every theorem α of T0 there is an interpretation of α in T1.

Download Full-text

A note on valuation definable expansions of fields

Journal of Symbolic Logic ◽

10.2307/2586860 ◽

1998 ◽

Vol 63 (2) ◽

pp. 739-743 ◽

Cited By ~ 1

Author(s):

Deirdre Haskell ◽

Dugald Macpherson

Keyword(s):

Valuation Ring ◽

Quantifier Elimination ◽

Real Closed Field ◽

Closed Field ◽

Real Closed Fields ◽

Ordered Field ◽

Valued Field ◽

Closed Fields ◽

Binary Predicate ◽

Algebraically Closed Fields

In this note, we consider models of the theories of valued algebraically closed fields and convexly valued real closed fields, their reducts to the pure field or ordered field language respectively, and expansions of these by predicates which are definable in the valued field. We show that, in terms of definability, there is no structure properly between the pure (ordered) field and the valued field. Our results are analogous to several other definability results for reducts of algebraically closed and real closed fields; see [9], [10], [11] and [12]. Throughout this paper, definable will mean definable with parameters.Theorem A. Let ℱ = (F, +, ×, V) be a valued, algebraically closed field, where V denotes the valuation ring. Let A be a subset ofFndefinable in ℱv. Then either A is definable in ℱ = (F, +, ×) or V is definable in.Theorem B. Let ℛv = (R, <, +, ×, V) be a convexly valued real closed field, where V denotes the valuation ring. Let Abe a subset ofRndefinable in ℛv. Then either A is definable in ℛ = (R, <, +, ×) or V is definable in.The proofs of Theorems A and B are quite similar. Both ℱv and ℛv admit quantifier elimination if we adjoin a definable binary predicate Div (interpreted by Div(x, y) if and only if v(x) ≤ v(y)). This is proved in [14] (extending [13]) in the algebraically closed case, and in [4] in the real closed case. We show by direct combinatorial arguments that if the valuation is not definable then the expanded structure is strongly minimal or o-minimal respectively. Then we call on known results about strongly minimal and o-minimal fields to show that the expansion is not proper.

Download Full-text

On the elementary theory of pairs of real closed fields. II

Journal of Symbolic Logic ◽

10.2307/2273596 ◽

1982 ◽

Vol 47 (3) ◽

pp. 669-679 ◽

Cited By ~ 3

Author(s):

Walter Baur

Keyword(s):

Power Series ◽

Abelian Groups ◽

Elementary Theory ◽

Predicate Symbol ◽

Axiom System ◽

Closed Field ◽

Algebraic Numbers ◽

Real Closed Fields ◽

Order Language ◽

Closed Fields

Let ℒ be the first order language of field theory with an additional one place predicate symbol. In [B2] it was shown that the elementary theory T of the class of all pairs of real closed fields, i.e., ℒ-structures ‹K, L›, K a real closed field, L a real closed subfield of K, is undecidable.The aim of this paper is to show that the elementary theory Ts of a nontrivial subclass of containing many naturally occurring pairs of real closed fields is decidable (Theorem 3, §5). This result was announced in [B2]. An explicit axiom system for Ts will be given later. At this point let us just mention that any model of Ts, is elementarily equivalent to a pair of power series fields ‹R0((TA)), R1((TB))› where R0 is the field of real numbers, R1 = R0 or the field of real algebraic numbers, and B ⊆ A are ordered divisible abelian groups. Conversely, all these pairs of power series fields are models of Ts.Theorem 3 together with the undecidability result in [B2] answers some of the questions asked in Macintyre [M]. The proof of Theorem 3 uses the model theoretic techniques for valued fields introduced by Ax and Kochen [A-K] and Ershov [E] (see also [C-K]). The two main ingredients are(i) the completeness of the elementary theory of real closed fields with a distinguished dense proper real closed subfield (due to Robinson [R]),(ii) the decidability of the elementary theory of pairs of ordered divisible abelian groups (proved in §§1-4).I would like to thank Angus Macintyre for fruitful discussions concerning the subject. The valuation theoretic method of classifying theories of pairs of real closed fields is taken from [M].

Download Full-text

Decidability of some intuitionistic predicate theories

Journal of Symbolic Logic ◽

10.2307/2272747 ◽

1972 ◽

Vol 37 (3) ◽

pp. 579-587 ◽

Cited By ~ 15

Author(s):

Dov M. Gabbay

Keyword(s):

Reduction Method ◽

Abelian Groups ◽

Sufficient Conditions ◽

Kripke Model ◽

Predicate Calculus ◽

Kripke Models ◽

Classical Counterpart ◽

First Order ◽

Intuitionistic Theory ◽

Classical Predicate

Suppose T is a first order intuitionistic theory (more precisely, a theory of Heyting's predicate calculus, e.g., abelian groups, one unary function, dense linear order, etc.) presented to us by a set of axioms (denoted also by) T.Question. Is T decidable?One knows that if the classical counterpart of T (i.e., take the same axioms but with the classical predicate calculus as the underlying logic) is not decidable, then T cannot be decidable. The problem remains for theories whose classical counterpart is decidable. In [8], sufficient conditions for undecidability were given, and several intuitionistic theories such as abelian groups and unary functions (both with decidable equality) were shown to be undecidable. In this note we show decidability results (see Theorems 1 and 2 below), and compare these results with the undecidability results previously obtained. The method we use is the reduction-method, described fully in [12] and widely applied in [3], which is applied here roughly as follows:Let T be a given theory of Heyting's predicate calculus. We know that Heyting's predicate calculus is complete for the Kripke-model type of semantics. We choose a class M of Kripke models for which T is complete, i.e., all axioms of T are valid in any model of the class and whenever φ is not a theorem of T, φ is false in some model of M.

Download Full-text