Kleene and Post [2] have shown that between each degree a and its completion a′ there are an infinity of mutually incomparable degrees of unsolvability, and that between a and its nth. completion a(n) there are an infinity of mutually incomparable degrees each incomparable with a′, …, a(n−1). They have left open the following questions: whether there exist complete degrees in similar profusion; whether indeed there exist incomparable complete degrees at all; and whether certain degrees, such as a(ω) ([2] p. 401), are complete. All these questions are answered affirmatively by the corollary of the present paper, which states that every degree greater than or equal to 0′ is complete. Since every complete degree is already known to be greater than or equal to 0′, it follows from the present paper that being greater than or equal to 0′ is both a necessary and a sufficient condition for completeness.

The brilliant work of Ax-Kochen [1], [2], [3] and Ersov [6], and later work by Kochen [7] have made clear very striking resemblances between real closed fields and p-adically closed fields, from the model-theoretical point of view. Cohen [5], from a standpoint less model-theoretic, also contributed much to this analogy.

In this paper we shall point out a feature of all the above treatments which obscures one important resemblance between real and p-adic fields. We shall outline a new treatment of the p-adic case (not far removed from the classical treatments cited above), and establish an new analogy between real closed and p-adically closed fields.

We want to describe the definable subsets of p-adically closed fields. Tarski [9] in his pioneering work described the first-order definable subsets of real closed fields. Namely, if K is a real-closed field and X is a subset of K first-order definable on K using parameters from K then X is a finite union of nonoverlapping intervals (open, closed, half-open, empty or all of K). In particular, if X is infinite, X has nonempty interior.

Now, there is an analogous question for p-adically closed fields. If K is p-adically closed, what are the definable subsets of K? To the best of our knowledge, this question has not been answered until now.

What is the difference between the two cases? Tarski's analysis rests on elimination of quantifiers for real closed fields. Elimination of quantifiers for p-adically closed fields has been achieved [3], but only when we take a cross-section π as part of our basic data. The problem is that in the presence of π it becomes very difficult to figure out what sort of set is definable by a quantifier free formula. We shall see later that use of the cross-section increases the class of definable sets.

We give a simple proof characterizing the complexity of Presburger arithmetic augmented with additional predicates. We show that Presburger arithmetic with additional predicates is complete. Adding one unary predicate is enough to get hardness, while adding more predicates (of any arity) does not make the complexity any worse.

This is an attempt to give a survey of recent results concerning trees. The article is an extended version of our talk in Oberwolfach (Schwarzwald) last May; the forests surrounding the Forschungsinstitut turned out to be a good inspiration.

A tree is a partially ordered set T = (T, ≤) such that for every x ∈ T, the set = {y ∈ T: y < x} is well-ordered. The order type of is called the order of x, o(x), and the length of T is sup {o(x) + 1: x ∈ T}; an α-tree (where α is an ordinal) is a tree of length α. The αth level of T is the set Uα of all elements of T whose order is α. T∣α is the union of all Uβ, β < α; its length is α. A tree (T2, ≤2) is called an extension of (T1, ≤1) if ≤1 = ≤2 ∩ (T1 × T1); T2 is on end-extension of (T1 if T1 = T2∣α for some α. A maximal linearly ordered subset of a tree T is called a branch of T; an α-branch is a branch of length α.

Let Pp, Pd, and N be the intuitionistic formal systems of prepositional calculus, predicate calculus, and elementary number theory, respectively.1 Consider the following six propositions.8

(1) ├A V B only if ├A or ├B.

(2) ├∋xA(x) only if ├Ã(t) for some formula Ã(x) congruent to A(x) and some term t free for x in Ã(x).

We present a possible computational content of the negative translation of classical analysis with the Axiom of (countable) Choice. Interestingly, this interpretation uses a refinement of the realizability semantics of the absurdity proposition, which is not interpreted as the empty type here. We also show how to compute witnesses from proofs in classical analysis of ∃-statements and how to extract algorithms from proofs of ∀∃-statements. Our interpretation seems computationally more direct than the one based on Gödel's Dialectica interpretation.

By a theory we shall always mean one of first order, having finitely many non-logical constants. Then for theories with identity (as a logical constant, the theory being closed under deduction in first-order logic with identity), and also likewise for theories without identity, one may distinguish the following three notions of axiomatizability. First, a theory may be recursively axiomatizable, or, as we shall say, simply, axiomatizable. Second, a theory may be finitely axiomatizable using additional predicates (f. a.+), in the syntactical sense introduced by Kleene [9]. Finally, the italicized phrase may also be interpreted semantically. The resulting notion will be called s. f. a.+. It is closely related to the modeltheoretic notion PC introduced by Tarski [16], or rather, more strictly speaking, to PC∩ACδ.

For arbitrary theories with or without identity, it is easily seen that s. f. a.+ implies f. a.+ and it is known that f. a.+ implies axiomatizability. Thus it is natural to ask under what conditions the converse implications hold, since then the notions concerned coincide and one can pass from one to the other.

Kleene [9] has shown: (1) For arbitrary theories without identity, axiomatizability implies f. a.+. It also follows from his work that : (2) For theories with identity which have only infinite models, axiomatizability implies f. a.+.

One way to construct a contraction operator for a theory (belief set) is to assign to it a base (belief base) and an operator of partial meet contraction for that base. Axiomatic characterizations are given of the theory contractions that are generated in this way by (various types of) partial meet base contractions.

In the first of her papers on functional calculi based on strict implication, Ruth Barcan Marcus takes as her starting point the Lewis systems S2 and S4, supplemented by one of the normal bases for quantification theory, and by one special axiom for the mixture, asserting that if possibly something φ's then something possibly φ's. In the symbolism of Łukasiewicz, which will be used here, this axiom is expressible as CMΣxφxΣxMφx. In the present note I propose to show that if S5 had been taken as a startingpoint rather than S2 or S4, this formula need not have been laid down as an axiom but could have been deduced as a theorem.

It has been shown by Gödel that a system equivalent to S5 may be obtained if we add to any complete basis for the classical propositional calculus a pair of symbols for ‘Necessarily’ and ‘Possibly,’ which here will be ‘L’ and ‘M’; the axioms

the rule

RL: If α is a thesis, so is Lα;

and the definition

Df. M: M = NLN.

Articles by two American mathematicians, E. V. Huntington and Oswald Veblen, are discussed as examples of a movement in foundational research in the period 1900–1930 called American postulate theory. This movement also included E. H. Moore, R. L. Moore, C. H. Langford, H. M. Sheffer, C. J. Keyser, and others. The articles discussed exemplify American postulate theorists' standards for axiomatizations of mathematical theories, and their investigations of such axiomatizations with respect to metatheoretic properties such as independence, completeness, and consistency.

In his 1936 paper, On the Concept of Logical Consequence, Tarski introduced the celebrated definition of logical consequence: “The sentenceσ follows logically from the sentences of the class Γ if and only if every model of the class Γ is also a model of the sentence σ.” [55, p. 417] This definition, Tarski said, is based on two very basic intuitions, “essential for the proper concept of consequence” [55, p. 415] and reflecting common linguistic usage: “Consider any class Γ of sentences and a sentence which follows from the sentences of this class. From an intuitive standpoint it can never happen that both the class Γ consists only of true sentences and the sentence σ is false. Moreover, … we are concerned here with the concept of logical, i.e., formal, consequence.” [55, p. 414] Tarski believed his definition of logical consequence captured the intuitive notion: “It seems to me that everyone who understands the content of the above definition must admit that it agrees quite well with common usage. … In particular, it can be proved, on the basis of this definition, that every consequence of true sentences must be true.” [55, p. 417] The formality of Tarskian consequences can also be proven. Tarski's definition of logical consequence had a key role in the development of the model-theoretic semantics of modern logic and has stayed at its center ever since.

Recently Lafont [6] showed the finite model property for the multiplicative additive fragment of linear logic (MALL) and for affine logic (LLW), i.e., linear logic with weakening. In this paper, we shall prove the finite model property for intuitionistic versions of those, i.e. intuitionistic MALL (which we call IMALL), and intuitionistic LLW (which we call ILLW). In addition, we shall show the finite model property for contractive linear logic (LLC), i.e., linear logic with contraction. and for its intuitionistic version (ILLC). The finite model property for related substructural logics also follow by our method. In particular, we shall show that the property holds for all of FL and GL−-systems except FLc and of Ono [11], that will settle the open problems stated in Ono [12].

Les synthèses nouvelles par le rapprochement de disciplines mathématiques différentes constituent des événements remarquables dans l'histoire des mathématiques. Une telle synthèse semble émerger actuellement du rapprochement de:

(1) La géométrie algébrique sous la forme élaborée par Grothendieck.

(2) La logique formelle.

Le point de contact s'est effectué aux environs de 1970 par W. Lawvere et M. Tierney et l'instrument de rapprochement a été la théorie des catégories, plus particulièrement la théorie des faisceaux. Depuis ce moment, une dialectique incessante imprime un mouvement dynamique à toute une série de recherches qui visent à rapprocher les méthodes suivantes:

(1) Mathématique intuitionniste.

(2) Forcing de Cohen et Robinson.

(3) Logique algébrique.

(4) Géométrie algébrique.

(5) Géométrie différentielle et analytique.

(6) Topologie algébrique: cohomologie, homotopie.

(7) Théorie de Galois.

Certains rapprochements sont dans un stade avancé, d'autres encore embryonnaires: (6) ↔ (3).

La structure centrale qui joue le rôle d'élément provocateur et unificateur est celle de topos. Avant d'être axiomatisée par Lawvere, celle-ci a été étudiée systématiquement par l'école de Grothendieck (voir [1]) et c'est dans le contexte de la géométrie algébrique qu'elle fit son apparition. Dans cet article nous utiliserons cependant la définition de Lawvere telle qu'améliorée par Mikkelsen [12] et Kock [8].

Le but de ce travail est de présenter une version (au sens de la logique formelle) du concept de topos et d'examiner brièvement les rapports entre la théorie des topos, la logique et les mathématiques. Cette version a déjà été exposée par l'un des auteurs lors du Séminaire de Mathématiques Supérieures de l'Université de Montréal, à l'été 1974. Depuis elle a fait l'objet d'une thèse où elle a été améliorée et sa cohérence vérifiée [2]. Des systèmes différents ont été proposés simultanément par Fourman [4] et Coste [3].

There are not many global results on modal logics. One of these is the following theorem by Sahlqvist on completeness and correspondence for a wide class of modal formulae (including many well known logics, e.g. D, T, B, S4, K4, S5, …) (see [S]).

Sahlqvist's Theorem. Let A be any modal formula which is equivalent to a conjunction of formulae of the form □m(A1 → A2), where m ≥ 0, A2 is positive and A1 is obtained from propositional variables and their negations applying ∧, ∨, ♢, and □ in such a way that no positive occurrence of a variable is in a subformula of the form B1 ∨ B2 or ♢ B1 within the scope of some □. Then A corresponds effectively to a first order formula, and L + A is canonical whenever Lis a canonical logic.

A formula A satisfying the above conditions is henceforth called a Sahlqvist formula. Unfortunately, till now, the only complete proof was the original proof of Sahlqvist (a proof of the correspondence half has also been given by van Benthem [vB]). It is so complicated and long that even in an advanced textbook of modal logic [HC] it has not found a place. Here, by considering general frames as topological spaces, an attitude which we developed in [TD], we give a proof of Sahlqvist's theorem simplified to such an extent that one can easily grasp the key idea on which it is based and apply the resulting algorithm to specific modal formulae in a straightforward manner, suitable even for implementation on a personal computer. This key idea also improves on previous preliminary work in the same direction (see [S1], [S2]).

We are concerned here with recursive function theory analogs of certain problems in chromatic graph theory. The motivating question for our work is: Does there exist a recursive (countably infinite) planar graph with no recursive 4-coloring? We obtain the following results: There is a 3-colorable, recursive planar graph which, for all k, has no recursive k-coloring; every decidable graph of genus p ≥ 0 has a recursive 2(x(p) − 1)-coloring, where x(p) is the least number of colors which will suffice to color any graph of genus p; for every k ≥ 3 there is a k-colorable, decidable graph with no recursive k-coloring, and if k = 3 or if k = 4 and the 4-color conjecture fails the graph is planar; there are degree preserving correspondences between k-colorings of graphs and paths through special types of trees which yield information about the degrees of unsolvability of k-colorings of graphs.

We investigate logical consequence in temporal logics in terms of logical consecutions, i.e., inference rules. First, we discuss the question: what does it mean for a logical consecution to be ‘correct’ in a propositional logic. We consider both valid and admissible consecutions in linear temporal logics and discuss the distinction between these two notions. The linear temporal logic LDTL, consisting of all formulas valid in the frame 〈L ≤, ≥〉 of all integer numbers, is the prime object of our investigation. We describe consecutions admissible in LDTL in a semantic way—via consecutions valid in special temporal Kripke/Hintikka models. Then we state that any temporal inference rule has a reduced normal form which is given in terms of uniform formulas of temporal degree 1. Using these facts and enhanced semantic techniques we construct an algorithm, which recognizes consecutions admissible in LDTL. Also, we note that using the same technique it follows that the linear temporal logic L(N) of all natural numbers is also decidable w.r.t. inference rules. So, we prove that both logics LDTL and L(N) are decidable w.r.t. admissible consecutions. In particular, as a consequence, they both are decidable (known fact), and the given deciding algorithms are explicit.

In this paper we continue our study, begun in [5], of the connection between ultraproducts and saturated structures. If D is an ultrafilter over a set I, and is a structure (i.e., a model for a first order predicate logic ℒ), the ultrapower of modulo D is denoted by D-prod. The ultrapower is important because it is a method of constructing structures which are elementarily equivalent to a given structure (see Frayne-Morel-Scott [3]). Our ultimate aim is to find out what kinds of structure are ultrapowers of . We made a beginning in [5] by proving that, assuming the generalized continuum hypothesis (GCH), for each cardinal α there is an ultrafilter D over a set of power α such that for all structures , D-prod is α+-saturated.

A relational structure of cardinality ℵ0 is called homogeneous by Fraissé [1] if each isomorphism between finite substructures of can be extended to an automorphism of . In §1 of this paper it is shown that there are isomorphism types of such structures for the first order language L0 with a single (binary) relation symbol, answering a question raised by Fraissé. In fact, as is shown in §2, a family of nonisomorphic homogeneous structures for L0 can be constructed, each member of which satisfies the following conditions (where U is the homogeneous, ℵ0-universal graph, the structure of which is considered in [4]):

(i) The relation R of is asymmetric (R ∩ R−1 = ∅);

(ii) If A is the domain of and S is the symmetric relation R ∪ R−1, then (A, S) is isomorphic to U. That is, each may be regarded as the result of assigning a unique direction to each edge of the graph U.

Let T0 be the first order theory of all homogeneous structures for L0 which have cardinality ℵ0. In §3 (which can be read independently of §2) it is shown that T0 has complete extensions (in L0), each of which is ℵ0-categorical. Moreover, among the complete extensions of T0 are theories of arbitrary (preassigned) degree of unsolvability. In particular, there exists an undecidable, ℵ0-categorieal theory in L0, which answers a question raised by Grzegorczyk [2], [3].

It follows from Theorem 6 of [3] that there are ℵ0-categorical theories of partial orderings which have arbitrarily high degrees of unsolvability. This is in sharp contrast to the situation for linear orderings, which were the motivation for Fraissé's early work. Indeed, as is shown in [10], every ℵ0-categorical theory of a linear ordering is finitely axiomatizable. (W. Glassmire [12] has independently shown the existence of theories in L0 which are all ℵ0-categorical, and C. Ash [13] has independently shown that such theories exist with arbitrary degree of unsolvability.)

The existence of an ω2-Souslin tree will be proved (Theorem 2.2 or §3) from the Generalized Continuum Hypothesis (GCH) plus Jensen's combinatorial principle □ω1. Thus, it follows from Jensen's 1.4(2) that the consistency of the formal theory T given by ZFC + GCH + “ω2-Souslin Hypothesis” implies the consistency of ZFC + “there exists a Mahlo cardinal.” So one does not hope to prove the consistency of this T relative to the consistency of ZFC + “there is an inaccessible cardinal, hence there are transitive models of ZFC.”

Silver [5, Theorem 5.8] has shown that the consistency of ZFC + “there is a weakly compact cardinal” implies the consistency of ZFC + not GCH + “there is no ω2-Aronszajn tree, hence no ω2-Souslin tree”; this is one reason why we deal with GCH here. Jensen has shown that the consistency of ZFC implies the consistency of ZFC +GCH + “ω1-Souslin Hypothesis.”

In the preliminary §1, we state some definitions and known results about trees and some of Jensen's combinatorial principles, including □ and ◇*(E).

Our main Lemma 2.1 states (a fortiori) that GCH implies ◇* at ω-cofinal elements of ω2 (i.e., in our notation, ◇*(E(ω) ∩ ω2)). From Lemma 2.1 and the known facts of §1, it is proved (2.5) that if □ k , the cofinality cf(k)> ω, and GCH, then there is a k +-Souslin tree. For k = ω1, this implies the result mentioned above for ω2-Souslin trees.

This paper deals with the notion of direct product in the theory of decision problems.

Elementary mathematical theories are always concerned with certain functions defined in a set I (called the universe of discourse of the theory) and certain relations with the common domain I. The notions of functions and relations are known to be reducible to each other. To avoid duplication of definitions and proofs we shall eliminate the former notion in favor of the latter and consider only theories in which all the primitive terms are of the type of relations (with an arbitrary number of arguments).

It is easy to define for relations the notion of a direct product in the way which is usual in abstract algebra. We are led to this definition in a very natural way when we reflect that relations are but a particular case of functions, and the direct product of an arbitrary number of functions is defined in algebra.

A relation which is representable as a product of an arbitrary number of pairwise identical relations is called the power-relation, and the relations which occur as factors are called the base-relations.

The content of the present paper can now be characterized more precisely as follows.

We shall discuss a theory of which the primitive notions are representable as powers of certain base-relations, and shall try to reduce all the problems concerning this theory (in particular the decision problem) to problems concerning the theory of the base-relations. It will be seen that this reduction is in fact possible, and that several particular cases of the decision problem, the solutions of which are known from the literature, can be included in the general scheme established in the present paper.