In [4] Curry raised the possibility that his system proposed in ξ15C of [3] might be inconsistent. In this paper this inconsistency is proved using a method also employed in [1].

From Curry's axiom ⊦LH, it follows that

holds for arbitrary X.

The other results from that are required are

Modus Ponens, and the Deduction Theorem for implication:

Assuming ⊦HA, we define as in [1]:

and let

where Y is the paradoxical (or fixed point) combinator.

In [B1] and [B2] we have shown that the classical theorems on the continuity of effective operations are not derivable in various constructive formal systems. The purpose of this paper is to establish that these systems are closed under the corresponding rules of inference, which have the form: If e can be proved to be (the index of) an effective operation, then e can be proved to be continuous. In fact we establish closure under apparently stronger rules of the form, if e can be proved to be an effective operation, then e* can be proved to be (the index of) a modulus of continuity for e, where e* is canonically obtained from e.

We again deal with two kinds of effective operations: (i) partial operations on partial arguments, and (ii) total operations on total arguments. The continuity theorem for operations of kind (i) is due to Myhill-Shepherdson [MS] and is called MS; for kind (ii) is due to Kreisel, Lacombe, and Shoenfield [KLS] and is called KLS. We also deal with effective operations on the (recursive) real numbers, which are of kind (ii). In [B1], [B2] it is shown that KLS and MS are derivable in in-tuitionistic arithmetic HA from Markov's principle MP (this follows from examination of the classical proofs); that they do not imply MP in HA; and that they are not derivable in HA. (These theorems remain true when HA is replaced by various stronger systems.) The derived rules to be established in this paper therefore represent nontrivial closure properties of the systems to which they apply.

Before the remarkable theorem of Martin and Steel [6] showing that the existence of a supercompact cardinal κ implies L[R] ⊨ ZF + AD + DC, and the later theorem of Woodin [9] showing that Con(ZFC + There exists an ω sequence of Woodin cardinals) ⇔ Con(ZF + AD + DC), much set-theoretic research was focused upon showing that the consistency of fragments of AD + DC followed from more “reasonable” hypotheses such as versions of supercompactness. A good example of this is provided by the results of [1], in which the following theorems are proven.

Each relational structure X has an associated Gaifman graph, which endows X with the properties of a graph. If x is an element of X, let Bn(x) be the ball of radius n around x. Suppose that X is infinite, connected and of bounded degree. A first-order sentence ϕ in the language of X is almost surely true (resp. a.s. false) for finite substructures of X if for every x ∈ X, the fraction of substructures of Bn(x) satisfying ϕ approaches 1 (resp. 0) as n approaches infinity. Suppose further that, for every finite substructure, X has a disjoint isomorphic substructure. Then every ϕ is a.s. true or a.s. false for finite substructures of X. This is one form of the geometric zero-one law. We formulate it also in a form that does not mention the ambient infinite structure. In addition, we investigate various questions related to the geometric zero-one law.

In this paper we study the consistency strength of the theory

and we prove the consistency of this theory relative to the consistency of the existence of a supercompact cardinal and an inaccessible above it.

The purpose of this note is to clarify two points about the topos Lif, introduced in [13] as a generalization of Lifschitz' realizability ([9, 12]). Lif is a subtopos of Hyland's Effective topos ([1]). The points I want to make are:

Remark 1. Lif is the largest subtopos of satisfying the axiom (O):

where denotes partial recursive application, and “∈ Tot” means that e and f range over codes for total recursive functions. One may read (O) as the statement “The union of two -sets is again a -set”. That is, let be a subtopos of . Then (O) is true in for the standard interpretation (the variables range over the natural numbers object of , etc.) if and only if the inclusion ↣ factors through the inclusion Lif ↣ .

Remark 2. Like , Lif contains at least two weakly complete internal full subcategories, thus providing us with more models of polymorphism and other impredicative type theories.

The principle (O) has some standing in the history of constructive mathematics:

- H. Friedman has proved that (O) is equivalent to a formulation of intuitionistic completeness of the intuitionistic predicate calculus for Tarskian semantics; see [8]. This is not to imply that this result is of immediate relevance to Lif: Friedman works in a system of analysis, a theory of lawless sequences with an axiom of “open data” for arithmetical formulas, which at least for the domain of all functions from N to N fails in Lif. However, there might exist a “nonstandard model” of arithmetic and a corresponding system of analysis, in which we may be able to carry out his proof.

- Moreover, Remark 2 entails that Lif should provide us with models of synthetic domain theory (for an exposition, see [3]), and one with the nice property that the dual of one of the axioms (axiom 7 in [3]) comes for free, by (O).

We prove that there are 2χ0 pairwise non elementarily equivalent existentially closed ordered groups, which solve the main open problem in this area (cf. [3, 10]).

A simple direct proof is given of the weaker fact that the theory of ordered groups has no model companion; the case of the ordered division rings over a field k is also investigated.

Our main result uses constructible sets and can be put in an abstract general framework.

Comparison with the standard methods which use forcing (cf. [4]) is sketched.

Two questions were left open in [1]. 1) Do W(σ) and W(r) have the same many-one degree for any σ, τ such that ωη+1.2 ≤ σ < τ < ωη+2? 2) Is W(σ) many-one reducible to W(r) for any σ, τ such that ωη+1.2 ≤ σ < τ < ωη+2? We answered the second question affirmatively in [2]. In this paper we answer the first question in the negative. From the results of [1] [2] and this paper we have a complete picture of the many-one degrees of the predicates e ∈ W(σ)

In a current paper, Church and Quine show how any dyadic relation of natural numbers can be defined in terms of a symmetric dyadic relation of natural numbers together with the truth functions and quantification over natural numbers. The purpose of the present note is to extend their result to the following: Where R1, R2, …, ad infinitum are any classes or relations (of any degree) of natural numbers, they can all be defined in terms of a single symmetric dyadic relation of natural numbers together with the truth functions and quantification over natural numbers.

Let pi, for each i, be the tth prime > 1. Let the degree of Ri, for each i, be di. Let R be the dyadic relation which each number x bears to each number y such that either x is a factor of y or else x is 0 and y is for some such that . Since R is dyadic, we know from Church and Quine's result that R is definable in terms of a symmetric dyadic relation. Moreover, as seen in the incidental constructions in §1 of Church and Quine, ‘y = x + 1’ is expressible on the same basis.

Let R be a commutative ring with 1 and R[X 1, …, Xn ] the polynomial ring in n variables over R. Then for any relation f(X) = 0 in R[X] there exists a conjunction of equations φ f such that f(X) = 0 holds in R[X] iff φ f holds in R; φ f is of course the formula saying that all the coefficients of f(X) vanish. Moreover, φ f is independent of R and formed uniformly for all polynomials f up to a given formal degree. In this paper we investigate first order theories T for which a similar phenomenon holds. More precisely, we let TAH be the universal Horn part of a theory T and look at free extensions of models of T in the class of models of TAH . We ask whether an atomic relation t 1(X, a) = t 2(X, a) or R(t 1(X, a), …, tn (X, a)) in can be equivalently expressed by a finite or infinitary formula φ(a) in , such that φ(y) depends only on t i{X, y) and not on or a 1, …, am ∈ A.

We will show that for a wide class of theories T “defining formulas” φ(y) in this sense exist and can be taken as infinite disjunctions of positive existential formulas.

We show that the theory of the real field with a generic real power function is decidable, relative to an oracle for the rational cut of the exponent of the power function. We also show the existence of generic computable real numbers, hence providing an example of a decidable o-minimal proper expansion of the real field by an analytic function.

Indecomposability of ultrafilters was introduced by Keisler as a natural weakening of the concept of measurability. The property was first studied in depth by Chudnovsky and Chudnovsky, Prikry, and Silver (see [4] and [5]). One intriguing result of this early work was the following theorem: if κ is an inaccessible cardinal and there is an indecomposable ultrafilter over κ, then κ is in fact ω-Mahlo. Silver asked whether this result could be strengthened to say that an inaccessible cardinal carrying an indecomposable ultrafilter must be measurable. We prove in this paper that this is not the case; we construct a model where κ is inaccessible and carries an indecomposable ultrafilter but κ is not even weakly compact.

The results in this paper form part of the research for my doctoral dissertation at the University of California, Berkeley. I would like to thank my thesis advisor, Robert Solovay, for his patient guidance during this endeavor.

In this note we partly answer a question left open in [1, p. 52] by proving the following theorem.

Theorem. Supposep0≧2, ωn+1·p0≦σ<ωn+1(p0+1). Then W(σ) is uniformly many-one reducible to W(τ) for τ≧(ωn+1·p0)+1.

To prove this theorem we need only show that there is a recursive function f(e) such that if ∣e∣<σ, then ∣f(e)<(ωn+1·p0)+1, while if ∣e∣ ≮ σ, f(e)∉W. (For the notations see [2].)

The forcing construction ℙmax, invented by W. Hugh Woodin, produces a model whose collection of subsets of ω1 is in some sense maximal. In this paper we study the Boolean algebra induced by the nonstationary ideal on ω1 in this model. Among other things we show that the induced quotient does not have a simply definable form. We also prove several results about saturation properties of the ideal in this extension.

Epistemic arithmetic—that is, first-order arithmetic with S4 as the underlying logic—was introduced by Shapiro in [7] and independently by Reinhardt in [6]. Shapiro showed that intuitionistic first-order arithmetic HA can be embedded in epistemic arithmetic EA . Moreover he showed that some of the basic proof-theoretic facts about HA , such as the existence and disjunction properties, can be extended to EA . In [3] we showed that the interpretation of HA in EA is faithful. (G.E. Mine has independently also proved this theorem.) Finally, in [2], Flagg showed that a suitable form of Church's thesis is consistent with EA . (Carlson [1] has announced another proof of this result.) Flagg's argument involves an ingenious realizability notion for EA which, as it stands, is not very perspicuous. The purpose of the present paper is to give a more transparent treatment of Flagg realizability. We obtain a new version of Flagg's proof of the consistency of Church's thesis with EA . Our main new result is that, in a sense to be made precise below, Flagg realizability coincides on HA embedded in EA with Kleene's 1945 realizability (e.g. see [5, pp. 501–516]). Thus it turns out once more that methods and results proved for EA can be viewed as extensions or generalizations of well-known methods and results for HA .

The large cardinal-like properties of saturated ideals have been investigated by various authors, including Foreman [F], and Jech and Prikry [JP], among others. One of the most interesting consequences of a strongly compact cardinal is the following theorem of Solovay [So2]: if a strongly compact cardinal exists then the singular cardinal hypothesis holds above it. In this paper we discuss the question of relating the existence of saturated ideals and the singular cardinal hypothesis. We will show that the existence of “strongly” saturated ideals implies the singular cardinal hypothesis. As a biproduct we will present a proof of the above mentioned theorem of Solovay using generic ultrapowers. See Jech and Prikry [JP] for a nice exposition of generic ultrapowers. We owe a lot to the work of Foreman [F]. We would like to express our gratitude to Noa Goldring for many helpful comments and discussions.

Throughout this paper we assume that κ is a strongly inaccessible cardinal and λ is a cardinal >κ. By an ideal on κλ we mean a κ-complete fine ideal on Pκλ. For I an ideal on κλ let PI denote the poset of I-positive subsets of κλ.

Definition. Let I be an ideal on κλ. We say that I is a bounding ideal if 1 ⊩-PI “δ(δ is regular cardinal ”.

We can show that if a normal ideal is “strongly” saturated then it is bounding.

Theorem 1. If 1 is an η-saturated normal ideal onκλ, where η is a cardinal <λsuch that there are fewer thanκmany cardinals betweenκand η (i.e. η < κ+κ), then I is bounding.

Proof. Let I be such an ideal on κλ. By the work of Foreman [F] and others, we know that every λ+-saturated normal ideal is precipitous. Suppose G is a generic filter for our PI. Let j: V → M be the corresponding generic elementary embedding. By a theorem of Foreman [F, Lemma 10], we know that Mλ ⊂ M in V[G]. By η-saturation, cofinalities ≥η are preserved; that is, if cfvα ≥ η, then cfvα = cfv[G]α. From j ↾ Vκ being the identity on Vκ and M being λ-closed in V[G], we conclude that cofinalities <κ are preserved. Therefore if cfvα ≠ cfv[G]α then κ ≤ cfvα < η.

The main result is Vaught's conjecture for weakly minimal, locally modular and non-ω-stable theories. The more general results yielding this are the following.

Theorem A. Suppose that T is a small unidimensional theory and D is a weakly minimal set, definable over the finite set B. Then for all finite A ⊂ D there are only finitely many nonalgebraic strong types over B realized in acl(A) ∩ D.

Theorem B. Suppose that T is a small, unidimensional, non-ω-stable theory such that the universe is weakly minimal and locally modular. Then for all finite A there is a finite B ⊂ cl(A) such that a ∈ cl(A) iff a ∈ cl(b) for some b ∈ B.

Recall the property (S) defined in the abstract of [B1].

Theorem C. Let T be as in Theorem B. Then, if T does not satisfy (S), T has many countable models.

Combining Theorem C and the results in [B1] we obtain Vaught's conjecture for such theories.

It is proved (Theorem 1) that if 0# exists, then any constructible forcing property which over L adds no reals, over V collapses an uncountable L-cardinal to cardinality ω. This improves a theorem of Foreman, Magidor, and Shelah. Also, a method for approximating this phenomenon generically is found (Theorem 2). The strategy is first to reduce the problem of ‘disabling’ forcing properties to that of specializing certain trees in a weak sense.