It is shown that the modally first-degree formulas of quantificational S5 constitute a reduction class.

Metakides and Nerode in [2] suggested the study of what they termed the lattice of recursively enumerable substructures of a recursively presented model. For example, Metakides and Nerode in [3] introduced the lattice of of recusively enumerable subspaces, , of a recursively presented vector space V∞. The similarities and differences between and ℰ, the lattice of recursively enumerable subsets of the natural numbers N as defined in [9], have been studied by Metakides and Nerode, Kalantari, Remmel, Retzlaff, and Shore. In [6], we studied some similarities and differences between ℰ and the lattice of recursively enumerable sub-algebras of a weakly recursively presented Boolean algebra and this paper continues that study. A weakly recursively presented Boolean algebra (W.R.P.B.A.), , consists of a recursive subset of N, ∣∣, called the field of , and operations (meet), (join), and (complement) which are partial recursive and under which becomes a Boolean algebra. We shall write and for the zero and unit of . If S is a subset of , we let (S)* denote the subalgebra generated by S. Given sub-algebras B and C of , we let B + C denote (B ⋃ C)*. A subalgebra B of is recursively enumerable (recursive) if {x ∈ ∣∣ x ∈ B} is a recursively enumerable (recursive) subset of ∣∣. The set of all recursively enumerable subalgebras of , , forms a lattice under the operations of intersection and sum (+).

This paper compares the strength of two sorts of sentences of PA (classical first-order arithmetic with induction): reflection principles and sentences that may be called iterated consistency assertions.

Let Bew(x) be the standard provability predicate for PA, and for any sentence S of PA, let ⌈S⌉ be the numeral for the Gödel number of S. The reflection principle for S is the sentence Bew(⌈S⌉) → S, and a reflection principle is simply the reflection principle for some sentence. Nothing false (in the standard model for PA) is provable in PA, and therefore every reflection principle is true. Löb's theorem asserts that S is provable (in PA) if the reflection principle for S is provable.

We shall suppose that the 0-ary propositional connectives ⊤ and ⊥ are taken as primitives in the formulation of PA. We define the iterated consistency assertions Conm by: Con0 = ⊤; Conm−1 = − Bew(⌈ − Conm⌉). Con1 may be taken to be the sentence of PA that expresses the consistency of PA; Conn−1, the sentence that expresses the consistency of PA ⋃ {Conn}.

Our starting point is the observation that Con1 is equivalent (in PA) to the reflection principle for ⊥. (The second incompleteness theorem thus follows in a well-known way from Löb's theorem: if PA is consistent, then ⊥ is not provable, the reflection principle for ⊥ is not provable, and the consistency of PA is not provable either.)

The notion of forking has been introduced by Shelah, and a full treatment of it will appear in his book on stability [S1]. The principal aim of this paper is to show that it is an easy and natural notion.

Consider some well-known examples of ℵ0-stable theories: vector spaces over Q, algebraically closed fields, differentially closed fields of characteristic 0; in each of these cases, we have a natural notion of independence: linear, algebraic and differential independence respectively. Forking gives a generalization of these notions. More precisely, if are subsets of some model and c a point of this model, the fact that the type of c over does not fork over means that there are no more relations of dependence between c and than there already existed between c and . In the case of the vector spaces, this means that c is in the space generated by only if it is already in the space generated by . In the case of differentially closed fields, this means that the minimal differential equations of c with coefficient respectively in and have the same order. Of course, these notions of dependence are essential for the study of the above mentioned structures. Forking is no less important for stable theories. A glance at Shelah's book will convince the reader that this is the case.

What we have to do is the following. Assuming T stable and given and p a type on , we want to distinguish among the extensions of p to some of them that we shall call the nonforking extensions of p.

We are interested in studying the length of the shortest proof of a propositional tautology in various proof systems as a function of the length of the tautology. The smallest upper bound known for this function is exponential, no matter what the proof system. A question we would like to answer (but have not been able to) is whether this function has a polynomial bound for some proof system. (This question is motivated below.) Our results here are relative results.

In §§2 and 3 we indicate that all standard Hilbert type systems (or Frege systems, as we call them) and natural deduction systems are equivalent, up to application of a polynomial, as far as minimum proof length goes. In §4 we introduce extended Frege systems, which allow introduction of abbreviations for formulas. Since these abbreviations can be iterated, they eliminate the need for a possible exponential growth in formula length in a proof, as is illustrated by an example (the pigeonhole principle). In fact, Theorem 4.6 (which is a variation of a theorem of Statman) states that with a penalty of at most a linear increase in the number of lines of a proof in an extended Frege system, no line in the proof need be more than a constant times the length of the formula proved.

We are often told, correctly, that modern logic originated with Frege. For Frege clearly depicted polyadic predication, negation, the conditional, and the quantifier as the bases of logic; moreover, he introduced the idea of a formal system, and argued that mathematical demonstrations, to be fully precise, must be carried out within a formal language by means of explicitly formulated syntactic rules.

Consequently Frege has often been read as providing all the central notions that constitute our current understanding of quantification. For example, in his recent book on Frege [1973], Michael Dummett speaks of ”the semantics which [Frege] introduced for formulas of the language of predicate logic.” That is, “An interpretation of such a formula … is obtained by assigning entities of suitable kinds to the primitive nonlogical constants occurring in the formula … [T]his procedure is exactly the same as the modern semantic treatment of predicate logic” (pp. 89–90). Indeed, “Frege would therefore have had within his grasp the concepts necessary to frame the notion of the completeness of a formalization of logic as well as its soundness … but he did not do so” (p. 82).

This common appraisal of Frege's work is, I think, quite misleading. Even given Frege's tremendous achievements, the road to an understanding of quantification theory was an arduous one. Obtaining such understanding and formulating those notions which are now common coin in the discussion of logical systems were the tasks of much of the work in logic during the nineteen-twenties.

We prove there are theories (stable or countable) for which over every A there is a prime model but it is not necessarily unique. We also give a simplified proof of the uniqueness theorem for countable stable theories.

In this paper we indicate how compact languages containing the Magidor-Malitz quantifiers Qκn in different cardinalities can be amalgamated to yield more expressive, compact languages.

The language Lκ<ω, originally introduced by Magidor and Malitz [9], is a natural extension of the language L(Q) introduced by Mostowski and investigated by Fuhrken [6], [7], Keisler [8] and Vaught [13]. Intuitively, Lκ<ω is first-order logic together with quantifiers Qκn (n ∈ ω) binding n free variables which express “there is a set X of cardinality κ such than any n distinct elements of X satisfy …”, or in other words, iff the relation on determined by φ contains an n-cube of cardinality κ. With these languages one can express a variety of combinatorial statements of the type considered by Erdös and his colleagues, as well as concepts in universal algebra which are beyond the scope of first-order logic. The model theory of Lκ<ω has been further developed by Badger [1], Magidor and Malitz [10] and Shelah [12].

We refer to a language as being < κ compact if, given any set of sentences Σ of the language, if Σ is finitely satisfiable and ∣Σ∣ < κ, then Σ has a model. The phrase countably compact is used in place of <ℵ1 compact.

This paper proposes a generalization of several reducibilities in the sense of recursive function theory. For this purpose two structures are introduced as models of combinatory logic and reducibilities are defined in a rather natural way by means of the application operation in each model. The first model we consider is called the graph model and was introduced by Dana Scott in [11]. Reducibilities in this model are generalizations of enumeration and Turing reducibilities. The second model is called the hypergraph model and induces reducibilities which are generalizations of hyperenumeration and hyperarithmetical reducibilities.

The possibility of formulating reducibilities in this way is not new. For the graph model it is implicit in [7] and for the hypergraph model in [9]. On the other hand it is possible to look at the present method as a variant of the well-known technique of relativization in recursive function theory. We think that this does not exhaust the power of the method, which is conceptually elegant and provides a natural frame for the results of this paper.

In the first part of the paper we discuss the definition and general properties of the models. Then we introduce the reducibilities in the graph model and prove several theorems which are generalizations of properties already Known for enmeration and Turing reducibilities. Next we define reducibilities in the hypergraph model and try to extend the preceding results. For this purpose we prove two theorems showing significant relations between the operators in both models. In fact we prove that each operator in the hypergraph model can be simulated on a comeager set by an operator of the graph model.

We give here a direct purely combinatorial proof that weak compactness is equivalent to a combinatorial property (2). This property (2) is apparently stronger, and from it, all other usual equivalent definitions and usual properties of weakly compact cardinals can be deduced. So this proof may be useful for books which want to present weakly compact cardinals, but not logic.

A direct simple proof of a weaker implication (e.g., weakly compact μ is not the first inaccessible, and every stationary set has an initial segment which is stationary) was given by Kunen [K] and independently by the author [Sh]. Baumgartner [B] had another proof.

We were motivated by the manuscript of Erdös, Hajnal, Mate and Rado's book on partition calculus, and by conversations with A. Levi who was writing a book on naive set theory.

Notation. Let i, j, α, β, γ, η, σ be ordinals, μ be a cardinal, f, g be functions.

Let cf α be the cofinality of α.

A partially ordered set T is a tree if for any a ∈ T, {b: b < a, b ∈ T} is well ordered; its order type (an ordinal) is called the level of a, and Tα is the set of a ∈ T of level a.

With PC understood to be the propositional calculus of [3], call a binary function Pr from the wffs of PC to the reals a Carnap (probability) function if it meets requirements A1—A5 in Table I (with ‘⊢…’ short in A3—A4 for ‘… is a tautology’), and call the function a Popper (probability) function if it meets requirements Bl—B6 there:

Leblanc established in [3] that every Carnap function is a Popper one, and he tendered proof of the converse. As reported by Stalnaker in [5], the proof unfortunately was incomplete, a mishap due to Leblanc's abbreviating ‘Pr(A, ∼ A) = 1’ as ‘⊢ A’ when Pr is a Popper function. Borrowing from [4], Leblanc did show, as Harper notes in [2, footnote 17], that

(1) If Pr is a Popper function and A is a tautology, then Pr(A, ∼ A) = 1. He did not, however, show that

(2) If Pr is a Popper function and Pr(A, ∼ A) = 1, then A is a tautology.

Nor could he have done so: (2) is false, as the simplest of counterexamples shows. Denied (2), Leblanc had no hope of proving that every Popper function is a Carnap one: of a Popper function Pr it is easily ascertained that Pr meets requirement A4 if and only if Pr(A, ∼ A) = 1 just in case A is a tautology.

Various equivalents and weakenings of the combinatorial principle ◊ are considered. The paper contains both absolute results and consistency results. Also included is a new characterisation of the notion of a stationary subset of ω1.

It is well known that the first strongly inaccessible cardinal is strictly less than the first weakly compact cardinal which in turn is strictly less than the first Ramsey cardinal, etc. However, once one passes the first measurable cardinal the inequalities are no longer strict. Magidor [3] has shown that the first strongly compact cardinal may be equal to the first measurable cardinal or equal to the first super-compact cardinal (the first supercompact cardinal is strictly larger than the first measurable cardinal). In this note we will indicate how Magidor's methods can be used to show that it is undecidable whether one cardinal (the first strongly compact) is greater than or less than another large cardinal (the first huge cardinal). We assume that the reader is familiar with the ultrapower construction of Scott, as presented in Drake [1] or Kanamori, Reinhardt and Solovay [2].

Definition. A cardinal κ is huge (or 1-huge) if there is an elementary embedding j of the universe V into a transitive class M such that M contains the ordinals, is closed under j(κ) sequences, j(κ) > κ and j ↾ Rκ = id. Let κ denote the first huge cardinal, and let λ = j(κ).

One can see from easy reflection arguments that κ and λ are inaccessible in V and, in fact, that κ is measurable in V.

Let A be a standard transitive admissible set. Σ1-separation is the principle that whenever X and Y are disjoint Σ1A subsets of A then there is a ⊿1A subset S of A such that X ⊆ S and Y ∩ S = ∅.

Theorem. If satisfies Σ-separation, then

(1) If 〈Tn∣n < ω) ϵ A is a sequence of trees on ω each of which has at most finitely many infinite paths in A then the function n ↦ (set of infinite paths in A through Tn) is in A.

(2) If A is not closed under hyperjump and α = OnA then A has in it a nonstandard model of V = L whose ordinal standard part is α.

Theorem. Let α be any countable admissible ordinal greater than ω. Then there is a model of Σ1-separation whose height is α.

Spector [21] proved that a relation R on ω is Π11 if and only if it is (positive elementary) inductive on the structure 〈ω, +, ·〉; Kleene [8] showed that R is Π11 if and only if it is semirecursive in the type 2 object E. These two “constructive” characterizations of the Π11 relations have led to the independent study of (positive elementary) induction and recursion in E on an arbitrary structure, as natural generalizations of the theory of Π11 relations on (ω, +, · 〉.

The theory of (positive elementary) induction on an arbitrary structure was developed by Moschovakis in his book Elementary induction on abstract structures (EIAS); one of the most important theorems there is a generalization of the classical theorem of Spector [20] and Gandy [3] about the Π11 relations on ω: a relation R is inductive on an acceptable structure . if and only if there is a formula φ(Y, x) of the language of such that:

where HYP is the collection of hyperelementary relations on .

Moschovakis [17] and Kechris and Moschovakis [6] showed how to develop the theory of recursion in higher types as a chapter in the general theory of inductive definability. This approach to recursion in higher types makes it possible to use methods from the theory of inductive definability in studying recursion in E.

In this paper we establish some results about recursion in E on a structure which bolster the naturalness of this theory and contribute to its comparison with (positive elementary) induction.

A structure is recursive if the set of quantifier-free sentences in the complete diagram ⊿() of is recursive. It has been known for some time that every decidable theory has a recursive model. In fact, every decidable theory has a decidable model (that is a model such that ⊿() is recursive). In this paper we find other conditions which imply that a theory have a recursive model.

In §1 we study the relation between an ℵ0-categorical theory T having a recursive model and the complexity of the quantificational hierarchy of that theory. We let ∃0 denote the set of quantifier-free sentences, and let ∃n÷1 denote the set of sentences beginning with an existential quantifier and having n alternations of quantifiers. (∀n is defined analogously.) Then we show that if T is an arithmetical ℵ0-categorical theory such that T ⋂ ∃n÷2 is Σn÷10 for each n < ω, then T has a recursive model. We show that this is a best possible result by giving an example of a ⊿n÷20 ℵ0-categorical theory T such that T ⋂ ∃n÷1 is recursive yet T has no recursive model.

In §2 we consider the theory of trees. Ershov [1] had proved that every Σ10 theory of trees has a recursive model. We show this to be best possible by giving an example of a ⊿20 theory of trees which has no recursive model.

Large cardinal properties divide rather strikingly into two groups. “Small” large cardinal properties such as weak compactness always relativize to L, while in contrast “large” large cardinal properties such as Ramsey are incompatible with L. These properties seem to be similar otherwise and this sense of similarity is reinforced by the fact that many of the large cardinals do exist in the L-like model L(μ). This paper will show that the division is caused by an artificially restrictive class of “constructible” sets rather than an essential difference in the properties themselves. Specifically, we consider the class K of sets constructible from mice as defined by Dodd and Jensen [3] and prove

Theorem 1. If ρ is Ramsey then ρ is Ramsey in K.

A modification of the proof will show

Theorem 2. If ρ is Jonson, then ρ is Ramsey in K.

Since Ramsey implies Jonson this shows that the notions are equiconsistent. Theorem 2 was proved by Kunen [5] under the assumption that V = L(μ).

The proof of Theorems 1 and 2 depends heavily on results of Dodd and Jensen [3] about K and mice. These results are stated without proof in §2. §2 also contains elementary (to a reader familiar with the theory of iterated ultrapowers) proofs of special cases of some of these lemmas sufficient to give a self contained proof of the following corollary of Theorem 1:

Corollary. If ρ ≤ κ,ρ is Ramsey and L(μ) ⊨ μ is a measure on κ then L(μ) ⊨ ρ is Ramsey.

This paper is mainly concerned with describing complete theories of modules by decomposing them (up to elementary equivalence) into direct products of simpler modules. In §1, I give a decomposition theorem which works for arbitrary direct product theories T. Given such a T, I define T-indecomposable structures and show that every model of T is elementarily equivalent to a direct product of T-indecomposable models of T. In §2, I show that if R is a commutative ring then every R-module is elementarily equivalent to ΠMM where M ranges over the maximal ideals of R and M is the localization of at M. This is applied to prove that if R is a commutative von Neumann regular ring and TR is the theory of R-modules then the TR-indecomposables are precisely the cyclic modules of the form R/M where M is a maximal ideal. In §3, I use the decomposition established in §2 to characterize the ω1-categorical and ω-stable modules over a countable commutative von Neumann regular ring and the superstable modules over a commutative von Neumann regular ring of arbitrary cardinality. In the process, I also prove several general characterizations of ω-stable and superstable modules; e.g., if R is any countable ring, then an R-moduIe is ω-stable if and only if every R-module elementarily equivalent to it is equationally compact.

In [6], Metakides and Nerode introduced the study of the lattice of recursively enumerable substructures of a recursively presented model as a means to understand the recursive content of certain algebraic constructions. For example, the lattice of recursively enumerable subspaces, , of a recursively presented vector space V∞ has been studied by Kalantari, Metakides and Nerode, Retzlaff, Remmel and Shore. Similar studies have been done by Remmel [12], [13] for Boolean algebras and by Metakides and Nerode [9] for algebraically closed fields. In all of these models, the algebraic closure of a set is nontrivial. (The formal definition of the algebraic closure of a set S, denoted cl(S), is given in §1, however in vector spaces, cl(S) is just the subspace generated by S, in Boolean algebras, cl(S) is just the subalgebra generated by S, and in algebraically closed fields, cl(S) is just the algebraically closed subfield generated by S.)

In this paper, we give a general model theoretic setting (whose precise definition will be given in §1) in which we are able to give constructions which generalize many of the constructions of classical recursion theory. One of the main features of the models which we study is that the algebraic closure of set is just itself, i.e., cl(S) = S. Examples of such models include the natural numbers under equality 〈N, = 〉, the rational numbers under the usual ordering 〈Q, ≤〉, and a large class of n-dimensional partial orderings.

‘In Time rigorous abstraction, in Time the highest, in Time divine knowledge, is comprehended’

Atharva Veda

Following McTaggart [17], we may distinguish two aspects of time: The A-series, running through the past to the present and on into the future, and the B-series, running from earlier to later. In Indo-European languages at least, verbs are tensed, so we cannot help but place whatever we speak of in one of the three divisions of the A-series. But these divisions are not permanent: what is present was future and will be past. Hence a typical statement, e.g. ‘Socrates is sitting’, may well be true at one time and false at another. The instability of truth-value over time was a commonplace among pre-Renaissance logicians, but most modern writers have ‘abstracted from’, i.e. ignored, this feature of ordinary language.

Early logicians were quite interested in time: Aristotle questioned the applicability of the excluded middle to predictions of future contingencies in the famous ‘sea-fight’ passage of On interpretation. Later Greek logicians debated whether that which neither is nor will be can legitimately be called possible, and whether, in order for the conditional ‘if p, then q’ to be true, it is required that ‘not both p and not ∼q’ be true (not just now but) always. Mediaeval logicians in Western Europe struggled with logical difficulties created by the Dogmas of the Church, Omniscience and Free Will. Their counterparts in the Islamic world puzzled over the semantics of the temporal adverbs, ‘always’, ‘usually’, ‘often’, ‘sometimes’, ‘seldom’, ‘never’.