Ehrenfeucht and Mostowski [3] introduced the notion of indiscernibles and proved that every first order theory has a model with an infinite set of order indiscernibles. Since their work, techniques involving indiscernibles have proved to be extremely useful for constructing models with various specialized properties. In this paper and in a sequel [5], we investigate the effective content of Ehrenfeucht's and Mostowski's result. In this paper we consider the question of which decidable theories have decidable models with infinite recursive sets of indiscernibles. In §1, using some basic facts from stability theory, we show that certain large classes of decidable theories have decidable models with infinite recursive sets of indiscernibles. For example, we show that every ω-stable decidable theory and every stable theory which possesses a certain strong decidability property called ∃Q-decidability have such models. In §2 we construct several examples of decidable theories which have no decidable models with infinite recursive sets of indiscernibles. These examples show that our hypothesis for our positive results in §1 are necessary. Finally in §3 we give two applications of our results. First as an easy application of our results in §1, we show that every ω-stable decidable theory has uncountable models which realize only recursive types. Also our counterexamples in §2 allow us to answer negatively two questions of Baldwin and Kueker [1] concerning the effectiveness of their elimination of Ramsey quantifiers for certain theories.

In [5], we show that in general the problem of finding an infinite set of indiscernibles in a decidable model is recursively equivalent to finding a path through a recursive infinite branching tree. Similarly, we show that the problem of finding an co-type of a set of indiscernibles in a decidable ω-categorical theory is recursively equivalent to finding a path through a highly recursive finitely branching tree.

κ-saturation [SL] is probably the single most useful property of nonstandard models of analysis. For some applications, however, stronger saturation hypotheses seem necessary. Henson formulated his elegant κ-isomorphism property (see [H1], and §2 below) to address this need. This property, though well-suited to certain situations (notably those arising in Banach space theory), is often difficult to apply in practice (see [SL, §7.7]).

In this paper I describe an alternative to κ-isomorphism which is much easier to use; in particular, a proof which assumes that the nonstandard model is fully saturated can usually be converted directly to one using this special model axiom.

Precise definitions of both these axioms appear in §2. In §3 I prove some simple properties of the special model axiom, one of which is that it is at least as strong as κ-isomorphism. In §§4, 5, and 6 the axiom is used to construct a few examples, many of which are pathological, or at the very least counterintuitive. (These examples are given primarily to illustrate use of the axiom; the only one of independent interest is Theorem 5.5.) In §7 some alternative axioms and open problems are discussed.

Many of the results in this paper grew out of discussion and correspondence with C. Ward Henson, to whom I am consequently most grateful.

Gentzen's sequential system LJ of intuitionistic logic has two symbols of implication. One is the logical symbol → and the other is the metalogical symbol ⇒ in sequents

Considering the logical system LJ as a mathematical object, we understand that the logical symbols ∧, ∨, →, ¬, ∀, ∃ are operators on formulas, and ⇒ is a relation. That is, φ ⇒ Ψ is a metalogical sentence which is true or false, on the understanding that our metalogic is a classical logic. In other words, we discuss the logical system LJ in the classical set theory ZFC, in which φ ⇒ Ψ is a sentence.

The aim of this paper is to formulate an intuitionistic set theory together with its metatheory. In Takeuti and Titani [6], we formulated an intuitionistic set theory together with its metatheory based on intuitionistic logic. In this paper we postulate that the metatheory is based on classical logic.

Let Ω be a cHa. Ω can be a truth value set of a model of LJ. Then the logical symbols ∧, ∨, →, ¬, ∀x, ∃x are interpreted as operators on Ω, and the sentence φ ⇒ Ψ is interpreted as 1 (true) or 0 (false). This means that the metalogical symbol ⇒ also can be expressed as a logical operators such that φ ⇒ Ψ is interpreted as 1 or 0.

Gödel's Second Incompleteness Theorem states axiom systems of sufficient strength are unable to verify their own consistency. We will show that axiomatizations for a computer's floating point arithmetic can recognize their cut-free consistency in a stronger respect than is feasible under integer arithmetics. This paper will include both new generalizations of the Second Incompleteness Theorem and techniques for evading it.

There is an analogy between concepts such as end-extension types and minimal types in the model theory of Peano arithmetic and concepts such as P-points and selective ultrafilters in the theory of ultrafilters on N. Using the notion of conservative extensions of models, we prove some theorems clarifying the relation between these pairs of analogous concepts. We also use the analogy to obtain some model-theoretic results with techniques originally used in ultrafilter theory. These results assert that every countable nonstandard model of arithmetic has a bounded minimal extension and that some types in arithmetic are not 2-isolated.

In an earlier article, I proposed a way of determining the relative simplicity of different sets of extralogical primitives. The calculations assumed a fully platonistic logic, committed to an indefinite hierarchy of classes, with sequences and relations defined as classes. Recently it has been shown that a nominalistic logic, countenancing no entities other than individuals, can be made to serve many of the purposes for which a platonistic logic had been thought necessary. The question naturally arises how we are to determine the simplicity of extralogical bases of systems founded upon a nominalistic logic. In such bases, the only extralogical predicates will be predicates (of one or more places) of individuals. The present paper offers a general method of measuring the simplicity of such bases.

Using Steel's recent result that assuming AD, in L[ℝ] below Θ, κ is regular iff κ is measurable, we mimic below Θ certain earlier results of Gitik. In particular, we construct via forcing a model in which all uncountable cardinals below Θ are singular and a model in which the only regular uncountable cardinal below Θ is ℵ1.

For automatic and recursive graphs, we investigate the following problems:

(A) existence of a Hamiltonian path and existence of an infinite path in a tree

(B) existence of an Euler path, bounding the number of ends, and bounding the number of infinite branches in a tree

(C) existence of an infinite clique and an infinite version of set cover

The complexity of these problems is determined for automatic graphs and. supplementing results from the literature, for recursive graphs. Our results show that these problems

(A) are equally complex for automatic and for recursive graphs (-complete).

(B) are moderately less complex for automatic than for recursive graphs (complete for different levels of the arithmetic hierarchy),

(C) are much simpler for automatic than for recursive graphs (decidable and -complete, resp.).

In Oskar Becker's Zur Logik der Modalitäten four systems of modal logic are considered. Two of these are mentioned in Appendix II of Lewis and Langford's Symbolic logic. The first system is based on A1–8 plus the postulate,

From A7: ∼◊p⊰∼p we can prove the converse of C11 by writing ∼◊p for p, and hence derive

The addition of this postulate to A1–8, as Becker points out, allows us to “reduce” all complex modal functions to six, and these six are precisely those which Lewis mentions in his postulates and theorems: p, ∼p, ◊p, ∼◊p, ∼◊∼p, and ◊∼p This reduction is accomplished by showing

where ◊n means that the modal operator ◊ is repeated n times; e.g., ◊3p = ◊◊◊p. Then it is shown that

By means of (1), (2), and (3) any complex modal function whatsoever may be reduced to one of the six “simple” modals mentioned above.

It might be asked whether this reduction could be carried out still further, i.e., whether two of the six “irreducible” modals could not be equated. But such a reduction would have to be based on the fact that ◊p = p which is inconsistent with the set B1–9 of Lewis and Langford's Symbolic logic and independent of the set A1–8. Hence for neither set would such a reduction be possible.

Sets of postulates for at least three different combinatory logics have been given ([2], [3], [4], [5], [6], [7]). The logics and their sets of postulates are quite similar. In all cases it is the proof of the completeness of the set of postulates which causes the difficulty and makes the main papers so long ([3], [7]). It is the purpose of this paper to present a method of writing down sets of postulates for combinatory logics for which the proof of completeness will be fairly simple. We assume acquaintance with certain descriptive portions of [1], namely sections 1–6, 12, 13, 15. Otherwise the present paper is self-contained.

We first solve our problem for the particular logic studied by Rosser ([7]) and then indicate how the method would apply to other logics.

We start with a set, s, of primitive terms. We define s-combination as in [1], p. 43. The precise contents of s need not concern us. It suffices that there be s-combinations I, J, and Q, with no variables in them, and having properties as described below. I and J are to have the same meaning as in [1], p. 43, namely IA is the same as A and JABCD is the same as AB(ADC). QAB is to have the meaning that A and B, considered as functions, are the same.

We show that every splitting of in the local structure of the enumeration degrees, , contains at least one low-cuppable member. We apply this new structural property to show that the classes of all -pairs in , all downwards properly enumeration degrees and all upwards properly enumeration degrees are first order definable in .

By recent work on some conjectures of Pillay, each definably compact group in a saturated o-minimal structure is an extension of a compact Lie group by a torsion free normal divisible subgroup, called its infinitesimal subgroup. We show that the infinitesimal subgroup is cohomologically acyclic. This implies that the functorial correspondence between definably compact groups and Lie groups preserves the cohomology.

A set J of Turing degrees is called an ideal if (1) J ≠ ∅, (2) for any pair of degrees ã, , if ã, ϵ J, then ã ⋃ ϵJ, and (3) for any ⋃ ϵ J and any , if < ⋃, then ϵ J. A set J of degrees is said to be closed if for any theory T with a set of axioms of degree in J, T has a completion of degree in J.

Closed ideals of degrees arise naturally in the following way. If is a recursively saturated structure, let I() = { for some ā ϵ }. Let D() = {: is recursive in d-saturated}. (Recursive in d-saturation is defined like recursive saturation except that the sets of formulas considered are recursive in d.) These two sets of degrees were investigated in [2]. It was shown that if is a recursively saturated model of P, Pr = Th(ω, +), or Pr′ = Th(Z, +, 1), then I() = D(), and this set is a closed ideal. Any closed ideal J can be represented as I() = D() for some recursively saturated model of Pr′. For sets J of power at most ℵ1, Pr′ can be replaced by P.

Assuming CH, all closed ideals have power at most ℵ1, but if CH fails, there are closed ideals of power greater than ℵ1, and it is not known whether these can be represented as I() = D() for a recursively saturated model of P.

In the present paper, it will first be shown that information about representation of closed ideals provides new information about an old problem of MacDowell and Specker [6] and extends an old result of Scott [8] in a natural way. It will also be shown that the representation results from [2] answer a problem of Friedman [1]. This part of the paper is aimed at convincing the reader that representation problems are worth investigating.

We consider any set of Gentzen-type rules in a formal system of the following sort. The terms of the system are propositions, generally to be thought of as the propositions of some underlying theory. The elementary statements are of the form

where and are finite sequences of propositions and (1) expresses a relation, called entailment, between such sequences. These sequences will be called prosequences; they may be void, or consist of a single proposition; and they may contain repetitions of the same proposition. The members of a prosequence will be called its constituents. Two prosequences which are permutations of one another will be regarded as the same. Prosequences will be designated by German letters, single propositions by Latin ones.

The rules of the system are to be of the following form:

This notation is to be understood as indicating p premises and a conclusion, each of the form (1). The constituents of and occur in all premises and conclusion; they are called the parametric constituents, or simply the parameters, of the inference.

Theorem 1. (◊ℵ1,) If B is an infinite Boolean algebra (BA), then there is B1, such that ∣ Aut (B1) ≤∣B1∣ = ℵ1 and 〈B1, Aut (B1)〉 ≡ 〈B, Aut(B)〉.

Theorem 2. (◊ℵ1) There is a countably compact logic stronger than first-order logic even on finite models.

This partially answers a question of H. Friedman. These theorems appear in §§1 and 2.

Theorem 3. (a) (◊ℵ1) If B is an atomic ℵ-saturated infinite BA, Ψ Є Lω1ω and 〈B, Aut (B)〉 ⊨Ψ then there is B1, Such that ∣Aut(B1)∣ ≤ ∣B1∣ =ℵ1, and 〈B1, Aut(B1)〉⊨Ψ. In particular if B is 1-homogeneous so is B1. (b) (a) holds for B = P(ω) even if we assume only CH.

We show that the valuation ring $F_q [[t]]$ in the local field $F_q \left( t \right)$ is existentially definable in the language of rings with no parameters. The method is to use the definition of the henselian topology following the work of Prestel-Ziegler to give an ∃-$F_q $-definable bounded neighbouhood of 0. Then we “tweak” this set by subtracting, taking roots, and applying Hensel’s Lemma in order to find an ∃-$F_q $-definable subset of $F_q [[t]]$ which contains $tF_q [[t]]$. Finally, we use the fact that $F_q $ is defined by the formula $x^q - x = 0$ to extend the definition to the whole of $F_q [[t]]$ and to rid the definition of parameters.

Several extensions of the theorem are obtained, notably an ∃-∅-definition of the valuation ring of a nontrivial valuation with divisible value group.

We study the expressive power of independence-friendly quantifier prefixes composed of universal $\left( {\forall x/X} \right)$, existential $\left( {\exists x/X} \right)$, and majority quantifiers $\left( {Mx/X} \right)$. We provide four quantifier prefixes that can express NP hard properties and show that all quantifier prefixes capable of expressing NP-hard properties embed at least one of these four quantifier prefixes. As for the quantifier prefixes that do not embed any of these four quantifier prefixes, we show that they are equivalent to a first-order quantifier prefix composed of $\forall x$, $\exists x$, and Mx. In unison, our results imply a dichotomy result: every independence-friendly quantifier prefix is either decidable in LOGSPACE or NP hard.

We investigate the partial orderings of the form P(X),⊂〉, where X is a relational structure and P(X) the set of the domains of its isomorphic substructures. A rough classification of countable binary structures corresponding to the forcing-related properties of the posets of their copies is obtained.

We answer a question raised in [9], that is whether the infinite weight of the generic type of the free group is witnessed in Fω. We also prove that the set of primitive elements in finite rank free groups is not uniformly definable. As a corollary, we observe that the generic type over the empty set is not isolated. Finally, we show that uncountable free groups are not ℵ1-homogeneous.

We answer a question of Just, Miller, Scheepers and Szeptycki whether certain diagonalization properties for sequences of open covers are provably closed under taking finite or countable unions.