We give necessary conditions for a set to be definable by a formula with a universal quantifier and an existential quantifier over algebraic integer rings or algebraic number fields. From these necessary conditions we obtain some undefinability results. For example, N is not definable by such a formula over Z. This extends a previous result of R. M. Robinson.

Let I⊿0 denote the fragment of Peano arithmetic where induction is restricted only to bounded formulas (⊿0-formulas), i.e. formulas where all the quantifiers are bounded. We will examine the behaviour in I⊿0 of Chebyshev's classical result on the distribution of primes. Chebyshev showed that each of the following functions on N is bounded by a polynomial in each of the others:

In his proof he used, as auxiliaries, factorials and binomial coefficients.

When we work in a weak system like I⊿0 we have to deal with two problems:

(i) There is not an immediate meaning for symbols like xy, Πp≤xp, and x!.

(ii) Some basic functions like exponentiation, factorial, and product of primes up to a certain element, are in general only partially definable.

The first problem is equivalent to finding ⊿0-formulas representing the relations z = xy, y = Πp≤xp, and y = x!. While we can easily express that y is the product of all primes less than or equal to x in a ⊿0-way, it requires a subtle argument to define z = xy by a ⊿0-formula. The most natural way of expressing it is via the formalization of the Chinese remainder theorem coding the recursion procedure used in the definition of xy. But this can be expressed only via a Σ1-formula. ⊿0-definitions of exponentiation were given by Paris and Bennett (see [GD] and [B]), and all sensible definitions of this type are equivalent (see Remark 1). Later we will examine properties of such a definition E0(x, y, z). The ⊿00-definition of y = Πp≤xp is much more straightforward, since both the relation of being a prime and the divisibility relation are ⊿0-definable. We will give an explicit definition of it and denote it by Ψ(x, y). In this way, by a ⊿0-induction, we will be able to prove the uniqueness of the elements y and z satisfying Ψ(x, y) and E0(x, y, z), respectively.

Tychonoff's theorem states that a product of compact spaces is compact. In [3], P. Johnstone presents a proof of Tychonoff's theorem in a “localic” framework. The surprise is that the point-free formulation of Tychonoff's theorem is provable without the axiom of choice, whereas in the usual formulation it is equivalent to the axiom of choice (see Kelley [5]).

The proof given in [3], however, is classical and seems to use the replacement axiom of Zermelo-Fraenkel. The aim of this paper is to present what we believe to be a more direct proof, which is intuitionistic and can be proved using as primitive only the notion of inductive definition, as it is for instance presented in Martin-Löf [6]. One main point of the paper is to show that the theory of locales can be developed rather naturally in the framework of inductive definitions. We think that our arguments can be presented in the constructive set theory of Aczel [2].

The paper is organized as follows. In §1 we show the argument in the case of a product of two spaces. This proof has a direct generalisation to the case of a product over a set with a decidable equality.

§1. Product of two spaces. We first recall a possible definition of a point-free space (see Johnstone [3] or Vickers [10]). It is a poset (X, ≤), together with a meet operation ab, written multiplicatively, and, for each a ∈ X, a set Cov(a) of subsets of {x ∈ X ∣ x ≤ a}. We ask that if M ∈ Cov(a) and b ≤ a, then {bs ∈ s ∈ M} ∈ Cov(b). This property of Cov will be called the axiom of covering. The elements of Cov(u) are called basic covers of u ∈ X.

We prove the following surprising property of Heyting's intuitionistic propositional calculus, IpC. Consider the collection of formulas, ϕ, built up from propositional variables (p, q, r, …) and falsity (⊥) using conjunction (∧), disjunction (∨) and implication (→). Write ⊢ϕ to indicate that such a formula is intuitionistically valid. We show that for each variable p and formula ϕ there exists a formula Apϕ (effectively computable from ϕ), containing only variables not equal to p which occur in ϕ, and such that for all formulas ψ not involving p, ⊢ψ → Apϕ if and only if ⊢ψ → ϕ. Consequently quantification over propositional variables can be modelled in IpC, and there is an interpretation of the second order propositional calculus, IpC2, in IpC which restricts to the identity on first order propositions.

An immediate corollary is the strengthening of the usual interpolation theorem for IpC to the statement that there are least and greatest interpolant formulas for any given pair of formulas. The result also has a number of interesting consequences for the algebraic counterpart of IpC, the theory of Heyting algebras. In particular we show that a model of IpC2 can be constructed whose algebra of truth-values is equal to any given Heyting algebra.

We prove that the set of all recursive functions cannot be inferred using first-order queries in the query language containing extra symbols [+ , <]. The proof of this theorem involves a new decidability result about Presburger arithmetic which is of independent interest. Using our machinery, we show that the set of all primitive recursive functions cannot be inferred with a bounded number of mind changes, again using queries in [+, <]. Additionally, we resolve an open question in [7] about passive versus active learning.

The idea of this paper is to approach linear orderings as generalized ordinals and to study how they are made from their initial segments. First we look at how the equality of two linear orderings can be expressed in terms of equality of their initial segments. Then we shall use similar methods to define functions by recursion with respect to the initial segment relation. Our method is based on the use of a game where smaller and smaller initial segments of linear orderings are considered. The length of the game is assumed to exceed that of the descending sequences of elements of the linear orderings considered. By use of such game-theoretical methods we can for example extend the recursive definitions of the operations of sum, product and exponentiation of ordinals in a unique and natural way for arbitrary linear orderings. Extensions coming from direct limits do not satisfy our game-theoretic requirements in general. We also show how our recursive definitions allow very simple constructions for fixed points of functions, giving rise to certain interesting linear orderings.

In this paper we study differential fields of characteristic 0 (with perhaps additional structure) whose theory is superstable. Our main result is that such a differential field has no proper strongly normal extensions in the sense of Kolchin [K1]. This is an approximation to the conjecture that a superstable differential field is differentially closed (although we believe the full conjecture to be false). Our result improves earlier work of Michaux [Mi] who proved that a (plain) differential field with quantifier elimination has no proper Picard-Vessiot extension. Our result is a generalisation of Michaux's, due to the fact that any plain differential field K with quantifier elimination is ω-stable. (Any quantifier free type over K defines a unique type over K in the sense of dc(k), the differential closure of K, and as we mention below the theory of differentially closed fields is ω-stable.) The proof of our main result depends on (i) Kolchin's theory [K3] which states that any strongly normal extension L of an algebraically closed differential field K is generated over K by an element η of some algebraic group G defined over CK, the constants of K, where η satisfies some specific differential equations over K related to invariant differential forms on G (η is “G-primitive” over K), and (ii) the fact that a superstable field has a unique generic type which is semiregular.

In [MP] Marker and Pillay showed that if X ⊂ Cn is constructible but (C, +, X) is not locally modular, then multiplication is definable in the structure (C, +,X). That result extended earlier results of Martin [M] and Rabinovich and Zil'ber [RZ]. Here we will examine additive reducts of R and Qp.

Definition. A subset X of Rn is called semialgebraic if it is definable in the structure (R, +,·). A subset X of Rn is called semilinear if it is definable in the structure (R, +, <,λr)r∈b, where λr is the function x ↦ rx [scalar multiplication by r].

Every semilinear set is a Boolean combination of sets of the form {: p () = 0} and {: q() > 0}, where p() and q() are linear polynomials.

Van den Dries asked the following question: if X is semialgebraic but not semilinear, can we define multiplication in (R, +, <,X)? This was answered negatively by Pillay, Scowcroft and Steinhorn.

Theorem 1.1 [PSS]. Suppose X ⊂ Rnis semialgebraic and X ⊂ Infor some bounded interval I. Then multiplication is not definable in (R, +, <,X,λr)r∈R.

In particular if X = · ∣ [0, l ]2, the graph of multiplication restricted to the unit interval, then X is not semilinear so we have a negative answer to van den Dries' question. Peterzil showed that this is the only restriction.

The global function on finite systems is a new concept defined by Gurevich in [1] and discussed in [2] and [3]. In the last ten years this concept has become more and more useful in computer science and logic. Gurevich also pointed out the importance of global functionals on finite systems. In this paper we will give a brief introduction to the concepts of global functions and global functionals on finite systems.

In studying the natural number system N = 〈N, +,0〉 we often refer to its functions and functionals. There are a lot of books and papers in this area. Kleene in [4] gave a detailed introduction to the recursive functions of N. The functionals of N are normally very difficult to compute because here we need to tell the machine what the input function is, which is not very easy to do. In developing the theory of finite systems the functions and functionals are also very useful. For computing the functionals in finite systems we can take the entire graph of a function as the input, which is not possible in N. We will discuss recursive functions and functionals for finite systems. The definitions of recursive functions are very similar to the case in N, but we will have a very different situation. In N the number of elements is infinite. The number of all possible functions from N to N is the continuum. In a finite system the number of all possible functions is finite. It seems that there is no necessity to define the global functions.

In this paper I give a characterization of the closed fragment of the provability logic of I Δ0 + EXP with a propositional constant for EXP. In three appendices many details on arithmetization are provided.

In [2], Juhasz and Shelah use a forcing argument to show that it is consistent with GCH that there is a 0-dimensional T2 topological space X of cardinality ℵ3 such that every partition of the triples of X into countably many pieces has a nondiscrete (in the topology) homogeneous set. In this paper we will show how to construct such a space using a simplified (ω2, 1)-morass with certain additional structure added to it. The additional structure will be a slight strengthening of a built-in ◊ sequence, analogous to the strengthening of ordinary ◊k to ◊S for a stationary set S ⊆ k.

Suppose 〈〈θα∣ ∝ ≤ ω2〉, 〈∝β∣α < β ≤ ω2〉〉 is a neat simplified (ω2, 1)-morass (see [3]). Let ℒ be a language with countably many symbols of all types, and suppose that for each α < ω2, α is an ℒ-structure with universe θα. The sequence 〈α∣α < ω2 is called a built-in ◊ sequence for the morass if for every ℒ-structure with universe ω3 there is some α < ω2 and some f ∈αω2 such that f(α) ≺ , where f(α) is the ℒ-structure isomorphic to α under the isomorphism f. We can strengthen this slightly by assuming that α is only defined for α ∈ S, for some stationary set S ⊆ ω2. We will then say that is a built-in ◊ sequence on levels in S if for every ℒ-structure with universe ω3 there is some α ∈ S and some f ∈ αω2 such that f(α) ≺ .

We prove that there exists a function f which reduces a given subset P of an internal set X of an ω1 saturated nonstandard universe to the set WF of well-founded trees possessing properties similar to those possessed by the standard part map. We use f to define the Lusin-Sierpiński index of points in X, and prove the basic properties of that index using the classical properties of the Lusin-Sierpiński index. An example of a but not set is given.

In 1947 E. Post [28] and A. A. Markov [18] independently proved the undecidability of the word problem (or the problem of deducibility of relations) for semigroups. In 1968 V. L. Murskil [23] proved the undecidability of the identity problem (or the problem of deducibility of identities) in semigroups.

If we slightly generalize the statement of these results we can state many related results in the literature and state our new results proved here. Let V denote either a (Birkhoff) variety of semigroups or groups or a pseudovariety of finite semigroups. By a very well-known theorem a (Birkhoff) variety is defined by equations or equivalently closed under substructure, surmorphisms and all products; see [7]. It is also well known that V is a pseudovariety of finite semigroups iff V is closed under substructure, surmorphism and finite products, or, equivalently, determined eventually by equations w1 = w1′, w2 = w2′, w3 = w3′,… (where the finite semigroup S eventually satisfies these equations iff there exists an n, depending on S, such that S satisfies Wj = Wj′ for j ≥ n). See [8] and [29]. All semigroups form a variety while all finite semigroups form a pseudovariety.

We now consider a table (see the next page). In it, for example, the box denoting the “word” (identity) problem for the psuedovariety V” means, given a finite set of relations (identities) E and a relation (identity) u = ν, the problem of whether it is decidable that E implies u = ν inside V.

In this paper, we continue the line of investigation undertaken in [HR], with which we assume familiarity. For a comprehensive reference we refer the reader to [P]. The authors would like to thank each other for their light spirit and good humor.

Pillay and Prest [PP, Proposition 7.10] have shown that a module M of U-rank 1 which is not totally transcendental may be decomposed as M = Ml ⊕ Mu, where Ml, ⊨ Th(M) omits the unlimited type and Mu imbeds purely into a model of the unlimited part Tu, of T = Th(M). We devote the first section of this paper to a generalization of this result to the case when T has a regular generic and m-dim(M) = 1. (Note that m-dim(M) = 0 implies M is totally transcendental, in which case a general decomposition theorem was proved by Garavaglia [G].)

In this paper we give an introduction to categorical proof theory, and reinterpret, with improvements, Läuchli's work on abstract realizability restricted to propositional logic (but see [M1] for predicate logic). Partly to make some points of a foundational nature, we have included a substantial amount of background material. As a result, the paper is (we hope) readable with a knowledge of just the rudiments of category theory, the notions of category, functor, natural transformation, and the like. We start with an extended introduction giving the background, and stating what we do with a minimum of technicalities.

In three publications [L1, 2, 3] published in the years 1968, 1969 and 1972, J. Lambek gave a categorical formulation of the notion of formal proof in deductive systems in certain propositional calculi. The theory is also described in the recent book [LS]. See also [Sz].

The basic motivation behind Lambek's theory was to place proof theory in the framework of modern abstract mathematics. The spirit of the latter, at least for the purposes of the present discussion, is to organize mathematical objects into mathematical structures. The specific kind of structure we will be concerned with is category.

In Lambek's theory, one starts with an arbitrary theory in any one of several propositional calculi. One has the (formal) proofs (deductions) in the given theory of entailments A ⇒ B, with A and B arbitrary formulas. One introduces an equivalence relation on proofs under which, in particular, equivalent proofs are proofs of the same entailment; equivalence of proofs is intended to capture the idea of the proofs being only inessentially different. One forms a category whose objects are the formulas of the underlying language of the theory, and whose arrows from A to B, with the latter arbitrary formulas, are the equivalence classes of formal proofs of A ⇒ B.

By means of an Ehrenfeucht-Mostowski construction we obtain an automorphism theorem for a syntactically characterized class of Laa-theories comprising in particular the finitely determinate ones. Examples of Laa-theories with only rigid models show this result to be optimal with respect to a classification in terms of prenex quantifier type: Rigidity is seen to hinge on quantification of type … ∀ … stat … permitting of the parametrization of families of disjoint stationary systems by the elements of the universe.

Let be a countable saturated structure, and assume that D(v) is a strongly minimal formula (without parameter) such that is the algebraic closure of D(). We will prove the two following theorems:

Theorem 1. If G is a subgroup of Aut() of countable index, there exists a finite set A in such that every A-strong automorphism is in G.

Theorem 2. Assume that G is a normal subgroup of Aut() containing an element g such that for all n there exists X ⊆ D() such that Dim(g(X)/X) > n. Then every strong automorphism is in G.