To what extent can mathematical thought be analyzed in formal terms? Gödel's theorems show the inadequacy of single formal systems for this purpose, except in relatively restricted parts of mathematics. However at the same time they point to the possibility of systematically generating larger and larger systems whose acceptability is implicit in acceptance of the starting theory. The engines for that purpose are what have come to be called reflection principles. These may be iterated into the constructive transfinite, leading to what are called recursive progressions of theories. A number of informative technical results have been obtained about such progressions (cf. Feferman [1962], [1964], [1968] and Kreisel [1958], [1970]). However, for some years I had hoped to give a more realistic and perspicuous finite generation procedure. This was first done in a rather special way in Feferman [1979] for the characterization of predicativity, which may be regarded as that part of mathematical thought implicit in our acceptance of elementary number theory. What is presented here is a new and simple notion of the reflective closure of a schematic theory which can be applied quite generally.

Two examples of schematic theories in the sense used here are versions of Peano arithmetic and Zermelo set theory.

The purpose of this paper is to give structural results on graphs lying in the product of two hyperfinite sets X and Y, whose Y-sections are either all internal sets or all of “small” cardinality with respect to the saturation assumption imposed on our nonstandard universe. These results generalize those of [KKML] and [HeRo]. In [KKML] Keisler, Kunen, Miller and Leth proved, among other results, that any countably determined function in the product of two internal sets X and Y can be covered by countably many internal functions provided that the nonstandard universe is at least ℵ-saturated. This shows that any countably determined function can be represented as a union of countably many restrictions of internal functions to countably determined sets. On the other hand, Henson and Ross use in [HeRo] Choquet's capacitability theorem to prove that any Souslin function in the product of two internal sets X and Y is a.e. equal to an internal function. (Here “a.e.” refers to an arbitrary but fixed bounded Loeb measure.) Therefore, in our terminology, every Souslin function possesses an internal a.e. lifting.

After the introductory §0, where all the necessary terminology is introduced, we continue by presenting the structural result for graphs all of whose Y-sections are of cardinality ≤κ (provided that the nonstandard universe is ≤κ+-saturated) in §1. We show that, under the above saturation assumption, a κ-determined graph with all of the Y-sections of cardinality ≤κ is covered by κ-many internal functions. Therefore, any such graph is a union of κ-many κ-determined functions. In particular if the graph in question is Borel, Souslin, κ-Borel or κ-Souslin (or a member of one of the Borel, κ-Borel or projective hierarchies) then the corresponding constituting functions are of the same “complexity”. Thus, any Borel graph all of whose Y-sections are at most countable is a union of countably many Borel functions and, consequently, has Borel domain. In the setting of Polish topological spaces this was proved by Novikov (see [De]).

We assume that the reader is familiar with the program of “reverse mathematics” and the development of countable algebra in subsystems of second order arithmetic. The subsystems we are using in this paper are RCA0, WKL0 and ACA0. (The reader who wants to learn about them should study [1].) In [1] it was shown that the statement “Every countable commutative ring has a prime ideal” is equivalent to Weak Konig's Lemma over RCA0, while the statement “Every countable commutative ring has a maximal ideal” is equivalent to Arithmetic Comprehension over RCA0. Our main result in this paper is that the statement “Every countable commutative ring has a minimal prime ideal” is equivalent to Arithmetic Comprehension over RCA0. Minimal prime ideals play an important role in the study of countable commutative rings; see [2, pp. 1–7].

In this paper we study notions of a “meager subset” of a hyper-finite set. We work within an ω-saturated nonstandard universe and fix a hyperfinite natural number Є *N∖N. We shall consider subsets of the set = {1, 2, …,H}.

By analogy with the meager subsets of the real interval [0, 1], a notion of meager subset of should have the following properties.

1. Finite sets, countable unions of meager sets, subsets of meager sets, and translates of meager sets should be meager.

2. The Baire Category Theorem should hold; that is, should not be meager.

3. The internal analogue of the Cantor set should be meager.

4. The notion of a meager set should be with respect to a natural topology on .

5. There should exist meager subsets of of Loeb measure one.

6. Sierpiński and Lusin sets should have hyperfinite counterparts with properties similar to the classical case.

Property 5 is desirable so that, as with Lebesgue measure and Baire category on [0, 1], the topological and measure-theoretic notions of “large” and “small” sets are incomparable.

Property 6, while not as necessary as the other five, is desirable because of the strong interplay between measure and category in the classical results about Lusin and Sierpinski sets. Our objective is to find notions of meager set which have a relationship to Loeb measure similar to the classical relationship between meager sets and Lebesgue measure.

We investigate the cofinality of the partial order κ of functions from a regular cardinal κ into the ideal of Lebesgue measure zero subsets of R. We show that when add () = κ and the covering lemma holds with respect to an inner model of GCH, then cf (κ) = max{cf(κκ), cf([cf()]κ)}. We also give an example to show that the covering assumption cannot be removed.

The core model K was introduced by R. B. Jensen and A. J. Dodd [DoJ]. K is the union of Gödel's constructible universe L together with all mice, i.e., , and K is a transitive model of ZFC + (V = K) + GCH (see [DoJ]). V = K is consistent with the existence of Ramsey cardinals [M], and if cf(α) > ω, V = K is consistent with the existence of α-Erdös cardinals [J]. Let K be Ramsey. Then there is a smallest inner model Wκ of ZFC in which κ is Ramsey. We have Wκ ⊨ V = K and Wκ ⊆ K [M]. The existence of Wκ with is equivalent to the existence of a sharplike mouse on N ⊨ K with N ⊨ κ Ramsey. (A mouse N on is called sharplike provided .) We have , where is the mouse iteration of N. N is the oleast mouse not in Wκ (see [J] and [DJKo]). Here < denotes the mouse order. The context always clarifies whether the mouse order or the usual <-relation is meant.

The main result of §1 is that Wκ ⊨ κ is the only Ramsey cardinal. A similar result has been found true in the smallest inner model L[U] of ZFC + “κ is measurable” if U is a normal measure on κ: L[U] ⊨ κ is the only measurable cardinal [Ku].

Basic results on the model theory of substructures of a fixed model are presented. The main point is to avoid the use of the compactness theorem, so this work can easily be applied to the model theory of Lω1,ω and its relatives. Among other things we prove the following theorem:

Let M be a model, and let λ be a cardinal satisfying λ∣L(M)∣ = λ. If M does not have the ω-order property, then for every A ⊆ M, ∣A∣ ≤ λ, and every I ⊆ M of cardinality λ+ there exists J ⊆ I cardinality λ+ which is an indiscernible set over A.

This is an improvement of a result of S. Shelah.

Let M be a given model with similarity type L = L(M), and let L′ be any fragment of L∣L(M∣+,ω of cardinality ∣L(M)∣. We call N ≺ ML′-relatively saturated iff for every B ⊆ N of cardinality less than ∥N∥ every L′-type over B which is realized in M is realized in N. We discuss the existence of such submodels.

The following are corollaries of the existence theorems.

(1) If M is of cardinality at least ℶω1, and fails to have the ω order property, then there exists N ≺ M which is relatively saturated in M of cardinality ℶω1.

(2) Assume GCH. Let ψ ∈ Lω1, ω, and let L′ ⊆ Lω1, ω be a countable fragment containing ψ. If ∃χ > ℵ0 such that I(χ, ψ) < 2χ, then for every M ⊨ ψ and every cardinal λ < ∥M∥ of uncountable cofinality, M has an L′-relatively saturated submodel of cardinality λ.

In this paper we prove the strong normalization theorem for full first order classical N.D. (natural deduction)—full in the sense that all logical constants are taken as primitive. We also give a syntactic proof of the normal form theorem and (weak) normalization for the same system.

The theorem has been stated several times, and some proofs appear in the literature. The first proof occurs in Statman [1], where full first order classical N.D. (with the elimination rules for ∨ and ∃ restricted to atomic conclusions) is embedded in a system for second order (propositional) intuitionistic N.D., for which a strong normalization theorem is proved using strongly impredicative methods.

A proof of the normal form theorem and (weak) normalization theorem occurs in Seldin [1] as an extension of a proof of the same theorem for an N.D.-system for the intermediate logic called MH.

The proof of the strong normalization theorem presented in this paper is obtained by proving that a certain kind of validity applies to all derivations in the system considered.

The notion “validity” is adopted from Prawitz [2], where it is used to prove the strong normalization theorem for a restricted version of first order classical N.D., and is extended to cover the full system. Notions similar to “validity” have been used earlier by Tait (convertability), Girard (réducibilité) and Martin-Löf (computability).

In Prawitz [2] the N.D. system is restricted in the sense that ∨ and ∃ are not treated as primitive logical constants, and hence the deductions can only be seen to be “natural” with respect to the other logical constants. To spell it out, the strong normalization theorem for the restricted version of first order classical N.D. together with the well-known results on the definability of the rules for ∨ and ∃ in the restricted system does not imply the normalization theorem for the full system.

Many philosophers take set-theoretic discourse to be about objects of a special sort, namely sets; correlatively, they regard truth in such discourse as quite like truth in discourse about nonmathematical objects. There is a thin “disquotational” way of construing this construal; but that may candy-coat a philosophically substantive semantic theory: the Mathematical-Object theory of the basis for the distribution of truth and falsehood to sentences containing set-theoretic expressions. This theory asserts that truth and falsity for sentences containing set-theoretic expressions are grounded in semantic facts (about the relation between language and the world) of the sort modelled by the usual model-theoretic semantics for an uninterpreted formal first-order language. For example, it would maintain that ‘{ } ∈ {{ }}” is true in virtue of the set-theoretic fact that the empty set is a member of its singleton, and the semantic facts that ‘{ }’ designates the empty set,‘{{ }}’ designates its singleton, and ‘∈’ applies to an ordered pair of objects iff that pair's first component is a member of its second component.

Now this theory may come so naturally as to seem trivial. My purpose here is to loosen its grip by “modelling” an alternative account of the alethic underpinnings of set-theoretic discourse. According to the Alternative theory, the point of having set-theoretic expressions (‘set’ and ‘∈’ will do) in a language is not to permit its speakers to talk about some special objects under a special relation; rather it is to clothe a higher-order language in lower-order garments.

Let Γ be the unique (up to isomorphism) countable graph with the following property: (*) Given any two finite disjoint subsets U and V of Γ, there exists a vertex z ∈ Γ joined to every vertex in U and to none in V.

Thus Γ is the countable, universal, homogeneous graph; also known as the random graph. In this paper, we shall study the reducts of Γ Here a reduct of Γ is defined to be a permutation group (G, Γ) such that:

(i) Aut(Γ) ≤ G; and

(ii) G is a closed subgroup of Sym(Γ).

Equivalently, there exists a structure for some language L such that:

(iii) has universe Γ;

(iv) for each R ∈ L, is definable without parameters in Γ; and

(v) G = Aut().

In [12] Slaman and Steel posed the following problem:

Assume ZF + DC + AD. Suppose we have a function assigning to each Turing degree d a linear order <d of d. Then must the rationals embed order preservingly in <d for a cone of d's?

They had already obtained a partial answer to this question by showing that there is no such d ↦ <d with <d of order type ζ = ω* + ω on a cone. Already the possibility that <d has order type ζ · ζ was left open.

We use here, ideas and methods associated with the concept of amenability (of groups, actions, equivalence relations, etc.) to prove some general results from which one can obtain a positive answer to the above problem.

Lachlan [5] has shown that it is not possible to embed the diamond lattice in the r.e. Turing degrees while preserving least and greatest elements; that is, there do not exist incomparable r.e. Turing degrees a and b such that a ∧ b = 0 and a ∨ b = 0′. Cooper [3] has compared the r.e. Turing degrees to the enumeration degrees below 0e′ and has asked if the two structures are elementarily equivalent.

In this paper we show that such an embedding is possible in the Σ2enumeration degrees, which implies a negative answer to Cooper's question.

Theorem. There are low enumeration degreesaandbsuch thata ∧ b = 0eanda ∨ b = 0e′.

Lower case italic letters denote elements of ω while upper case italic letters denote subsets of ω. D, E and F are reserved for finite sets, and K for ′. If D = {x0, x1, …, xn} then the canonical index of D is , and the canonical index of is ∅. Dx denotes the set with canonical index x. {Wi}i∈ω is any fixed standard listing of the r.e. sets, and <·, ·> is any fixed recursive bijection from ω × ω to ω.

Intuitively, A is enumeration reducible to B if there is an effective algorithm for producing an enumeration of A from any enumeration of B. There is a natural one-to-one correspondence between all such algorithms and the r.e. sets.

In this paper, we show the normalization of proofs of NF (Quine's New Foundations; see [15]) minus extensionality. This system, called SF (Stratified Foundations) differs in many respects from the associated system of simple type theory. It is written in a first order language and not in a multi-sorted one, and the formulas need not be stratifiable, except in the instances of the comprehension scheme. There is a universal set, but, for a similar reason as in type theory, the paradoxical sets cannot be formed.

It is not immediately apparent, however, that SF is essentially richer than type theory. But it follows from Specker's celebrated result (see [16] and [4]) that the stratifiable formula (extensionality → the universe is not well-orderable) is a theorem of SF.

It is known (see [11]) that this set theory is consistent, though the consistency of NF is still an open problem.

The connections between consistency and cut-elimination are rather loose. Cut-elimination generally implies consistency. But the converse is not true. In the case of set theory, for example, ZF-like systems, though consistent, cannot be freed of cuts because the separation axioms allow the formation of sets from unstratifiable formulas. There are nevertheless interesting partial results obtained when restrictions are imposed on the removable cuts (see [1] and [9]). The systems with stratifiable comprehension are the only known set-theoretic systems that enjoy full cut-elimination.

In this paper the existence or nonexistence of isomorphic mappings between graph models for the untyped lambda calculus is studied. It is shown that Engeler's is DA completely determined, up to isomorphism, by the cardinality of its ‘atom-set’ A. A similar characterization is given for a collection of graph models of the -type; from this some propositions regarding automorphisms are obtained. Also we give an indication of the complexity of the first-order theory of graph models by showing that the second-order theory of first-order definable elements of a graph model is first-order expressable in the model.

Let G be a stable abelian group with regular modular generic. We show that either

1. there is a definable nongeneric K ≤ G such that G/K has definable connected component and so strongly regular generics, or

2. distinct elements of the division ring yielding the dependence relation are represented by subgroups of G × G realizing distinct strong types (when regarded as elements of Geq).

In the latter case one can choose almost 0-definable subgroups representing the elements of the division ring. We find a bound ((G: G0)) for the size of the division ring in case G has no definable subgroup K so that G/K is infinite with definable connected component. We show in case (2) that the group G/H, where H consists of all nongeneric points of G, inherits a weakly minimal group structure from G naturally, and Th(G/H) is independent of the particular model G as long as G/H is infinite.

Assuming AD + (V = L(R)), it is shown that for κ an admissible Suslin cardinal, o(κ) (= the order type of the stationary subsets of κ) is “essentially” regular and closed under ultrapowers in a manner to be made precise. In particular, o(κ) ≫ κ+, κ++, etc. It is conjectured that this characterizes admissibility for L(R).

Many-valued logics in general and 3-valued logic in particular is an old subject which had its beginning in the work of Łukasiewicz [Łuk]. Recently there is a revived interest in this topic, both for its own sake (see, for example, [Ho]), and also because of its potential applications in several areas of computer science, such as proving correctness of programs [Jo], knowledge bases [CP] and artificial intelligence [Tu]. There are, however, a huge number of 3-valued systems which logicians have studied throughout the years. The motivation behind them and their properties are not always clear, and their proof theory is frequently not well developed. This state of affairs makes both the use of 3-valued logics and doing fruitful research on them rather difficult.

Our first goal in this work is, accordingly, to identify and characterize a class of 3-valued logics which might be called natural. For this we use the general framework for characterizing and investigating logics which we have developed in [Av1]. Not many 3-valued logics appear as natural within this framework, but it turns out that those that do include some of the best known ones. These include the 3-valued logics of Łukasiewicz, Kleene and Sobociński, the logic LPF used in the VDM project, the logic RM3 from the relevance family and the paraconsistent 3-valued logic of [dCA]. Our presentation provides justifications for the introduction of certain connectives in these logics which are often regarded as ad hoc. It also shows that they are all closely related to each other. It is shown, for example, that Łukasiewicz 3-valued logic and RM3 (the strongest logic in the family of relevance logics) are in a strong sense dual to each other, and that both are derivable by the same general construction from, respectively, Kleene 3-valued logic and the 3-valued paraconsistent logic.

A basic goal in model-theoretic algebra is to obtain the classification of the complete extensions of a given (first-order) algebraic theory.

Results of this type, for the theory of totally ordered abelian groups, were obtained first by A. Robinson and E. Zakon [5] in 1960, later extended by Yu. Gurevich [4] in 1964, and further clarified by P. Schmitt in [6].

Within this circle of ideas, we give in this paper an axiomatization of the first-order theory of the class of all direct products of totally ordered abelian groups, construed as lattice-ordered groups (l-groups)—see the theorem below. We think of this result as constituing a first step—undoubtedly only a small one—towards the more general goal of classifying the first-order theory of abelian l-groups.

We write groups for abelian l-groups construed as structures in the language 〈 ∨, ∧, +, −, 0〉 (“−” is an unary operation). For unproved statements and unexplicated definitions, the reader is referred to [1].

A well-known question of Feferman asks whether there is a logic which extends the logic , is ℵ0-compact and satisfies the interpolation theorem. (Cf. Makowsky [M] for background and terminology.)

The same question was open when ℵ1 in is replaced by any other uncountable cardinal κ. We shall show that when κ is an uncountable strongly compact cardinal and there is a strongly compact cardinal > κ, then there is such a logic. It is impossible to prove the existence of uncountable strongly compact cardinals in ZFC. However, the logic that we describe has a simple and natural definition, together with several other pleasant properties. For example it satisfies Robinson's lemma, PPP (pair preservation property, viz. the theory of the sum of two models is the sum of their theories), versions of the elementary chain lemma for chains of length < λ, and isomorphism of (suitable) ultralimits.

This logic is described in §2 below; we call it 1. It is not a new logic—it was introduced in [Sh, Part II, §3] as an example of a logic which has the amalgamation and joint embedding properties. See the transparent presentation in [M]. But we shall repeat all the definitions. In [HS] we presented a logic with some of the same properties as 1, also based on a strongly compact cardinal λ; but unlike 1, it was not a sublogic of λ,λ.