Several extensions of the basic modal language are characterized in terms of interpolation. Our main results are of the following form: Language L′ is the least expressive extension of L with interpolation. For instance, let ℳ(D) be the extension of the basic modal language with a difference operator [7], First-order logic is the least expressive extension of ℳ(D) with interpolation. These characterizations are subsequently used to derive new results about hybrid logic, relation algebra and the guarded fragment.

Many known tools for proving expressibility bounds for first-ordér logic are based on one of several locality properties. In this paper we characterize the relationship between those notions of locality. We note that Gaifman's locality theorem gives rise to two notions: one deals with sentences and one with open formulae. We prove that the former implies Hanf's notion of locality, which in turn implies Gaifman's locality for open formulae. Each of these implies the bounded degree property, which is one of the easiest tools for proving expressibility bounds. These results apply beyond the first-order case. We use them to derive expressibility bounds for first-order logic with unary quantifiers and counting. We also characterize the notions of locality on structures of small degree.

To show that a formula A is not provable in propositional classical logic, it suffices to exhibit a finite boolean model which does not satisfy A. A similar property holds in the intuitionistic case, with Kripke models instead of boolean models (see for instance [11]). One says that the propositional classical logic and the propositional intuitionistic logic satisfy a finite model property. In particular, they are decidable: there is a semi-algorithm for provability (proof search) and a semi-algorithm for non provability (model search). For that reason, a logic which is undecidable, such as first order logic, cannot satisfy a finite model property.

The case of linear logic is more complicated. The full propositional fragment LL has a complete semantics in terms of phase spaces [2, 3], but it is undecidable [9]. The multiplicative additive fragment MALL is decidable, in fact PSPACE-complete [9], but the decidability of the multiplicative exponential fragment MELL is still an open problem. For affine logic, that is, linear logic with weakening, the situation is somewhat better: the full propositional fragment LLW is decidable [5].

Here, we show that the finite phase semantics is complete for MALL and for LLW, but not for MELL. In particular, this gives a new proof of the decidability of LLW. The noncommutative case is mentioned, but not handled in detail.

(1.1) A well-known example of a theory with built-in Skolem functions is (first-order) Peano arithmetic (or rather a certain definitional extension of it). See [C-K, pp. 143, 162] for the notion of a theory with built-in Skolem functions, and for a treatment of the example just mentioned. This property of Peano arithmetic obviously comes from the fact that in each nonempty definable subset of a model we can definably choose an element, namely, its least member.

(1.2) Consider now a real closed field R and a nonempty subset D of R which is definable (with parameters) in R. Again we can definably choose an element of D, as follows: D is a union of finitely many singletons and intervals (a, b) where – ∞ ≤ a < b ≤ + ∞; if D has a least element we choose that element; if not, D contains an interval (a, b) for which a ∈ R ∪ { − ∞}is minimal; for this a we choose b ∈ R ∪ {∞} maximal such that (a, b) ⊂ D. Four cases have to be distinguished:

(i) a = − ∞ and b = + ∞; then we choose 0;

(ii) a = − ∞ and b ∈ R; then we choose b − 1;

(iii) a ∈ R and b ∈ = + ∞; then we choose a + 1;

(iv) a ∈ R and b ∈ R; then we choose the midpoint (a + b)/2.

It follows as in the case of Peano arithmetic that the theory RCF of real closed fields has a definitional extension with built-in Skolem functions.

The notions of recursively saturated and resplendent models grew out of the study of admissible sets with urelements and admissible fragments of L ω1ω, but, when applied to ordinary first order model theory, give us new tools for research and exposition. We will discuss their history in §3.

The notion of saturated model has proven to be important in model theory. Its most important property for applications is that if , are saturated and of the same cardinality then = iff ≅ . See, e.g., Chang-Keisler [3]. The main drawback is that saturated models exist only under unusual assumptions of set theory. For example, if 2κ = κ+ then every theory T of L has a saturated model of power κ+. (Similarly, if κ is strongly inaccessible, then every T has a saturated model of power κ.) On the other hand, a theory T like Peano arithmetic, with types, cannot have a saturated model in any power κ with ω ≤ κ ≤ .

One method for circumventing these problems of existence (or rather non-existence) is the use of “special” models (cf. [3]). If κ = Σλ<κ2λ, κ < ω, then every theory T of L has a special model of power κ. Such cardinals are large and, themselves, rather special. There are definite aesthetic objections to the use of these large, singular models to prove results about first order logic.

This paper is a contribution to the following natural problem in complexity theory:

(*) Is there a complexity theory for isomorphism types of recursive countable relational structures? I.e. given a recursive relational structure ℛ over the set N of nonnegative integers, is there a nontrivial lower bound for the time-space complexity of recursive structures isomorphic (resp. recursively isomorphic) to ℛ?

For unary recursive relations R, the answer is trivially negative: either R is finite or coinfinite or 〈N, R〉 is recursively isomorphic to 〈N, {x ϵ N: x is even}〉.

The general problem for relations with arity 2 (or greater) is open.

Related to this problem, a classical result (going back to S. C. Kleene [4], 1955) states that every recursive ordinal is in fact primitive recursive.

In [3] Patrick Dehornoy, using methods relevant to computer science, improves this result, showing that every recursive ordinal can be represented by a recursive total ordering over N which has linear deterministic time complexity relative to the binary representation of integers. As he notices, his proof applies to every recursive total order type α such that the isomorphism type of α is not changed if points are replaced by arbitrary finite nonempty subsets of consecutive points.

In this paper we extend Dehornoy's result to all recursive total orderings over N and get minimal complexity for both time and space simultaneously.

Let κ denote a regular uncountable cardinal and NS the normal ideal of nonstationary subsets of κ. Our results concern the well-known open question whether NS fails to be κ+-saturated, i.e., are there κ+ stationary subsets of κ with pairwise intersections nonstationary? Our first observation is:

Theorem. NS isκ+-saturated iff for every normal ideal J on κ there is a stationary set A ⊆ κsuch that J = NS∣A = {X ⊆ κ: X ∩ A ∈ NS}.

Turning our attention to large cardinals, we extend the usual (weak) Mahlo hierarchy to define “greatly Mahlo” cardinals and obtain the following:

Theorem. If κ is greatly Mahlo then NS is notκ+-saturated.

Theorem. If κ is ordinal Π11-indescribable (e.g., weakly compact), ethereal (e.g., subtle), or carries aκ-saturated ideal, thenκis greatly Mahlo. Moreover, there is a stationary set of greatly Mahlo cardinals below any ordinal Π11-indescribable cardinal.

These methods apply to other normal ideals as well; e.g., the subtle ideal on an ineffable cardinal κ is not κ+-saturated.

Let T be a complete o-minimal extension of the theory of real closed fields. We characterize the convex hulls of elementary substructures of models of T and show that the residue field of such a convex hull has a natural expansion to a model of T. We give a quantifier elimination relative to T for the theory of pairs (ℛ, V) where ℛ ⊨ T and V ≠ ℛ is the convex hull of an elementary substructure of ℛ. We deduce that the theory of such pairs is complete and weakly o-minimal. We also give a quantifier elimination relative to T for the theory of pairs with ℛ a model of T and a proper elementary substructure that is Dedekind complete in ℛ. We deduce that the theory of such “tame” pairs is complete.

A theory formulated in a countable predicate calculus can have at most nonisomorphic countable models. It has been conjected (e.g., in [4]) that if it has an uncountable number of such models then it has exactly such. Of course, this would follow immediately if one assumed the continuum hypothesis.

In this paper we show that if a theory has more than ℵ1 (i.e., at least ℵ2) isomorphism types of countable models then it has exactly . Our results generalize immediately to theories in Lω1ω and even to pseudo-axiomatic classes in Lω1ω . In this last case, a result of H. Friedman shows that it is the best possible result.

For sets of natural numbers A and B, A is enumeration reducible to B if there is some effective algorithm which when given any enumeration of B will produce an enumeration of A. Gutteridge [5] has shown that in the upper semilattice of the enumeration degrees there are no minimal degrees (see Cooper [3]), and in this paper we study those pairs of degrees with gib 0. Case [1] constructed a minimal pair. This minimal pair construction can be relativised to any gib, and following a suggestion of Jockusch we can also fix one of the degrees and still construct the pair. These methods yield an easier proof of Case's exact pair theorem for countable ideals. 0″ is an upper bound for the minimal pair constructed in §1, and in §2 we improve this bound to any Σ2-high Δ2 degree. In contrast to this we show that every low degree c bounds a degree a which is not in any minimal pair bounded by c. The structure of the co-r.e. e-degrees is isomorphic to that of the r.e. Turing degrees, and Gutteridge has constructed co-r.e. degrees which form a minimal pair in the e-degrees. In §3 we show that if a, b is any minimal pair of co-r.e. degrees such that a is low then a, b is a minimal pair in the e-degrees (and so Gutteridge's result follows). As a corollary of this we can embed any countable distributive lattice and the two nondistributive five-element lattices in the e-degrees below 0′. However the lowness assumption is necessary, as we also prove that there is a minimal pair of (high) r.e. degrees which is not a minimal pair in the e-degrees (under the isomorphism). In §4 we present more concise proofs of some unpublished work of Lagemann on bounding incomparable pairs and embedding partial orderings.

As usual, {Wi}i ∈ ω is the standard listing of the recursively enumerable sets, Du is the finite set with canonical index u and {‹ m, n ›}m, n ∈ ω is a recursive, one-to-one coding of the pairs of numbers onto the numbers. Capital italic letters will be variables over sets of natural numbers, and lower case boldface letters from the beginning of the alphabet will vary over degrees.

We deal here with two modal logics, GL and Grz, that are known to have interesting arithmetical interpretations connected with the notion of provability. GL is the extensiom of K (or K4) by the schema □(□ A → A) → □ A, and Grz is the extension of S4 by □(□(A → □A) →A) → □A. GL is also known to be sound and complete with respect to the class of all Kripke models that are transitive, irreflexive and well founded. Grz bears the same relation to the corresponding reflexive models. We refer the reader to [1] for a full exposition of the subject. (See also [4], [2], [6].)

In §I we develop a sequential calculus for both GL and Grz and give a semantical proof that both systems admit cut-elimination. (Incidentally, this provides an easy proof of the semantical completeness of the two systems.) With respect to GL this yields a correction of an error in [2].

In §II we show that cut-elimination fails for QGL (the extension of GL to a language with quantifiers). We further show that, despite this failure, QGL still has some of GL's interesting properties (e.g., the disjunction property). We also show, using fixed-point techniques, that similar properties obtain if we take as semantics for QGL the arithmetical interpretation extended in the obvious way.

We want to thank Professor H. Gaifman for his help while working on the subject.

This paper is an attempt to explain as non-technically as possible the principles and devices used in the various proofs of Gödel's Theorems and Church's Theorem.

Roman numerals in references shall refer to the papers in the bibliography. In the statements of Gödel's Theorems and Church's Theorem, we will employ the phrase “for suitable L.” The hidden assumptions which we denote by this phrase have never been put down explicitly in a form intelligible to the average reader. The necessity for thus formulating them has commonly been avoided by proving the theorems for special logics and then remarking that the proofs can be extended to other logics. Hence the conditions necessary for the proofs of Gödel's Theorems and Church's Theorem are at present very indefinite as far as the average reader is concerned. To partly clarify this situation, we will now mention the more prominent of these assumptions.

I. In any proof of Gödel's Theorems or Church's Theorem, two logics are concerned. One serves as the “logic of ordinary discourse” in which the proof is carried out, and the other is a formal logic, L, about which the theorem is proved. The first logic may or may not be formal. However L must be formal. Among other things, this implies that the propositions of L are formulas built according to certain rules of structure.

The text of this article was done together with Gödel in 1976 to 1977 and was approved by him at that time. The footnotes and section headings have been added much later.

Gödel was born on April 28, 1906 at Brno (or Brünn in German), Czechoslovakia (at that time part of the Austro-Hungarian Monarchy). After completing secondary school there, he went, in 1924, to Vienna to study physics at the University. His interest in precision led him from physics to mathematics and to mathematical logic. He enjoyed much the lectures by Furtwangler on number theory and developed an interest in this subject which was, for example, relevant to his application of the Chinese remainder theorem in expressing primitive recursive functions in terms of addition and multiplication. In 1926 he transferred to mathematics and coincidentally became a member of the M. Schlick circle. However, he has never been a positivist, but accepted only some of their theses even at that time. Later on, he moved further and further away from them. He completed his formal studies at the University before the summer of 1929. He also attended during this period philosophical lectures by Heinrich Gomperz whose father was famous in Greek philosophy.

At about this time he read the first edition of Hilbert-Ackermann (1928) in which the completeness of the (restricted) predicate calculus was formulated and posed as an open problem. Gödel settled this problem and wrote up the result as his doctoral dissertation which was finished and approved in the autumn of 1929. The degree was granted on February 6, 1930. A somewhat revised version of the dissertation was published in 1930 in the Monatshefte.

There are well-known theorems in mathematical logic that indicate rather profound differences between the logic of first-order languages and the logic of second-order languages. In the first-order case, for example, there is Gödel's completeness theorem: every consistent set of sentences (vis-à-vis a standard axiomatization) has a model. As a corollary, first-order logic is compact: if a set of formulas is not satisfiable, then it has a finite subset which also is not satisfiable. The downward Löwenheim-Skolem theorem is that every set of satisfiable first-order sentences has a model whose cardinality is at most countable (or the cardinality of the set of sentences, whichever is greater), and the upward Löwenheim-Skolem theorem is that if a set of first-order sentences has, for each natural number n, a model whose cardinality is at least n, then it has, for each infinite cardinal κ (greater than or equal to the cardinality of the set of sentences), a model of cardinality κ. It follows, of course, that no set of first-order sentences that has an infinite model can be categorical. Second-order logic, on the other hand, is inherently incomplete in the sense that no recursive, sound axiomatization of it is complete. It is not compact, and there are many well-known categorical sets of second-order sentences (with infinite models). Thus, there are no straightforward analogues to the Löwenheim-Skolem theorems for second-order languages and logic.

There has been some controversy in recent years as to whether “second-order logic” should be considered a part of logic, but this boundary issue does not concern me directly, at least not here.

In this paper we formulate a notion similar to o-minimality but appropriate for the p-adics. The paper is in a sense a sequel to [11] and [5]. In [11] a notion of minimality was formulated, as follows. Suppose that L, L+ are first-order languages and + is an L+-structure whose reduct to L is . Then + is said to be -minimal if, for every N+ elementarily equivalent to +, every parameterdefinable subset of its domain N+ is definable with parameters by a quantifier-free L-formula. Observe that if L has a single binary relation which in is interpreted by a total order on M, then we have just the notion of strong o-minimality, from [13]; and by a theorem from [6], strong o-minimality is equivalent to o-minimality. If L has no relations, functions, or constants (other than equality) then the notion is just strong minimality.

In [11], -minimality is investigated for a number of structures . In particular, the C-relation of [1] was considered, in place of the total order in the definition of strong o-minimality. The C-relation is essentially the ternary relation which naturally holds on the maximal chains of a sufficiently nice tree; see [1], [11] or [5] for more detail, and for axioms. Much of the motivation came from the observation that a C-relation on a field F which is preserved by the affine group AGL(1,F) (consisting of permutations (a,b) : x ↦ ax + b, where a ∈ F \ {0} and b ∈ F) is the same as a non-trivial valuation: to get a C-relation from a valuation ν, put C(x;y,z) if and only if ν(y − x) < ν(y − z).

This paper is a continuation of Zakharyaschev [25], where the following basic results on modal logics with transitive frames were obtained:

• With every finite rooted transitive frame and every set of antichains (which were called closed domains) in two formulas α (, , ⊥) and α(, ) were associated. We called them the canonical and negation free canonical formulas, respectively, and proved the Refutability Criterion characterizing the constitution of their refutation general frames in terms of subreduction (alias partial p-morphism), the cofinality condition and the closed domain condition.

• We proved also the Completeness Theorem for the canonical formulas providing us with an algorithm which, given a modal formula φ, returns canonical formulas α(i, i), ⊥), for i = 1,…, n, such that

if φ is negation free then the algorithm instead of α(i, i, ⊥) can use the negation free canonical formulas α(i, i). Thus, every normal modal logic containing K4 can be axiomatized by a set of canonical formulas.

In this Part we apply the apparatus of the canonical formulas for establishing a number of results on the decidability, finite model property, elementarity and some other properties of modal logics within the field of K4.

Our attention will be focused on the class of logics which can be axiomatized by canonical formulas without closed domains, i.e., on the logics of the form

Adapting the terminology of Fine [11], we call them the cofinal subframe logics and denote this class by . As was shown in Part I, almost all standard modal logics are in .

The Cantor-Bendixson theorem says: For every closed set , ∣∣ ≤ ω0 ∨ ⊇ perfect (and therefore is countable or has the power of the continuum). W. H. Young proved the alternative for Gδ-sets, and Hausdorff extended it to Souslin-sets. Cantor used his ordinals to prove the theorem (I like to think he invented them for this purpose). In Hausdorff's Mengenlehre ordinals do not officially enter in either of the three proofs. You should try to put them back. It is very important never to hide away ω1 when it actually is there, and it is there when the continuum problem is the subject.

In Davis [6] you find that Cantor's alternative is equivalent to another alternative: (I wins ) ∨ (J wins ). Here means a lopsided game in which one of the players makes long moves on the game tree. So, the classical theorems can be restated as determinacy results for lopsided games, and now I make this observation: The original CB-proof “actually presents” a winning strategy. The HD-proofs do no such thing; all you know at the end is existence of a winning strategy (and Davis' remark is needed to gain this knowledge).

You understand now why I like CB-proofs, particularly for determinacy of games. They do exist also for games in which both players make short moves. Many years ago I tried to publish such a proof for determinacy of Fσ-games. The referee said it was not worth the trouble. I say you should remake this proof (it is a special case of the one presented in this paper), because it is the ideal of a determinacy proof.

We prove independence results concerning the number of nonisomorphic models (using the S-chain condition and S-properness) and the consistency of “ there is a universal linear order of power ℵ1”. Most of these results were announced in [Sh 4], [Sh 5].

In subsequent papers we shall prove an analog f MA for forcing which does not destroy stationary subsets of ω1 investigate -properness for various filters and prove the consistency with G.C.H. of an axiom implying SH (for ℵ1), and connected results.

For the formulation of the remaining axioms we need the notions of a function and of a one-to-one correspondence.

We define a function to be a class of pairs in which different elements always have different first members; or, in other words, a class F of pairs such that, to every element a of its domain there is a unique element b of its converse domain determined by the condition 〈a, b〉ηF. We shall call the set b so determined the value of F for a, and denote it (following the mathematical usage) by F(a).

A set which represents a function—i.e., a set of pairs in which different elements always have different first members—will be called a functional set.

If b is the value of the function F for a, we shall say that F assigns the set b to the set a; and if a functional set f represents F, we shall say also that f assigns the set b to the set a.

A class of pairs will be called a one-to-one correspondence if both it and its converse class are functions. We shall say that there exists a one-to-one correspondence between the classes A and B (or of A to B) if A and B are domain and converse domain of a one-to-one correspondence. Likewise we shall say that there exists a one-to-one correspondence between the sets a and b (or of a to b) if a and b respectively represent the domain and the converse domain of a one-to-one correspondence. In the same fashion we speak of a one-to-one correspondence between a class and a set, or a set and a class.