A Boolean algebra (henceforth abbreviated B.A.) is said to be recursive if B is a recursive subset of the natural numbers N and the operations ∧ (meet), ∨ (join), and ¬ (complement) are partial recursive. Let denote the set of atoms of and denote the ideal generated by the atoms of . Given recursive B.A.s and , we write ≈ if is isomorphic to and ≈r if is recursively isomorphic to , i.e., if there is a partial recursive isomorphism from onto .

Recursive B.A.s have been studied by several authors including Ershov [2], Fiener [3], [4], Goncharov [5], [6], [7], LaRoche [8], Nurtazin [7], and the author [10], [11]. This paper continues a study of the recursion theoretic relationships among , , and the recursive isomorphism type of a recursive B.A. we started in [11]. We refer the reader to [11] for any unexplained notation and definitions. In [11], we were mainly concerned with the possible recursion theoretic properties of the set of atoms in recursive B.A.s. We found that even if we insist that be recursive, there is considerable freedom for the properties of . For example, we showed that if is a recursive B.A. such that is recursive and is infinite, then (i) there exists a recursive B.A. such that and both and are recursive and (ii) for any nonzero r.e. degree δ, there exist recursive B.A.s , , … such that for each i, is of degree δ, is recursive, is immune if i is even and is not immune if i is odd, and no two B.A.s in the sequence are recursively isomorphic.

We prove that there exists a noncomputable c.e. real which is low for weak 2-randomness, a definition of randomness due to Kurtz, and that all reals which are low for weak 2-randomness are low for Martin-Löf randomness.

“Apart from merits or defects of PA1, however, its existence demonstrates the feasibility of a new approach to the logic of propositions involving the principle of subjunctive contrariety. We thus have good reason to investigate the effect this principle, and a concept of conditionality compatible with it, might exert if introduced into standard quantification theory, into set theory, into modal logic and into epistemology and the philosophy of science.”

We present a cut elimination argument that witnesses the conservativity of the compositional axioms for truth (without the extended induction axiom) over any theory interpreting a weak subsystem of arithmetic. In doing so we also fix a critical error in Halbach’s original presentation. Our methods show that the admission of these axioms determines a hyper-exponential reduction in the size of derivations of truth-free statements.

Attention was directed to modal systems in which ‘necessarily α’ is interpreted as ‘α. is and always will be the case’ by Prior in his John Locke Lectures of 1956. The present paper shows that S4.3, the extension of S4 with

ALCLpLqLCLqLp,

is complete with respect to this interpretation when time is taken to be continuous, and that D, the extension of S4.3 with

ALNLpLCLCLCpLpLpLp,

is complete with respect to this interpretation when time is taken to be discrete. The method employed depends upon the application of an algebraic result of Garrett Birkhoff's to the models for these systems, in the sense of Tarski.

A considerable amount of work on S4.3 and D precedes this paper. The original model with discrete time is given in Prior's [7] (p. 23, but note the correction in [8]); that taking time to be continuous yields a weaker system is pointed out by him in [9]. S4.3 and D are studied in [3] of Dummett and Lemmon, where it is shown that D includes S4.3 and

CLCLCpLpLpCMLpLp.

While in Oxford in 1963, Kripke proved that these were in fact sufficient for D, using semantic tableaux. A decision procedure for S4.3, using Birkhoff's result, is given in my [2]. Dummett conjectured, in a conversation, that taking time to be continuous yielded S4.3. Thus the originality of this paper lies in giving a suitable completeness proof for S4.3, and in the unified algebraic treatment of the systems. It should be emphasised that the credit for first axiomatising D belongs to Kripke.

We prove the following Main Theorem: ZF + AD + V ⇒ L(R) ⇒ DC. As a corollary we have that Con(ZF + AD) ⇒ Con(ZF + AD + DC). Combined with the result of Woodin that Con(ZF + AD) ⇒ Con(ZF + AD + ¬ ACω) it follows that DC (as well as ACω) is independent relative to ZF + AD. It is finally shown (jointly with H. Woodin) that ZF + AD + ¬DCR, where DCR is DC restricted to reals, implies the consistency of ZF + AD + DC, in fact implies R# (i.e. the sharp of L(R)) exists.

In [3], Martin computed the degrees of certain classes of RE sets. To state the results succinctly, some notation is useful.

If A is a set (of natural numbers), dg(A) is the (Turing) degree of A. If A is a class of sets, dg ( A ) = {dg(A): A ∈ A ). Let M be the class of maximal sets, HHS the class of hyperhypersimple sets, and DS the class of dense simple sets. Martin showed that dg ( M ), dg ( HHS ), and dg ( DS ) are all equal to the set H of RE degrees a such that a ′ = 0″.

Let M * be the class of coinfinite RE sets having no superset in M ; and define HHS * and DS * similarly. Martin showed that dg ( DS *) = H. In [2], Lachlan showed (among other things) that dg ( M *)⊆K, where K is the set of RE degrees a such that a ″ > 0″. We will show that K ⊆ dg ( HHS *). Since maximal sets are hyperhypersimple, this gives dg ( M *) = dg ( HHS *) = K.

These results suggest a problem. In each case in which dg(A) has been calculated, the set of nonzero degrees in dg(A) is either H or K or the empty set or the set of all nonzero RE degrees. Is this always the case for natural classes A? Natural here might mean that A is invariant under all automorphisms of the lattice of RE sets; or that A is definable in the first-order theory of that lattice; or anything else which seems reasonable.

In their original paper on degrees [3], Kleene and Post showed that there is a degree between 0 and 0′. Later, Friedberg [1] and Muchnik [4] showed that there is a recursively enumerable degree between 0 and 0′. Since then, this phenomenon has been repeated several times: a result has been proved for degrees, and then, after considerable additional effort, it has been proved for recursively enumerable degrees.

There are some obvious respects in which that set of all degrees differs from the set of recursively enumerable degrees; e.g., the former is uncountable and has no largest member.

The present paper concerns the relation of relative interpretability introduced in [8], and arises from a question posed by Tarski: are there two finitely axiomatizable subtheories of the arithmetic of natural numbers neither of which is relatively interpretable in the other? The question was answered affirmatively (without proof) in [3], and the answer was generalized in [4]: for any positive integer n, there exist n finitely axiomatizable subtheories of arithmetic such that no one of them is relatively interpretable in the union of the remainder. A further generalization was announced in [5] and is proved here: there is an infinite set of finitely axiomatizable subtheories of arithmetic such that no one of them is relatively interpretable in the union of the remainder. Several lemmas concerning the existence of self-referential and mutually referential formulas are given in Section 1, and will perhaps be of interest on their own account.

Cet article ne contient rien de révolutionnaire, et son auteur a conscience du risque qu'il court de le voir dépassé, lors de sa parution, par des travaux plus profonds. Il a pensé qu'il n'était pas inutile de publier, faute de mieux, les résultats simples auxquels il est parvenu (le lecteur lui saura gré de ce caractère reposant), en espérant qu'il passeront à la postérité sous forme d'exercices dans les manuels futurs où les petits enfants apprendront la théorie des modèles.

Il s'agit de groupes stables; on sait depuis longtemps que la stabilité de la théorie d'un groupe impose des “conditions de chaîne” sur ses sous-groupes définissables : l'exploitation de ce phénomène, de nature bien algébrique, qui est brièvement exposé dans la première section de cet article, a fait le bonheur d'une génération de théoriciens des modèles. Un autre phénomène, plus subtil, semble ne pas avoir épuisé sa substance : c'est celui, dont l'apparition remonte aux travaux de B. Zilber, qui est décrit dans [7] sous le nom de “types de strate maximum”, et dans [2] sous le nom de “large sets”; la deuxième section lui est consacrée: elle a été écrite dans le désir de montrer l'équivalence de ces deux approches, et aussi par repentir de n'avoir pas suffisament éclairé ses motivations dans [7]. Ce souci d'unification a eu une influence, que j'espère salutaire, sur le vocabulaire: je parle ici de “types génériques” et d'“ensembles (ou de formules) génériques”. Ces termes, ainsi que celui de “composante connexe”, sont empruntés au langage de la géométrie: un groupe algébrique, étant définissable dans la théorie d'un corps algébriquement clos, est stable, et ses “types génériques” sont les “points génériques” des géomètres.

In teaching symbolic logic to beginners, it is a not infrequent experience to encounter difficulties in the transition from the informal “if …, then …” construction of common discourse to its analysis in terms of material implication and its truth-table. There is no trouble with the idea that “if p, then q” must be so understood that “if p/T1, then we must have (p⊃q)T when q/T, and (P⊃q)/F when q/F. There is thus no problem in leading the explanation to the point.

A notion of relative reducibility for partial functions, which coincides with Turing reducibility on the total functions, was first given by S.C. Kleene in Introduction to metamathematics [4]. Following Myhill [7], this was made more explicit in Hartley Rogers, Jr., Theory of recursive functions and effective computability [8, pp. 146, 279], where some basic properties of the partial degrees or (equivalent, but notationally more convenient) the enumeration degrees, were derived. The question of density of this proper extension of the degrees of unsolvability was left open, although Medvedev's result [6] that there are quasi-minimal partial degrees (that is, nonrecursive partial degrees with no nonrecursive total predecessors) is proved.

In 1971, Sasso [9] introduced a finer notion of partial degree, which also contained the Turing degrees as a proper substructure (intuitively, Sasso's notion of reducibility between partial functions differed from Rogers' in that computations terminated when the oracle was asked for an undefined value, whereas a Rogers computation could be thought of as proceeding simultaneously along a number of different branches of a ‘consistent’ computation tree—cf. Sasso [10]). His construction of minimal ‘partial degrees’ [11], while of interest in itself, left open the analogous problem for the more standard partial degree structure.

This paper proves that the disjunction property, the numerical existence property. Church's rule, and several other metamathematical properties hold true for Constructive Zermelo-Fraenkel Set Theory, CZF, and also for the theory CZF augmented by the Regular Extension Axiom.

As regards the proof technique, it features a self-validating semantics for CZF that combines realizability for extensional set theory and truth.

1. Introduction. Since this paper is a written version of one presented as a survey lecture at a meeting of the Association for Symbolic Logic, its form and content have been essentially determined by the form and content of that lecture, and these latter were themselves considerably influenced by a deliberate attempt to avoid the lecture consisting essentially either of a catalogue of results in some fairly wide field or of the presentation of detailed proofs of a few particular results in a very limited field, with, in either case, a consequential serious limitation of the time available for discussion of the motivation for the results and of the connections between them. There is thus no attempt to cover, even in outline, the full range of topics which could reasonably fall within the scope of its title.

The paper consists mainly of a general discussion of some results concerned with finite models of axiomatically defined calculi of propositional form, with particular reference to the occurrence of such models in proofs that certain propositional calculi are decidable. In addition, there is an account of some results concerned with the existence of undecidable propositional calculi and of others connected with the decidability or undecidability of certain structure problems which relate either to sets of propositional calculi or to different presentations of the same calculus.

Effective model theory is the subject that analyzes the typical notions and results of model theory to determine their effective content and counterparts. The subject has been developed both in the former Soviet Union and in the west with various names (recursive model theory, constructive model theory, etc.) and divergent terminology. (We use “effective model theory” as the most general and descriptive designation. Harizanov [6] is an excellent introduction to the subject as is Millar [13].) The basic subjects of model theory include languages, structures, theories, models and various types of maps between these objects. There are many ways to introduce considerations of effectiveness into the area. The two most prominent derive from starting, on the one hand, with the notion of a theory and its models or, on the other, with just structures.

If one begins with theories, then a natural version of effectiveness is to consider decidable theories (i.e., ones with a decidable (equivalently, computable or recursive) set of theorems). When one moves to models and wants them to be effective, one might start with the requirement that the model (of any theory) have a decidable theory (i.e., Th (), the set of sentences true in , is decidable). Typically, however, one wants to be able to talk about the elements of the model as well as its theory in the given language. Thus one naturally considers the model as a structure for the language expanded by adding a constant ai, for each element ai of . Of course, one requires that the mapping from the constants to the corresponding elements of be effective (computable). We are thus lead to the following basic definition:

A structure or model is decidable if there is a computable enumeration ai of A, the domain of , such that Th(, ai,) is decidable. (Of course, ai, is interpreted as ai, for each i Є ω.)

We define the notion of Souslin forcing, and we prove that some properties are preserved under iteration. We define a weaker form of Martin's axiom, namely , and using the results on Souslin forcing we show that is consistent with the existence of a Souslin tree and with the splitting number s = ℵ1. We prove that proves the additivity of measure. Also we introduce the notion of proper Souslin forcing, and we prove that this property is preserved under countable support iterated forcing. We use these results to show that ZFC + there is an inaccessible cardinal is equiconsistent with ZFC + the Borel conjecture + -measurability.

A structure is automatic if its domain, functions, and relations are all regular languages. Using the fact that every automatic structure is decidable, in the literature many decision problems have been solved by giving an automatic presentation of a particular structure. Khoussainov and Nerode asked whether there is some way to tell whether a structure has, or does not have, an automatic presentation. We answer this question by showing that the set of Turing machines that represent automata-presentable structures is ${\rm{\Sigma }}_1^1 $-complete. We also use similar methods to show that there is no reasonable characterisation of the structures with a polynomial-time presentation in the sense of Nerode and Remmel.

It will be shown that propositional tense logic (with the Kripke relational semantics) may be regarded as a fragment of propositional modal logic (again with the Kripke semantics). This paper deals only with model theory. The interpretation of formal systems of tense logic as formal systems of modal logic will be discussed in [6].

The languages M and T, of modal and tense logic respectively, each have a countable infinity of propositional variables and the Boolean connectives; in addition, M has the unary operator ⋄ and T has the unary operators F and P. A structure is a pair <W, ≺<, where W is a nonempty set and ≺ is a binary relation on W. An assignment V assigns to each propositional variable p a subset V(p) of W. Then V(α)£ W is defined for all formulas α of M or T by induction:

We say that α is valid in <W, ≺>, or <W, ≺>, ⊨ α, if ⊩ (α) = W for every assignment V for <W, ≺>. If Γ is a set of formulas of M [T] and α is a formula of M [T], then α is a logical consequence of Γ, or Γ ⊩ α,if α is valid in every model of Γ i.e., in every structure in which all γ ∈ Γare valid.

In the thirty years since its invention by Abraham Robinson, nonstandard analysis has become a useful tool for research in many areas of mathematics. It seems fair to say, however, that the search for practically satisfactory foundations for the subject is not yet completed. New proposals, intended to remedy various shortcomings of older approaches, continue to be put forward. The objective of this paper is to show that nonstandard concepts have a natural place in the usual (more or less “standard”) set theory, and to argue that this approach improves upon various aspects of hitherto considered systems, while retaining most of their attractive features. We do this by working in Zermelo-Fraenkel set theory with non-well-founded sets. It has always been clear that the axiom of regularity may fail for external sets. The previous approaches either avoid non-well-foundedness by considering only that fragment of nonstandard set theory that is well-founded (over individuals; enlargements of Robinson and Zakon [17]) or reluctantly live with it (various axiomatic nonstandard set theories). Ballard and Davidon [2] were the first to propose constructive use for non-well-foundedness in the foundations of nonstandard analysis. In the present paper we adopt a very strong anti-foundation axiom. In the resulting more or less “usual” set theory, the (to the “standard” mathematician) unfamiliar concepts of standard, external and internal sets can be defined and their requisite properties proved (rather than postulated, as is the case in axiomatic nonstandard set theories).

It is known that a countable $\omega $ -categorical structure interprets all finite structures primitively positively if and only if its polymorphism clone maps to the clone of projections on a two-element set via a continuous clone homomorphism. We investigate the relationship between the existence of a clone homomorphism to the projection clone, and the existence of such a homomorphism which is continuous and thus meets the above criterion.