We prove that the set of all Polish groups admitting a compatible complete left-invariant metric (called CLI) is coanalytic non-Borel as a subset of a standard Borel space of all Polish groups. As an application of this result, we show that there does not exist a weakly universal CLI group. This, in particular, answers in the negative a question of H.Becker.

Elementary Recursive Nonstandard Analysis, in short ERNA, is a constructive system of nonstandard analysis with a PRA consistency proof, proposed around 1995 by Patrick Suppes and Richard Sommer. Recently, the author showed the consistency of ERNA with several transfer principles and proved results of nonstandard analysis in the resulting theories (see [12] and [13]). Here, we show that Weak König's lemma (WKL) and many of its equivalent formulations over RCA0 from Reverse Mathematics (see [21] and [22]) can be ‘pushed down’ into the weak theory ERNA, while preserving the equivalences, but at the price of replacing equality with equality ‘up to infinitesimals’. It turns out that ERNA plays the role of RCA0 and that transfer for universal formulas corresponds to WKL.

A remarkable result of Henson and Ross [HR] states that if a function whose graph is Souslin in the product of two hyperfinite sets in an ℵ1 saturated nonstandard universe possesses a certain nice property (capacity) then there exists an internal subfunction of the given one possessing the same property. In particular, they prove that every 1-1 Souslin function preserves any internal counting measure, and show that every two internal sets A and B with ∣A∣/∣B∣ ≈ 1 are Borel bijective. As a supplement to the last-mentioned result of Henson and Ross, Keisler, Kunen, Miller and Leth showed [KKML] that two internal sets A and B are bijective by a countably determined bijection if and only if ∣A∣/∣B∣ is finite and not infinitesimal.

In this paper we first show that injective Borel functions map Borel sets into Borel sets, a fact well known in classical descriptive set theory. Then, we extend the result of Henson and Ross concerning the Borel bijectivity of internal sets whose quotient of cardinalities is infinitely closed to 1. We prove that two Borel sets, to which we may assign a counting measure not equal to 0 or ∞, are Borel bijective if and only if they have the same counting measure ≠0, ∞. This, together with the similar characterization for Souslin and measurable countably determined sets, extends the above-mentioned results from [HR] and [KKML].

We characterize omissibility of a type, or a family of types, in a countable theory in terms of non-existence of a certain tree of formulas. We extend results of L. Newelski on omitting < covK non-isolated types. As a consequence we prove that omissibility of a family of < covK types is equivalent to omissibility of each countable subfamily.

The sequent calculus formulation (L-formulation) of the theory of functionality without the rules allowing for conversion of subjects of [3, §14E6] fails because the (cut) elimination theorem (ET) fails. This can be most easily seen by the fact that it is easy to prove in the system

and

but not (as is obvious if α is an atomic type [an F-simple])

The error in the “proof” of ET in [14, §3E6], [3, §14E6], and [7, §9C] occurs in Stage 3, where it is implicitly assumed that if [x]X ≡ [x] Y then X ≡ Y. In the above counterexample, we have [x]x ≡ ∣ ≡ [x](∣x) but x ≢ ∣x. Since the formulation of [2, §9F] is not really satisfactory (for reasons stated in [3, §14E]), a new seguent calculus formulation is needed for the case in which the rules for subject conversions are not present. The main part of this paper is devoted to presenting such a formulation and proving it equivalent to the natural deduction formulation (T-formulation). The paper will conclude in §6 with some remarks on the result that every ob (term) with a type (functional character) has a normal form.

The conventions and definitions of [3], especially of §12D and Chapter 14, will be used throughout the paper.

The theory of valued difference fields (K, σ, υ,) depends on how the valuation υ interacts with the automorphism σ. Two special cases have already been worked out - the isometric case, where υ(σ(x)) = υ(x) for all x Є K, has been worked out by Luc Belair, Angus Macintyre and Thomas Scanlon; and the contractive case, where υ(σ(x)) > nυ(x) for all x Є K× with υ(x) > 0 and n Є ℕ, has been worked out by Salih Azgin. In this paper we deal with a more general version, the multiplicative case, where υ(σ(x)) = ρ · υ(x), where ρ (> 0) is interpreted as an element of a real-closed field. We give an axiomatization and prove a relative quantifier elimination theorem for this theory.

Let σ be any sequence B0, B1 …, Bn, … of transitive sets closed under pairs with for each n. In this paper we show that the smallest admissible set Aσ with σ ∈ Aσ is Σ1 compact. Thus we have an entirely new class of explicitly describable uncountable Σ1 compact sets.

The search for uncountable Σ1 compact languages goes back to Hanf's negative results on compact cardinals [7]. Barwise first showed that all countable admissible sets were Σ1 compact [1] and then went on to give a characterization of the Σ1 compact sets in terms of strict reflection [2]. While his characterization has been of interest in understanding the Σ1 compactness phenomenon it has led to the identification of only one class of uncountable Σ1 compact sets. In particular, Barwise showed [2], using the above notation, that if ⋃nBn is power set admissible it satisfies the strict reflection principle and hence is Σ1 compact. (This result was obtained independently by Karp using algebraic methods [9].)

In proving our compactness theorem we follow Makkai's approach to the Barwise Compactness Theorem [12] and use a modified version of Smullyan's abstract consistency property [14]. A direct generalization of Makkai's method to the cofinality ω case yields a proof of the Barwise-Karp result mentioned above [6]. In order to obtain our new result we depart from the usual definition of language and use instead the indexed languages of Karp [9] in which a conjunction is considered to operate on a function whose range is a set of formulas rather than on a set of formulas itself.

1. The purpose of the present paper is to formulate the problem of non-finitist proofs, and to solve it for certain extensions of the predicate calculus, and for analysis with the exclusion of the theory of sets of points. The corresponding problem for general formal systems is discussed in another publication [1].

To fix ideas we introduce the problem by examples from analysis. The general formulation is given in the text. Also, we shall use in the introduction the concepts decidable, verifiable, finitist without much formal explanation, because the reader is probably familiar with them, and they are defined early on in the text.

The paper presupposes some knowledge of the methods and results in the theory of proofs. These enable one to state the general problem rather more precisely.

In this paper, we analyze structures of Zermelo degrees via a list of four degree theoretic questions (see §2) in various fine structure extender models, or under large cardinal assumptions. In particular we give a detailed analysis of the structures of Zermelo degrees in the Mitchell model for ω many measurable cardinals. It turns out that there is a profound correlation between the complexity of the degree structures at countable cofinality singular cardinals and the large cardinal strength of the relevant cardinals. The analysis applies to general degree notions, Zermelo degree is merely the author’s choice for illustrating the idea.

I0(λ) is the assertion that there is an elementary embedding j : L(Vλ+1) → L(Vλ+1) with critical point < λ. We show that under I0(λ), the structure of Zermelo degrees at λ is very complicated: it has incomparable degrees, is not dense, satisfies Posner–Robinson theorem etc. In addition, we show that I0 together with a mild condition on the critical point of the embedding implies that the degree determinacy for Zermelo degrees at λ is false in L(Vλ+1). The key tool in this paper is a generic absoluteness theorem in the theory of I0, from which we obtain an analogue of Perfect Set Theorem for “projective” subsets of Vλ+1, and the Posner–Robinson follows as a corollary. Perfect Set Theorem and Posner–Robinson provide evidences supporting the analogy between $$AD$$ over L(ℝ) and I0 over L(Vλ+1), while the failure of degree determinacy is one for disanalogy. Furthermore, we conjecture that the failure of degree determinacy for Zermelo degrees at any uncountable cardinal is a theorem of $$ZFC$$.

In the following pages we wish to clarify some questions concerning definitions of relations in terms of other relations. A study is made of how a definition of a relation R1 in terms of another relation R2 works in a given specified universe U. The definition is regarded as a correlation rule between the “possible extensions” of R1 and R2. There are no difficulties in formulating necessary, and in a certain sense also sufficient, formal conditions for the existence of a definition relation between R1 and R2.

In particular, we are concerned with questions such as: “Is every relation of the form s1 definable in terms of some relation of the form s2?” (§ IV) A related question concerns the criterion used by Goodman1 for degrees of complexity, namely, whether for every relation R2 of the form s1 there is some relation R2 of the form s2 such that R1 and R2 are mutually definable (§ V). Some concrete results concerning this condition are stated in the theorems 22–24.

The “complexity function” which is defined (definition 17) and which very naturally suggests itself from the discussion of the definability conditions, seems to furnish an adequate measure of the sort of complexity discussed by Goodman.

Monotone inductive definitions occur frequently throughout mathematical logic. The set of formulas in a given language and the set of consequences of a given axiom system are examples of (monotone) inductively defined sets. The class of Borel subsets of the continuum can be given by a monotone inductive definition. Kleene's inductive definition of recursion in a higher type functional (see [6]) is fundamental to modern recursion theory; we make use of it in §2.

Inductive definitions over the natural numbers have been studied extensively, beginning with Spector [11]. We list some of the results of that study in §1 for comparison with our new results on inductive definitions over the continuum. Note that for our purposes the continuum is identified with the Baire space ωω.

It is possible to obtain simple inductive definitions over the continuum by introducing real parameters into inductive definitions over N—as in the definition of recursion in [5]. This is itself an interesting concept and is discussed further in [4]. These parametric inductive definitions, however, are in general weaker than the unrestricted set of inductive definitions, as is indicated below.

In this paper we outline, for several classes of monotone inductive definitions over the continuum, solutions to the following characterization problems:

(1) What is the class of sets which may be given by such inductive definitions ?

(2) What is the class of ordinals which are the lengths of such inductive definitions ?

These questions are made more precise below. Most of the results of this paper were announced in [2].

In a recent series of papers Kanamori ([4], [5], and [6]) defines generalizations of several combinatorial principles known to follow from the existence of morasses. Kanamori proves the consistency of his generalizations by forcing arguments which come close to satisfying the hypotheses of the Martin's Axiom-type characterizations of morasses developed independently by Shelah and Stanley [9] and the author [12]. A similar “almost application” of morasses appears in [11], in which Todorčević uses forcing to prove the consistency of the existence of Kurepa trees with no Aronszajn or Cantor subtrees. In all cases the attempted proofs using morasses fail for the same reason: the partial orders involved do not have strong enough closure properties.

In an attempt to solve this problem Shelah and Stanley strengthened their characterization of morasses to allow applications to what they called “good canonical limit” partial orders. However, for rather subtle reasons even this strengthened forcing axiom is not good enough for the proposed applications. The problem this time is that Shelah and Stanley's “weak commutativity of Lim and restriction” requirement (see [9, 3.9(iv)]) is not satisfied. Furthermore, there is reason to believe that an ordinary morass is just not good enough for these applications, since in L morasses exist at all regular uncountable cardinals, but even a weak form of Todorčević's conclusion cannot hold at ineffable cardinals (see the end of §4).

A possible solution to this problem is suggested by the fact that □κ is equivalent to a forcing axiom which applies to partial orders satisfying precisely the kind of weak closure conditions involved in the examples described above (see [13]). What is needed to make the proposed morass applications work is something which will do for morass constructions what □κ does for ordinary transfinite recursion constructions. In this paper we show how extra structure can be built into a morass to accomplish this goal.

We associate with any abstract logic L a family F(L) consisting, intuitively, of the limit ultrapowers which are complete extensions in the sense of L.

For every countably generated [ω, ω]-compact logic L, our main applications are:

(i) Elementary classes of L can be characterized in terms of ≡L only.

(ii) If and are countable models of a countable superstable theory without the finite cover property, then .

(iii) There exists the “largest” logic M such that complete extensions in the sense of M and L are the same; moreover M is still [ω, ω]-compact and satisfies an interpolation property stronger than unrelativized ⊿-closure.

(iv) If L = Lωω(Qx), then cf(ωx) > ω and λω < ωx, for all λ < ωx.

We also prove that no proper extension of Lωω generated by monadic quantifiers is compact. This strengthens a theorem of Makowsky and Shelah. We solve a problem of Makowsky concerning Lκλ-compact cardinals. We partially solve a problem of Makowsky and Shelah concerning the union of compact logics.

By the theory TT is meant the higher order predicate logic with the following recursively defined types:

(1) 1 is the type of individuals and [] is the type of the truth values:

(2) [τ1…..τn] is the type of the predicates with arguments of the types τ1…..τn.

The theory ITT described in this paper is an intensional version of TT. The types of ITT are the same as the types of TT, but the membership of the type 1 of individuals in ITT is an extension of the membership in TT. The extension consists of allowing any higher order term, in which only variables of type 1 have a free occurrence, to be a term of type 1. This feature of ITT is motivated by a nominalist interpretation of higher order predication.

In ITT both well-founded and non-well-founded recursive predicates can be defined as abstraction terms from which all the properties of the predicates can be derived without the use of non-logical axioms.

The elementary syntax, semantics, and proof theory for ITT are defined. A semantic consistency proof for ITT is provided and the completeness proof of Takahashi and Prawitz for a version of TT without cut is adapted for ITT: a consequence is the redundancy of cut.

In [KP] we have studied the problem of determining when a subset of a (countable) model M of PA can be coded in an elementary end extension of M. Sets with this property are called elementary extensional. In particular we can ask whether there are elementary extensional subsets of a model which have order type ω. It turns out that having elementary extensional subsets of order type ω is an interesting property connected with other structural properties of models of PA. We will call this property the ω-property. In [KP] the problem of characterizing models with the ω-property was left open. It is still open, and the aim of this paper is to present a collection of results pertaining to it. It should be mentioned that the same notion was studied by Kaufmann and Schmerl in [KS2] in connection with some weak notions of saturation which they discuss there. Our notion of a model with the ω-property corresponds to the notion of an upward monotonically ω-lofty cut.

It is fairly easy to see that countable recursively saturated models (or in fact all recursively saturated models with cofinality ω) and all short recursively saturated models have the ω-property (Proposition 1.2 below). On the other hand, if we had asked the question about the existence of models with the ω-property before 1975 (when recursively saturated models were introduced) the answer would probably not have been that easy and we would have to come to notions close to recursive saturation.

We know from [H1], [H2] that in a stable theory, given a nontrivial locally modular regular type q, one can define a group with generic domination equivalent to q, and that the dependence relation on q can be analyzed in terms of this group. In a stable one-based theory, every regular type is locally modular; hence, this result holds for every nontrivial regular type. We show here that, in fact, in a stable one-based theory, a similar type of construction can be done without the assumption of regularity. More precisely, we show that for any type q, the nontrivial part of q can be analyzed by generics of groups and that any nontrivial relation can be described by affine relations (Theorem A).

This construction is then used to answer a question about homogeneity in pairs of models which is still open in the case of arbitrary stable theories (Theorem C).

We distinguish between two kinds of mathematical assertions: objective and constructive. An objective assertion describes the universe of mathematical objects; a constructive one describes the (idealized) mathematician's ability to find mathematical objects with various properties. The familiar formalizations of classical mathematics are based on formal languages designed for expressing objective assertions only. The constructivist program stresses, on the contrary, the importance of constructive assertions; moreover, intuitionism claims that constructive activities of the mind constitute the very subject matter of mathematics, and thus questions the semantic status of objective assertions.

The purpose of this paper is to show that classical mathematics can be extended to include constructive sentences, so that both objective and constructive properties can be discussed in the framework of the same theory. To achieve this goal, we introduce a new property of mathematical objects, calculability.

The word “calculable” may be applied to objects of various types: natural numbers, integers, rational or real numbers, polynomials with rational or real coefficients, etc. In each case it has a different meaning, so that actually we define not one, but many new properties.

The question, “What do initial segments of the degrees of unsolvability look like?” has interested recursive function theorists for several years. Sacks [4] hypothesized that Sis a finite initial segment of degrees if and only if S is order-isomorphic to a finite initial segment of some upper semilattice with a least element. Lachlan [2] suggested the generalization, S is an initial segment of degrees if S is order-isomorphic to some countable upper semilattice with both least and greatest elements.

In [1] there were given postulates for an abstract “projective algebra” which, in the words of the authors, represented a “modest beginning for a study of logic with quantifiers from a boolean point of view”. In [5], D. Monk observed that the study initiated in [1] was an initial step in the development of algebraic versions of logic from which have evolved the cylindric and polyadic algebras.

Several years prior to the publication of [1], J. C. C. McKinsey [3] presented a set of postulates for the calculus of relations. Following the publication of [1], McKinsey [4] showed that every projective algebra is isomorphic to a subalgebra of a complete atomic projective algebra and thus, in view of the representation given in [1], every projective algebra is isomorphic to a projective algebra of subsets of a direct product, that is, to an algebra of relations.

Of course there has since followed an extensive development of projective algebra resulting in the multidimensional cylindric algebras [2]. However, what appears to have been overlooked is the correspondence between the Everett–Ulam axiomatization and that of McKinsey.

It is the purpose of this paper to demonstrate the above, that is, we show that given a calculus of relations as defined by McKinsey it is possible to introduce projections and a partial product so that this algebra is a projective algebra and conversely, for a certain class of projective algebras it is possible to define a multiplication so that the resulting algebra is McKinsey's calculus of relations.

We introduce the notion of infinitary interpretation of structures. In general, an interpretation between structures induces a continuous homomorphism between their automorphism groups, and furthermore, it induces a functor between the categories of copies of each structure. We show that for the case of infinitary interpretation the reversals are also true: every Baire-measurable homomorphism between the automorphism groups of two countable structures is induced by an infinitary interpretation, and every Baire-measurable functor between the set of copies of two countable structures is induced by an infinitary interpretation. Furthermore, we show that the complexities are maintained in the sense that if the functor is ${\bf{\Delta }}_\alpha ^0$, then the interpretation that induces it is ${\rm{\Delta }}_\alpha ^{in}$ up to ${\bf{\Delta }}_\alpha ^0$ equivalence.