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.

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 .

Based on the relevant logic R, the system R# was proposed as a relevant Peano arithmetic. R# has many nice properties: the most conspicuous theorems of classical Peano arithmetic PA are readily provable therein; it is readily and effectively shown to be nontrivial; it incorporates both intuitionist and classical proof methods. But it is shown here that R# is properly weaker than PA, in the sense that there is a strictly positive theorem QRF of PA which is unprovable in R#. The reason is interesting: if PA is slightly weakened to a subtheory P+, it admits the complex ring C as a model; thus QRF is chosen to be a theorem of PA but false in C. Inasmuch as all strictly positive theorems of R# are already theorems of P+, this nonconservativity result shows that QRF is also a nontheorem of R#. As a consequence, Ackermann's rule γ is inadmissible in R#. Accordingly, an extension of R# which retains its good features is desired. The system R##, got by adding an omega-rule, is such an extension. Central question: is there an effectively axiomatizable system intermediate between R# and R#, which does formalize arithmetic on relevant principles, but also admits γ in a natural way?

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 a paper J. Łukasiewicz and A. Tarski study the systems arising out of the implication function C (x, y) = min(1, 1 – x + y) and the negation function Nx = 1 – x, where x, y are real numbers between 0 and 1 inclusive. Let us then writeСxy = min(1, 1 – x + y) and Nx = 1 – x. (1)

In this note we shall consider another implication function, namelyС′xy = ССNxyy, (2)

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.

This paper deals with forcing in arithmetic (as first introduced by Feferman [2]) and its connections with recursive function theory. We define for each n ≥ 1 the class of weakly n-generic sets. We prove that these classes merge with the classes of n-generic sets to form the hierarchy suggested by the terminology. Our notation is the same as that of Jockusch [5].

We study the I-ultrafilters on ω, where I is a a collection of subsets of a set X, usually ℝ or ω1. The I-ultrafilters usually contain the P-points, often as a small proper subset. We study relations between I-ultrafilters for various I, and closure of I-ultrafilters under ultrafilter sums. We consider, but do not settle, the question whether I-ultrafilters always exist.

We prove a categoricity transfer theorem for tame abstract elementary classes.

Suppose that K is a χ-tame abstract elementary class and satisfies the amalgamation and joint embedding properties and has arbitrarily large models. Let λ ≥ Max{χ, LS(K+}. If K is categorical in λ and λ+, then K is categorical in λ++.

Combining this theorem with some results from [37]. we derive a form of Shelah's Categoricity Conjecture for tame abstract elementary classes:

Suppose K is χ-tame abstract elementary class satisfying the amalgamation and joint embedding properties. Let μ0 ≔ Hanf(K). Ifand K is categorical in somethen K is categorical in μ for all μ .

One of the most significant by-products of the study of admissible sets with urelements is the emphasis it has given to recursively saturated models. As suggested in [Schlipf, 1977], countable recursively saturated models (for finite languages) possess many of the desirable properties of saturated and special models. The notion of resplendency was introduced to isolate some of these desirable properties. In §§1 and 2 of this paper we study these parallels, showing how they can be exploited to give new proofs of some traditional model theoretic theorems. This yields both pedagogical and philosophical advantages: pedagogical since countable recursively saturated models are easier to build and manipulate than saturated and special models; philosophical since it shows that uncountable models — which the downward Lowenheim–Skolem theorem tells us are in some sense not basic in the study of countable theories — are not needed in model theoretic proofs of these theorems. In §3 we apply our local results to get results about resplendent models of ZF set theory and PA (Peano arithmetic). In §4 we shall examine certain analogous results for admissible languages, most similar to, and seemingly generally slightly weaker than, already known results. (The Chang–Makkai sort of result, however, is new.)

Although this paper is an outgrowth of work with admissible sets with urelements, I have tried to keep it as accessible as possible to those with a background only in finitary model theory. Thus §§1,2, and 3 should not involve any work with admissible sets. §4, however, is concerned with some admissible analogues to results in §2 and necessarily uses certain technical results of §11 5 of [Schlipf, 1977].

We characterise explicitly the decidable predicates on integers of Infinite Time Turing machines, in terms of admissibility theory and the constructible hierarchy. We do this by pinning down ζ, the least ordinal not the length of any eventual output of an Infinite Time Turing machine (halting or otherwise); using this the Infinite Time Turing Degrees are considered, and it is shown how the jump operator coincides with the production of mastercodes for the constructible hierarchy; further that the natural ordinals associated with the jump operator satisfy a Spector criterion, and correspond to the Lζ-stables. It also implies that the machines devised are “Σ2 Complete” amongst all such other possible machines. It is shown that least upper bounds of an “eventual jump” hierarchy exist on an initial segment.

We give characterizations for the (in ZFC unprovable) sentences “Every -set is measurable” and “Every -set is measurable” for various notions of measurability derived from well-known forcing partial orderings.

The main result of this paper is a probabilistic construction of finite rigid structures. It yields a finitely axiomatizable class of finite rigid structures where no formula with counting quantifiers defines a linear order.

Recent work in natural language semantics leads to some new observations on generalized quantifiers. In §1 we show that English quantifiers of type 〈1, 1〉 are booleanly generated by their generalized universal and generalized existential members. These two classes also constitute the sortally reducible members of this type.

Section 2 presents our main result — the Generalized Prefix Theorem (GPT). This theorem characterizes the conditions under which formulas of the form (Q1x1…QnxnRx1…xn and q1x1…qnxnRx1…xn are logically equivalent for arbitrary generalized quantifiers Qi, qi. GPT generalizes, perhaps in an unexpectedly strong form, the Linear Prefix Theorem (appropriately modified) of Keisler & Walkoe (1973).

In this paper we discuss several generalization of theorems from stability theory to simple theories. Cherlin and Hrushovski, in [2] develop a substitute for canonical bases in finite rank, ω-categorical supersimple theories. Motivated by methods there, we prove the existence of canonical bases (in a suitable sense) for types in any simple theory. This is done in Section 2. In general these canonical bases will (as far as we know) exist only as “hyperimaginaries”, namely objects of the form a/E where a is a possibly infinite tuple and E a type-definable equivalence relation. (In the supersimple, ω-categorical case, these reduce to ordinary imaginaries.) So in Section 1 we develop the general theory of hyperimaginaries and show how first order model theory (including the theory of forking) generalises to hyperimaginaries. We go on, in Section 3 to show the existence and ubiquity of regular types in supersimple theories, ω-categorical simple structures and modularity is discussed in Section 4. It is also shown here how the general machinery of simplicity simplifies some of the general theory of smoothly approximable (or Lie-coordinatizable) structures from [2].

Throughout this paper we will work in a large, saturated model M of a complete theory T. All types, sets and sequences will have size smaller than the size of M. We will assume that the reader is familiar with the basics of forking in simple theories as laid out in [4] and [6]. For basic stability-theoretic results concerning regular types, orthogonality etc., see [1] or [9].

The Gödel class with identity (GCI) is the class of closed, prenex quantificational formulas whose prefixes have the form ∀∀∃ … ∃ and whose matrices contain arbitrary predicate letters and the identity sign “ = ”, but do not contain function signs or individual constants. The ∀∀∃ … ∃ class without identity was shown solvable over fifty years ago ([4], [12], [17]); slightly later, that class was shown to possess the stronger property of finite controllability ([5], [18]). (A class of formulas is solvable iff it is decidable for satisfiability; it is finitely controllable iff every satisfiable formula in it has a finite model.) At the end of [5], Gödel claims that the finite controllability of the GCI can be shown “by the same method” as he employed to show this for the class without identity. This claim has been questioned for nearly twenty years; in §1 below we give a brief history of investigations into it. The major result of this paper shows Gödel to have been mistaken: the GCI is unsolvable. §2 contains the basic construction, which yields a satisfiable formula in the GCI that lacks finite models. This formula may easily be exploited to encode undecidable problems into the GCI.

Quantification theory, or the first-order predicate calculus, is ordinarily so formulated as to provide as theorems all and only those formulas which come out true under all interpretations in all non-empty domains. There are two strong reasons for thus leaving aside the empty domain.

(i) Where D is any non-empty domain, any quantificational formula which comes out true under all interpretations in all domains larger than D will come out true also under all interpretations in D. (Cf. [4], p. 92.) Thus, though any small domain has a certain triviality, all but one of them, the empty domain, can be included without cost. To include the empty one, on the other hand, would mean surrendering some formulas which are valid everywhere else and thus generally useful.

(ii) An easy supplementary test enables us anyway, when we please, to decide whether a formula holds for the empty domain. We have only to mark the universal quantifications as true and the existential ones as false, and apply truth-table considerations.

Incidentally, the existence of that supplementary test shows that there is no difficulty in framing an inclusive quantification theory (i.e., inclusive of the empty domain) if we so desire. A proof in this theory can be made to consist simply of a proof in the exclusive (or usual) theory followed by a check by the method of (ii). We may, however, be curious to see a more direct or autonomous formulation: one which does not consist, like the above, of the exclusive theory plus a rule of expurgation. And, in fact, such formulations have of late been forthcoming: Mostowski [5], Hailperin [3], and, as part of a broader context, Church [2]. I shall not presuppose acquaintance with these papers, except in my final paragraph (and then only with [3]).