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.

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.

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 Є ω.)

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.

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.

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.

We give topological characterizations of filters ${\cal F}$ on ω such that the Mathias forcing ${M_{\cal F}}$ adds no dominating reals or preserves ground model unbounded families. This allows us to answer some questions of Brendle, Guzmán, Hrušák, Martínez, Minami, and Tsaban.

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.

We study dp-minimal and strongly dependent theories and investigate connections between these notions and weight.

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).

What is an inference rule? This question does not have a unique answer. One usually finds two distinct standard answers in the literature; validity inference (σ ⊦vφ for every substitution τ, the validity of τ[σ] entails the validity of τ[φ]), and truth inference (σ⊦l φ if for every substitution τ, the truth of τ[σ] entails the truth of τ[φ]). In this paper we introduce a general semantic framework that allows us to investigate the notion of inference more carefully. Validity inference and truth inference are in some sense the extremal points in our framework. We investigate the relationship between various types of inference in our general framework, and consider the complexity of deciding if an inference rule is sound, in the context of a number of logics of interest: classical propositional logic, a nonstandard propositional logic, various propositional modal logics, and first-order logic.

In [2] Bachmann showed how a hierarchy of normal functions on the countable ordinals Ω can be constructed using certain uncountable ordinals together with appropriate fundamental sequences for limit ordinals, as indexing ordinals for the hierarchy. This method, explained in more detail in §1 below, has been generalized by Pfeiffer [6] and Isles [4] to produce larger hierarchies. Using the hierarchies constructed in this way it is possible, as an immediate consequence of the definitions, to assign ω-sequences 〈αn〉n∈ω to limit ordinals α in an initial segment I of Ω such that . Indeed this was the motivation for Bachmann's original construction. However the initial segments I constructed in this way are of interest even without the fundamental sequences because they occur naturally as the proof-theoretic ordinals associated with particular formal theories. The fundamental sequences necessary for the Bachmann method are not intrinsically of interest proof-theoretically and only serve to obscure the definitions of the associated initial segments. Feferman and Weyhrauch [9] suggested an alternative definition for a sequence of functions on the countable ordinals. This definition was generalized by Aczel [1] who showed how the new functions corresponded to those in Bachmann's hierarchy. (Independently, Weyhrauch established the same results for an initial segment of the sequence of Bachmann functions, i.e. those functions indexed by α < εΩ+1.)

It is well known that classical propositional logic can be interpreted in intuitionistic prepositional logic. In particular Glivenko's theorem states that a formula is provable in the former iff its double negation is provable in the latter. We extend Glivenko's theorem and show that for every involutive substructural logic there exists a minimum substructural logic that contains the first via a double negation interpretation. Our presentation is algebraic and is formulated in the context of residuated lattices. In the last part of the paper, we also discuss some extended forms of the Koltnogorov translation and we compare it to the Glivenko translation.

We prove that degrees that are low for Kurtz randomness cannot be diagonally non-recursive. Together with the work of Stephan and Yu [16], this proves that they coincide with the hyperimmune-free non-DNR degrees, which are also exactly the degrees that are low for weak 1-genericity.

We also consider Low(ℳ, Kurtz), the class of degrees a such that every element of ℳ is a-Kurtz random. These are characterised when ℳ is the class of Martin-Löf random, computably random, or Schnorr random reals. We show that Low(ML, Kurtz) coincides with the non-DNR degrees, while both Low(CR, Kurtz) and Low(Schnorr, Kurtz) are exactly the non-high, non-DNR degrees.

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.

We introduce stable canonical rules and prove that each normal modal multi-conclusion consequence relation is axiomatizable by stable canonical rules. We apply these results to construct finite refutation patterns for modal formulas, and prove that each normal modal logic is axiomatizable by stable canonical rules. We also define stable multi-conclusion consequence relations and stable logics and prove that these systems have the finite model property. We conclude the paper with a number of examples of stable and nonstable systems, and show how to axiomatize them.

In the early days of the development of Kripke-style semantics for modal logic a great deal of effort was devoted to showing that particular axiom systems were characterised by a class of models describable by a first-order condition on a binary relation. For a time the approach seemed all encompassing, but recent work by Thomason [6] and Fine [2] has shown it to be somewhat limited—there are logics not determined by any class of Kripke models at all. In fact it now seems that modal logic is basically second-order in nature, in that any system may be analysed in terms of structures having a nominated class of second-order individuals (subsets) that serve as interpretations of propositional variables (cf. [7]). The question has thus arisen as to how much of modal logic can be handled in a first-order way, and precisely which modal sentences are determined by first-order conditions on their models. In this paper we present a model-theoretic characterisation of this class of sentences, and show that it does not include the much discussed LMp → MLp.

Definition 1. A modal frame ℱ = 〈W, R〉 consists of a set W on which a binary relation R is defined. A valuation V on ℱ is a function that associates with each propositional variable p a subset V(p) of W (the set of points at which p is “true”).

We determine the exact bounds for the length of an arbitrary reduction sequence of a term in the typed λ-calculus with β-, ξ- and η-conversion. There will be two essentially different classifications, one depending on the height and the degree of the term and the other depending on the length and the degree of the term.

Combining techniques of the first author and Shelah with ideas of Magidor, we show how to get a model in which, for fixed but arbitrary finite n, the first n strongly compact cardinals k1..…kn are so that ki; for i = 1..…n is both the ith measurable cardinal and supercompact. This generalizes an unpublished theorem of Magidor and answers a question of Apter and Shelah.

Slaman and Wehner have constructed structures which distinguish the computable Turing degree 0 from the noncomputable degrees, in the sense that the spectrum of each structure consists precisely of the noncomputable degrees. Downey has asked if this can be done for an ordinary type of structure such as a linear order. We show that there exists a linear order whose spectrum includes every noncomputable degree, but not 0. Since our argument requires the technique of permitting below a set, we include a detailed explantion of the mechanics and intuition behind this type of permitting.