We present a faithful axiomatization of von Mises' notion of a random sequence, using an abstract independence relation. A byproduct is a quantifier elimination theorem for Friedman's “almost all” quantifier in terms of this independence relation.

A computer handles λ-terms more easily if these are translated into combinatory terms. This translation process is called bracket abstraction. The simplest abstraction algorithm—the (fab) algorithm of Curry (see Curry and Feys [6])—is lengthy to implement and produces combinatory terms that increase rapidly in length as the number of variables to be abstracted increases.

There are several ways in which these problems can be alleviated:

(1) A change in order of the clauses in the algorithm so that (f) is performed as a last resort.

(2) The use of an extra clause (c), appropriate to βη reduction.

(3) The introduction of a finite number of extra combinators.

The original 1924 form of bracket abstraction of Schönfinkel [17], which in fact predates λ-calculus, uses all three of these techniques; all are also mentioned in Curry and Feys [6].

A technique employed by many computing scientists (Turner [20], Peyton Jones [16], Oberhauser [15]) is to use the (fab) algorithm followed by certain “optimizations” or simplifications involving extra combinators and sometimes special cases of (c).

Another is either to allow a fixed infinite set of (super-) combinators (Abdali [1], Kennaway and Sleep [10], Krishnamurthy [12], Tonino [19]) or to allow new combinators to be defined one by one during the abstraction process (Hughes [7] and [8]).

A final method encodes the variables to be abstracted as an n-tuple—this requires only a finite number of combinators (Curien [5], Statman [18]).

We show that the following property (LN) holds in the basic Cohen model as sketched by Jech: The order topology of any linearly ordered set is normal. This proves the independence of the axiom of choice from LN in ZF, and thus settles a question raised by G. Birkhoff (1940) which was partly answered by van Douwen (1985).

Recursive model theory is supposed to be the study of the effectiveness of constructions and theorems in model theory. This often involves getting “effective” versions of various classical model-theoretic notions. The traditional way of doing this is to restrict attention to recursive models, and recursive isomorphisms between them, etc. Thus for example the following definition appears in the literature (in [3] and [1]).

Definition. Given a recursive model A and an n Є ω, a subset R ⊆ An is called intrinsically r.e. provided that for every recursive model B ≈ A, the isomorphic image in B of R is an r.e. subset of Bn.

It is clear that if R is definable by a (recursive, infinitary) Σ10 formula (with finitely many parameters from A), then R is intrinsically r.e. It seems natural for the converse to be true. Indeed, provided that (A, R) is sufficiently “regular” in a sense made precise in a theorem of Ash and Nerode (see [3]), the converse is true. However, if we drop the (rather strong) regularity conditions, there exist “pathological” examples of intrinsically r.e. relations which are not definable by a Σ10 formula (see [7]).

In this paper, we suggest a rather different approach to studying the effectiveness of model theory, an approach we have dubbed “effective model theory”. The basic idea is to allow arbitrary nonrecursive models, but to require all notions to be relativized to the complexity of the models involved. (Much the same notion has been used in [2] under the name “relatively recursive model theory”.) Thus for example we have the following effective model theory version of the property of being intrinsically r.e.

In [vDF], van Douwen and Fleissner introduce a number of axioms which hold in models constructed by iteratively forcing MA in a nontrivial extension of the set-theoretic universe. One such model is the Bell-Kunen model, obtained by starting with a model of ZFC + GCH, then forcing “MA + ϲ = ω2” by the standard means, then forcing “MA + ϲ = ω3”, and so on. The Bell-Kunen model is the result of an ω1 sequence of extensions of this form, with direct limits taken at limit ordinals. (See [BK] for a more complete description.) Van Douwen and Fleissner observed that many of the properties of this model could be distilled into a “Definable Forcing Axiom”, which states that “If P is a c.c.c. partial order which is definable from a real, then there is a sequence of filters through , such that if is any dense subset of P, then all but countably many of the ℱα's meet in a nonempty set.” (They call such a sequence ω1-generic.) Van Douwen and Fleissner ask whether one can eliminate the restriction on the c.c.c. order entirely; the resulting axiom (“If P is any c.c.c. partial order of cardinality at most ϲ, then there is a sequence of filters…”) is called the Undefinable Forcing Axiom (UFA).

In what follows, a coset is a subset of a group G of the form aH, where H is a subgroup of G; H can be recovered from the coset C: it is the only subgroup which is obtained from C by a left translation; we note in passing that these cosets, that we write systematically with the group to the right, are also of the form Ka, since aH = aHa−1a. A classical combinatorial lemma involving cosets appears in Neumann [1952]: If the coset C = aH is the union of the finite family of cosets C1 = a1H1,…,Cn = anHn, then it is the union of those Ci whose corresponding Hi has finite index in H.

In a structure where a group G is defined, Boolean combinations of cosets modulo its definable subgroups form a family of definable sets (by definable, we mean “definable with parameters”). The situation when any definable set is of that kind has been characterized model-theoretically in Hrushovski and Pillay [1987]: A group G is one-based if and only if, for each n, every definable subset of the cartesian power Gn is a(finite!) Boolean combination of cosets modulo definable subgroups. One side is given by a beautiful lemma of Pillay, stating that, in a one-based group which is saturated enough, every type is a right translate of the generic of its left stabilizer.

La première partie de cet article ([10], que nous désignerons par (I) dans la suite) était consacrée à la théorie élémentaire TX des algèbres de Boole munies d'idéaux distingués indéxés dans un ensemble X. On a vu que les idéaux définissables dans un modèle de Tx forment la sous-algèbre engendrée par les idéaux distingués de l'algèbre de Heyting des idéaux de munie de l'opérateur sa défini par sa(K) = {a: a/K est sans atome}, et que la théorie de peut être caractérisée par la structure composée de l'algèbre de Heyting des idéaux définissables munie de l'opérateur sa et des idéaux distingués, et par l'application qui à tout K de fait correspondre le nombre d'atomes de /K, pris dans N ⋃ {∞}.

Nous montrons maintenant que les structures possibles peuvent être définies de façon axiomatique en introduisant une classe équationnelle d'algèbres de Heyting munies d'une opération unaire, dites sa-algèbres de Heyting (en abrégé sa-AH), et en prouvant que cette classe est constituée des algèbres pouvant être plongées dans l'algèbre de Heyting des idéaux d'une algèbre de Boole, munie de l'opérateur sa. Ainsi les sont, à isomorphisme près, les sa-AH engendrées par des éléments distingués indéxés dans X; on en déduit une classification des extensions complètes de Tx en montrant que les applications qui peuvent être associées à une structure de la forme pour caractériser la théorie d'un modèle sont déterminées par leur restriction à une partie M() définie uniformément, sur laquelle elles prennent des valeurs dans (N − {0}) ⋃ {∞}, et que réciproquement toute application de M() dans (N − {0}) ⋃ {∞} est une telle restriction.

Many phrases have been used to express what are sometimes called anti-realist conceptions of truth: ‘verifiability’, ‘knowability’, ‘rational acceptability’, ‘warranted assertability’. In spite of their obvious differences, all four of these phrases have a common form; each is a cognitive attitude modified by ‘-ability’. They speak of the possibility of verification, knowledge, rational acceptance or warranted assertion. Schematically, it seems to be claimed that it is true that A if and only if it is possible that it is E'd that A, where ‘E’ is to be replaced by some cognitive verb and ‘A’ by any indicative sentence of the class to which the anti-realist conception is being claimed to apply. Since truth is redundant as a sentential operator, this boils down to the following thesis, where ‘p’ is a propositional variable and ‘M’ expresses the appropriate kind of possibility:

(*) also formalizes views such as Putnam's: ‘To claim a statement is true is to claim it could be justified’ [11, p. 56]. It is no doubt a crude model for anti-realism, but one has to start somewhere; by seeing how and why more sophisticated versions of anti-realism differ from (*) one should be able to understand them better too. Moreover, if an anti-realist rejects the equation of truth with, say, warranted assertibility, arguing that truth is rather to be identified with the possibility of getting into a position in which one's warrant to assert somehow cannot be overturned, the form of (*) is preserved, for truth is still being identified with the possibility of something.

Any finite support iteration of posets with precalibre ℵ1 which has the length of cofinahty greater than ω1 yields a model for the dual Borel conjecture in which the real line is covered by ℵ1 strong measure zero sets.

Recursive model theory involves the study of relationships between recursion theory and model theory. One direction this often takes is to study the effectiveness of various aspects of model theory. This paper examines such questions by examining some properties of recursive models; that is, models whose basic relations, functions, and constants are all uniformly recursive (and whose universe is the set of natural numbers). Somewhat more precisely:

Let be a model whose universe is N, and let (θ())i be an effective enumeration of all quantifier-free formulas of the language of . Then is recursive if {〈, i〉: satisfies (θ())i, in } is a recursive subset of N. (Here and throughout the paper, 〈 〉 denotes an effective pairing function, or an effective coding of sequences, as required.) Similarly, let (ϕ())i be an effective enumeration of all existential formulas of the language of . Then is existentially decidable if {〈, i〉: satisfies (ϕ())i in } is a recursive subset of N.

It is clear that if is recursive and is a model isomorphic to , then may lose many of the recursive properties of . In the simplest example, could easily fail to be a recursive model. But even if we require that be a recursive model, it could still fail to retain other recursive properties of . An example of the sort of property which can be studied in this vein is the following notion, introduced by Ash and Nerode in [2].

We show that every analytic filter is generated by a prefilter, every filter is generated by a prefilter, and if is a prefilter then the filter generated by it is also . The last result is unique for the Borel classes, as there is a -complete prefilter P such that the filter generated by it is -complete. Also, no complete coanalytic filter is generated by an analytic prefilter. The proofs use König's infinity lemma, a normal form theorem for monotone analytic sets, and Wadge reductions.

The family of readability toposes, of which the effective topos is the best known, was discovered by Martin Hyland in the late 1970's. Since then these toposes have been used for several purposes. The effective topos itself was originally intended as a category in which various recursion-theoretic or effective constructions would live as natural parts of the higher-order type structure. For example the hereditary effective operators become the higher types over N (Hyland [1982]), and effective domains become the countably-based domains in the topos (McCarty [1984], Rosolini [1986]). However, following the discovery by Moggi and Hyland that it contained nontrivial small complete categories, the effective topos has also been used to provide natural models of polymorphic type theories, up to and including the theory of constructions (Hyland [1987], Hyland, Robinson and Rosolini [1987], Scedrov [1987], Bainbridge et al. [1987]).

Over the years there have also been several different constructions of the topos. The original approach, as in Hyland [1982], was to construct the topos by first giving a notion of Pω-valued set. A Pω-valued set is a set X together with a function =x: X × X → Pω. The elements of X are to be thought of as codes, or as expressions denoting elements of some “real underlying” set in the topos. Given a pair (x,x′) of elements of X, the set =x (x,x′) (generally written ) is the set of codes of proofs that the element denoted by x is equal to the element denoted by x′.

Hereditarily finite sets are sets which are finite, whose members are finite, the members of whose members are finite, and so on. In ZF there are but countably many such sets; they constitute Vω. Were ZF to lose its axiom of regularity, however, one could not guarantee that the number of hereditarily finite sets would remain countable.

In Mostowski set theory, in which atomic sets are permissible, each atom, in isolation, would form a hereditarily finite collection. The number of hereditarily finite sets could be anything one should choose.

Even in a world that did not permit the free adjunction of arbitrary, meaningless atoms, the number of hereditarily finite sets could remain large. In Finsler set theory, it is shown as Theorem 22, below, that there are uncountably many hereditarily finite sets.

The reader who is interested in this paradoxical sounding fact can turn directly to §4 after grasping these introductory concepts. §3 is an exhaustive list of the smallest Finsler sets; it is hoped that this list will prove useful in checking future attempts to classify the finite Finsler sets.

Finsler set theory is not a firmly axiomatized theory. It is, at its present stage, a family of theories undergoing evolution. It permits the usual mathematical operations with sets. One can employ ordinal numbers, cardinal numbers, and the usual methods of Cantorian set theory freely. But there is a somewhat different interpretation attached to the concept “set” than one is used to in Zermelo-Fraenkel set theory, ZF.

κ-saturation [SL] is probably the single most useful property of nonstandard models of analysis. For some applications, however, stronger saturation hypotheses seem necessary. Henson formulated his elegant κ-isomorphism property (see [H1], and §2 below) to address this need. This property, though well-suited to certain situations (notably those arising in Banach space theory), is often difficult to apply in practice (see [SL, §7.7]).

In this paper I describe an alternative to κ-isomorphism which is much easier to use; in particular, a proof which assumes that the nonstandard model is fully saturated can usually be converted directly to one using this special model axiom.

Precise definitions of both these axioms appear in §2. In §3 I prove some simple properties of the special model axiom, one of which is that it is at least as strong as κ-isomorphism. In §§4, 5, and 6 the axiom is used to construct a few examples, many of which are pathological, or at the very least counterintuitive. (These examples are given primarily to illustrate use of the axiom; the only one of independent interest is Theorem 5.5.) In §7 some alternative axioms and open problems are discussed.

Many of the results in this paper grew out of discussion and correspondence with C. Ward Henson, to whom I am consequently most grateful.

Un prolongement de l'étude d'une théorie T, dans le langage , consiste à s'intéresser à la théorie T* des paires de modèles de T, c'est-à-dire les structures de la forme (K ⊊ L) où K ⊨ T, L ⊨ T, K ≺ L, dans le langage où E est un prédicat pour la sous-structure. Les propriétés de la théorie T ne se transmettent pas toujours à T*, particulièrement en ce qui concerne la complétude et la décidabilité. On trouve des illustrations de cas opposés dans les théories de corps:

—si T est la théorie des corps algébriquement clos de caractéristique fixée, T* est complète et décidable;

—si T est la théorie des corps réels clos, T est complète et décidable, mais T* est indécidable, et admet complétions différentes.

Nous allons nous intéresser ici aux paires de corps valués henseliens, et plus particulièrement au cas de caractéristique résiduelle nulle, de la forme (K ⊊ L, υ) où (K, υ) n'est pas nécessairement une sous-structure élémentaire de (L, υ). Ax, Kochen et Ershov ont montré que la théorie d'un corps valué henselien de caractéristique résiduelle nulle est entièrement déterminée par la théorie de son corps de restes et par la théorie de son groupe de valuation; par ailleurs, de résultats analogues existent pour certains corps de caractéristique résiduelle non nulle.

In this work we describe a new approach to the notions of relevance and paraconsistency. Unlike the works of Anderson and Belnap or da Costa (see [2], [8] and [7]) we shall mainly be guided in it by semantical intuitions. In the first two sections we introduce and investigate the algebraic structures that reflect those intuitions. The corresponding formal systems are briefly described in the third section (a more detailed treatment of these systems, including full proofs, will be given in another paper).

Our basic intuitive idea is that of “domains of discourse” or “relevance domains”. Classical logic, so we think, is valid in as much as sentences get values inside one domain; limitations on its use can be imposed only with respect to inferences in which more than one domain is involved. There are two basic binary relations over the collection of domains. One is relevance. It is reflexive and symmetric (but not necessarily transitive). Under a given interpretation two sentences are relevant to each other when their values are in relevant domains. Another basic relation between domains, no less important, is that of grading according to “degrees of reality”. The idea behind it is not new. Gentzen, for example, divided in [9] the world of mathematics into three grades, representing three “levels of reality”. The elementary theory of numbers has the highest degree or level of reality; set theory has the smallest degree and mathematical analysis occupies the intermediate level. In the theory of types, or in the accumulative von Neumann universe for set theory, we can find indication of a richer hierarchy.

We show that the structure (C, +, ·) has no proper non locally modular reducts which contain +. In other words, if X ⊂ Cn is constructible and not definable in the module structure (C, +, λa)a Є C (where λa denotes multiplication by a) then multiplication is definable in (C, +, X).

Recursion theory has been dominated by one example. The notion of a dominical category was introduced (see [2] and [3]) at least in part in the hope of subverting this dominance. The structures of number theory, freed from this original context, led to much of modern algebra with a consequent enrichment of number theory itself: it seemed not unreasonable to attempt to contribute, however modestly, to a similar development of recursion theory. Thus (in the loosest sort of analogy) recursion categories are intended to stand in relation to the class of partial recursive functions as rings do to the rational integers.

But if such a generalization is to serve its intended purpose, it ought to allow examples substantially different in spirit from the prototype. Recursion categories are, of course, the proper generalization of classical recursion theory. As a novice in this formidable field I am incapable of encompassing its full extent and must rely on the advice of others (I thank in particular R. DiPaola) in concluding that most of these earlier generalizations are not of this character. Indeed, the examples of recursion categories so far adduced (cf., in addition to the references above, [1] and [4]) are themselves closely tied to the classical one.

We attempt here to open the door to radically disparate examples by proving an existence theorem allowing the construction of recursion categories in a wide, and so far unexplored, variety of contexts very distant from that of the natural or ordinal numbers and their subsets, the locus of the traditional theory.

In order to do this, it has been necessary to introduce a number of unfamiliar notions—unfamiliar, that is, even in the context of the earlier discussion of dominical categories. This novelty is perhaps mitigated by the fact that, however unfamiliar, they cannot be said to be unusual, as the discussion later will show. We mention in particular those of a “formally free semigroup”, which retains the indexation function of a free semigroup, while giving up the characteristic universal property and that of “uniform generation”, which generalizes finite generation in the fashion assorted to our argument.