We define a structure which is much simpler than a morass, but whose existence is equivalent to the existence of a morass.

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 give a self-contained geometric proof of the completeness theorem for the infinite-valued sentential calculus of Łukasiewicz.

Our theme is that not every interesting question in set theory is independent of ZFC. We give an example of a first order theory T with countable D(T) which cannot have a universal model at ℵ1; without CH; we prove in ZFC a covering theorem from the hypothesis of the existence of a universal model for some theory; and we prove—again in ZFC—that for a large class of cardinals there is no universal linear order (e.g. in every regular ). In fact, what we show is that if there is a universal linear order at a regular λ and its existence is not a result of a trivial cardinal arithmetical reason, then λ “resembles” ℵ1—a cardinal for which the consistency of having a universal order is known. As for singular cardinals, we show that for many singular cardinals, if they are not strong limits then they have no universal linear order. As a result of the nonexistence of a universal linear order, we show the nonexistence of universal models for all theories possessing the strict order property (for example, ordered fields and groups, Boolean algebras, p-adic rings and fields, partial orders, models of PA and so on).

A type-structure of partial effective functionals over the natural numbers, based on a canonical enumeration of the partial recursive functions, is developed. These partial functionals, defined by a direct elementary technique, turn out to be the computable elements of the hereditary continuous partial objects; moreover, there is a commutative system of enumerations of any given type by any type below (relative numberings).

By this and by results in [1] and [2], the Kleene-Kreisel countable functionals and the hereditary effective operations (HEO) are easily characterized.

§0. Introduction. What follows is a write-up of my contribution to the symposium “Hilbert's Program Sixty Years Later” which was sponsored jointly by the American Philosophical Association and the Association for Symbolic Logic. The symposium was held on December 29,1985 in Washington, D. C. The panelists were Solomon Feferman, Dag Prawitz and myself. The moderator was Wilfried Sieg. The research which I discuss here was partially supported by NSF Grant DMS-8317874.

I am grateful to the organizers of this timely symposium on an important topic. As a mathematician I particularly value the opportunity to address an audience consisting largely of philosophers. It is true that I was asked to concentrate on the mathematical aspects of Hilbert's program. But since Hilbert's program is concerned solely with the foundations of mathematics, the restriction to mathematical aspects is really no restriction at all.

Hilbert assigned a special role to a certain restricted kind of mathematical reasoning known as finitistic. The essence of Hilbert's program was to justify all of set-theoretical mathematics by means of a reduction to finitism. It is now well known that this task cannot be carried out. Any such possibility is refuted by Gödel's theorem. Nevertheless, recent research has revealed the feasibility of a significant partial realization of Hilbert's program. Despite Gödel's theorem, one can give a finitistic reduction for a substantial portion of infinitistic mathematics including many of the best-known nonconstructive theorems. My purpose here is to call attention to these modern developments.

The philosophical dispute over whether there are universale, or abstract entities, is not a dispute over the admissibility of general terms. Both sides will agree that general terms, e.g. ‘man,’ and perhaps even abstract singular terms such as ‘mankind’ and ‘7’, are meaningful, in the sense at least of participating in statements which as wholes are true or false. Where the platonists (as I shall call those who accept universale) differ from their opponents, the nominalists, is in positing a realm of entities, universals, corresponding to such general or abstract words.

The platonist is likely to regard the word ‘man’ as naming a universal, the class of men or the property of being a man, much as the word ‘Caesar’ names the concrete object Caesar. Actually, however, this is an extraneous detail. The platonist could equally well concur with the nominalist in the view that general terms, though meaningful in context, are not names at all.

The ω-rule in the λ-calculus (or, more exactly, the λK-β, η calculus) is

In [1] it was shown that this rule is consistent with the other rules of the λ-calculus. We will show the rule cannot be derived from the other rules; that is, we will give closed terms M and N such that MZ = NZ can be proved without using the ω-rule, for each closed term Z, but M = N cannot be so proved. This strengthens a result in [4] and answers a question of Barendregt.

The language of the λ-calculus has an alphabet containing denumerably many variables a, b, c, … (which have a standard listing e 1, e 2, …), improper symbolsλ, ( , ) and a single predicate symbol = for equality.

Terms are defined inductively by the following:

(1) A variable is a term.

(2) If M and N are terms, so is (MN); it is called a combination.

(3) If M is a term and x is a variable, (λx M) is a term; it is called an abstraction.

We use ≡ for syntactic identity of terms.

If M and N are terms, M = N is a formula.

BV(M), the set of bound variables in M, and FV(M), its free variables, are defined inductively by

A term M is closed iff FV(M) = ∅.

We prove the following results: (i) PV proves NP ⊆ P/poly iff PV proves coNP ⊆ NP/O(1). (ii) If PV proves NP ⊆ P/poly then PV proves that the Polynomial Hierarchy collapses to the Boolean Hierarchy, (iii) proves NP ⊆ P/poly iff proves coNP ⊆ NP/O(log n). (iv) If proves NP ⊆ P/poly then proves that the Polynomial Hierarchy collapses to PNP[log n]. (v) If proves NP ⊆ P/poly then proves that the Polynomial Hierarchy collapses to PNP.

Motivated by these results we introduce a new concept in proof complexity: proof systems with advice, and we make some initial observations about them.

The purpose of this paper is to present two new theorems concerning the degrees of coinfinite recursively enumerable (r.e.) sets which have no maximal supersets Let the class of all such degrees be denoted by A. Martin in [2] conjectured that there was some equality or inequality involving a′ or a″ characterizing the degrees a in A. Martin himself proved ([2, Corollary 4.1]) that a′ = 0″ is sufficient for ar r.e. degree a to be in A, and Robinson [3] announced that a′ ≥ 0″ is necessary. In this paper we improve both of these theorems by a factor of the jump, i.e., we shall show that a″ = 0″ is sufficient for an r.e. degree a to be in A, and that a″ ≥ 0″ is necessary.

Why the Post-Kleene arithmetical hierarchy of degrees of (recursive) unsolvability was extended into the transfinite is not clear. Perhaps it was thought that if a hierarchy of sufficiently fine structure could be described that would include all sets of integers, some light might be thrown on the Continuum Hypothesis, and its truth or falsity possibly even ascertained. There is also some evidence in the 1955 papers of Kleene (cf. Kleene [2], [3], [4]) that it was once hoped that a theorem for the analytical hierarchy analogous to the result of Post and Kleene

We prove a cell decomposition theorem for Presburger sets and introduce a dimension theory for Z-groups with the Presburger structure. Using the cell decomposition theorem we obtain a full classification of Presburger sets up to definable bijection. We also exhibit a tight connection between the definable sets in an arbitrary p-minimal field and Presburger sets in its value group. We give a negative result about expansions of Presburger structures and prove uniform elimination of imaginaries for Presburger structures within the Presburger language.

A. M.Pitts in [Pi] proved that is a bi-Heyting category satisfying the Lawvere condition. We show that the embedding Φ: → Sh(P0, J0) into the topos of sheaves, (P0 is the category of finite rooted posets and open maps, J0 the canonical topology on P0) given by H ↦ HA(H, (−)) : P0 → Set preserves the structure mentioned above, finite coproducts, and subobject classifier; it is also conservative. This whole structure on can be derived from that of Sh(P0, J0) via the embedding Φ. We also show that the equivalence relations in are not effective in general. On the way to these results we establish a new kind of duality between and a category of sheaves equipped with certain structure defined in terms of Ehrenfeucht games. Our methods are model-theoretic and combinatorial as opposed to proof-theoretic as in [Pi].

We characterize (both from a syntactic and an algebraic point of view) the normal K4-logics for which unification is filtering. We also give a sufficient semantic criterion for existence of most general unifiers, covering natural extensions of K4.2+ (i.e., of the modal system obtained from K4 by adding to it, as a further axiom schemata, the modal translation of the weak excluded middle principle).

In [3]. two different effective versions of Borel embedding are defined. The first, called computable embedding, is based on uniform enumeration reducibility. while the second, called Turing computable embedding, is based on uniform Turing reducibility. While [3] focused mainly on computable embeddings, the present paper considers Turing computable embeddings. Although the two notions are not equivalent, we can show that they behave alike on the mathematically interesting classes chosen for investigation in [3]. We give a “Pull-back Theorem”, saying that if Ф is a Turing computable embedding of K into K′, then for any computable infinitary sentence φ in the language of K′, we can find a computable infinitary sentence φ* in the language of K such that for all A ∈ K A ⊨ φ* iff Φ (A) ⊨ φ and φ* has the same “complexity” as φ (i.e., if φ is computable Σα or computable Πα, for α ≥ 1, then so is φ*). The Pull-back Theorem is useful in proving non-embeddability, and it has other applications as well.

Interest has steadily increased among logicians and philosophers in versions of quantification theory which meet the following criteria: (1) no existence assumptions are made with respect to individual constants, and (2) theorems are valid in every domain including the empty domain. Logics meeting the former of these criteria are called free logics by Lambert and have been investigated in a series of papers by him and by van Fraassen, and by Leblanc and Thomason.1

Although it is natural to impose (2) in the presence of (1), the criteria are independent.2 Hence we baptize logics which meet both criteria universally free.

We prove that every n-modal logic between Kn and S5n is undecidable, whenever n ≥ 3. We also show that each of these logics is non-finitely axiomatizable, lacks the product finite model property, and there is no algorithm deciding whether a finite frame validates the logic. These results answer several questions of Gabbay and Shehtman. The proofs combine the modal logic technique of Yankov–Fine frame formulas with algebraic logic results of Halmos, Johnson and Monk, and give a reduction of the (undecidable) representation problem of finite relation algebras.

It is my intention in this paper to add somewhat to the observations already made in my earlier publications on the existence of undecidable statements in systems of logic possessing rules of inference of a “non-finitary” (“non-constructive”) character (§§1–4).

I also wish to emphasize once more the part played by the concept of truth in relation to problems of this nature (§§5–8).

At the end of this paper I shall give a result which was not touched upon in my earlier publications. It seems to be of interest for the reason (among others) that it is an example of a result obtained by a fruitful combination of the method of constructing undecidable statements (due to K. Gödel) with the results obtained in the theory of truth.

1. Let us consider a formalized logical system L. Without giving a detailed description of the system we shall assume that it possesses the usual “finitary” (“constructive”) rules of inference, such as the rule of substitution and the rule of detachment (modus ponens), and that among the laws of the system are included all the postulates of the calculus of statements, and finally that the laws of the system suffice for the construction of the arithmetic of natural numbers. Moreover, the system L may be based upon the theory of types and so be the result of some formalization of Principia mathematica. It may also be a system which is independent of any theory of types and resembles Zermelo's set theory.

Inductive definability has been studied for some time already. Nonetheless, there are some simple questions that seem to have been overlooked. In particular, there is the problem of the expressibility of the μ-calculus.

The μ-calculus originated with Scott and DeBakker [SD] and was developed by Hitchcock and Park [HP], Park [Pa], Kozen [K], and others. It is a language for including inductive definitions with first-order logic. One can think of a formula in first-order logic (with one free variable) as defining a subset of the universe, the set of elements that make it true. Then “and” corresponds to intersection, “or” to union, and “not” to complementation. Viewing the standard connectives as operations on sets, there is no reason not to include one more: least fixed point.

There are certain features of the μ-calculus coming from its being a language that make it interesting. A natural class of inductive definitions are those that are monotone: if X ⊃ Y then Γ (X) ⊃ Γ (Y) (where Γ (X) is the result of one application of the operator Γ to the set X). When studying monotonic operations in the context of a language, one would need a syntactic guarantor of monotonicity. This is provided by the notion of positivity. An occurrence of a set variable S is positive if that occurrence is in the scopes of exactly an even number of negations (the antecedent of a conditional counting as a negation). S is positive in a formula ϕ if each occurrence of S is positive. Intuitively, the formula can ask whether x ∊ S, but not whether x ∉ S. Such a ϕ can be considered an inductive definition: Γ (X) = {x ∣ ϕ(x), where the variable S is interpreted as X}. Moreover, this induction is monotone: as X gets bigger, ϕ can become only more true, by the positivity of S in ϕ. So in the μ-calculus, a formula is well formed by definition only if all of its inductive definitions are positive, in order to guarantee that all inductive definitions are monotone.

In Reverse Mathematics, the axiom system DNR. asserting the existence of diagonally non-recursive functions, is strictly weaker than WWKL0 (weak weak König's Lemma).