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.

In this paper I will develop a semantic account for modal logic by considering only the values of sentences (and formulas). This account makes no use of possible worlds. To develop such an account, we must recognize four values. These are obtained by subdividing (plain) truth into necessary truth (T) and contingent truth (t); and by subdividing falsity into contingent falsity (f) and necessary falsity (impossibility: F). The semantic account results from reflecting on these concepts and on the meanings of the logical operators.

To begin with, we shall consider the propositional language L0. The language L0 has (1) infinitely many atomic sentences, (2) the two truth-functional connectives ∼, ∨, and the modal operator □. (Square brackets are used for punctuation.) The other logical expressions are defined as follows:

D1 [A & B] = (def)∼[∼A ∨ ∼ B],

D2 [A ⊃ B] = (def)[∼A ∨ B],

D3 ◊ A =(def)∼□∼A.

I shall use matrices to give partial characterizations of the significance of logical expressions in L0. For negation, this matrix is wholly adequate:

Upon reflection, it should be clear that this matrix is the obviously correct matrix for negation.

There is no algorithm for determining whether or not an equation is true in every 3-dimensional cylindric algebra. This theorem completes the solution to the problem of finding those values of α and β for which the equational theories of CAα and RCAβ are undecidable. (CAα and RCAβ are the classes of α-dimensional cylindric algebras and representable β-dimensional cylindric algebras. See [4] for definitions.) This problem was considered in [3]. It was known that RCA0 = CA0 and RCA1 = CA1 and that the equational theories of these classes are decidable. Tarski had shown that the equational theory of relation algebras is undecidable and, by utilizing connections between relation algebras and cylindric algebras, had also shown that the equational theories of CAα and RCAβ are undecidable whenever 4 ≤ α and 3 ≤ β. (Tarski's argument also applies to some varieties K ⊆ RCAβ with 3 ≤ β and to any variety K such that RCAα ⊆ K ⊆ CAα and 4 ≤ α.)

Thus the only cases left open in 1961 were CA2, RCA2 and CA3. Shortly there-after Henkin proved, in one of Tarski's seminars at Berkeley, that the equational theory of CA2 is decidable, and Scott proved that the set of valid sentences in a first-order language with only two variables is recursive [11]. (For a more model-theoretic proof of Scott's theorem see [9].) Scott's result is equivalent to the decidability of the equational theory of RCA2, so the only case left open was CA3.

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).

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.

Assuming the existence of a supercompact cardinal, we construct a model of ZFC + (There exists a nonsplitting stationary subset of ). Answering a question of Uri Abraham [A], [A-S], we prove that adding a real to the world always makes stationary

This paper presents three generalizations of the Second Incompleteness Theorem of Gödel (see [2]) which apply to a broader class of formal systems than previous generalizations (as, e.g., the generalization in [1]).

The content of all three of our results is that it is versions of the third derivability condition of Hilbert and Bernays (see p. 286 of [3]) which are crucial to Gödel's theorem. The second derivability condition plays some role in certain logics, but even there, only in the far weaker form of a definability condition (see Theorem 2).

The elimination of the first derivability condition allows the application of the Consistency Theorem to cut-free logics which cannot prove that they are closed under cut.

It is Theorem 1 which will probably have primary interest for readers who are not concerned with technical proof theory or with foundations, for it treats logics with quantifiers, and in that case one can dispose entirely of the first and second derivability conditions. The derivation of this result requires a “new twist” on old arguments. Specifically, we use a new variation on the standard self-referential lemma (this is Lemma 5.1 of [l]) to obtain a somewhat different self-referential construction than has previously been employed (this is our lemma in §2 below). With this new construction, we consider the sentence φ which “expresses” the fact: “My negation is provable.” Then, using hypotheses associated with Gödel's First Incompleteness Theorem, one shows that ⊢¬φ is impossible in a consistent logic. Finally, using only a version of the third Hilbert-Bernays derivability condition, one shows that the provability of the consistency statement implies ⊢¬φ, and hence that consistency is unprovable.

The aim of this paper is to prove strengthenings of three theorems appearing in Jensen [1].

We show that either of the following hypotheses imply that there is an inner model with a proper class of strong cardinals and a proper class of Woodin cardinals. 1) There is a countably closed cardinal κ ≥ ℵ such that □κ and □(κ) fail. 2) There is a cardinal κ such that κ is weakly compact in the generic extension by Col(κ, κ+). Of special interest is 1) with κ = ℵ3 since it follows from PFA by theorems of Todorcevic and Velickovic. Our main new technical result, which is due to the first author, is a weak covering theorem for the model obtained by stacking mice over Kc∥κ.

In this paper we define intensional models for the classical theory of types, thus arriving at an intensional type logic ITL. Intensional models generalize Henkin's general models and have a natural definition. As a class they do not validate the axiom of Extensionality. We give a cut-free sequent calculus for type theory and show completeness of this calculus with respect to the class of intensional models via a model existence theorem. After this we turn our attention to applications. Firstly, it is argued that, since ITL is truly intensional, it can be used to model ascriptions of propositional attitude without predicting logical omniscience. In order to illustrate this a small fragment of English is defined and provided with an ITL semantics. Secondly, it is shown that ITL models contain certain objects that can be identified with possible worlds. Essential elements of modal logic become available within classical type theory once the axiom of Extensionality is given up.

As a contribution to definability theory in the spirit of Tarski's classical work on (R, <, 0, 1, +, ·) we extend here part of his results to the structure

Here exp ∣[0, 1] and sin ∣[0, π] are the restrictions of the exponential and sine function to the closed intervals indicated; formally we identify these restricted functions with their graphs and regard these as binary relations on R. The superscript “RE” stands for “restricted elementary” since, given any elementary function, one can in general only define certain restrictions of it in RRE.

Let (RRE, constants) be the expansion of RRE obtained by adding a name for each real number to the language. We can now formulate our main result as follows.

Theorem. (RRE, constants) is strongly model-complete.

This means that every formula ϕ(X1, …, Xm) in the natural language of (RRE, constants) is equivalent to an existential formula

with the extra property that for each x ∈ Rm such that ϕ(x) is true in RRE there is exactly one y ∈ Rn such that ψ(x, y) is true in RRE. (Here ψ is quantifier free.)

Let T be a countable complete theory and C(T) the category whose objects are the models of T and morphisms are the elementary maps. The main object of this paper will be the study of C(T). The idea that a better understanding of the category may give us model theoretic information about T is quite natural: The (semi) group of automorphisms (endomorphisms) of a given structure is often a powerful tool for studying this structure. But certainly, one of the very first questions to be answered is: “to what extent does this category C(T) determine T?”

There is some obvious limitation: for example let T0 be the theory of infinite sets (in a language containing only =) and T1 the theory, in the language ( =, U(ν0),f(ν0)) stating that:

(1) U is infinite.

(2)f is a bijective map from U onto its complement.

It is quite easy to see that C(T0) is equivalent to C(T1). But, in this case, T0 andT1 can be “interpreted” each in the other. To make this notion of interpretation precise, we shall associate with each theory T a category, loosely denoted by T, defined as follows:

(1) The objects are the formulas in the given language.

(2) The morphisms from into are the formulas such that

(i.e. f defines a map from ϕ into ϕ; two morphisms defining the same map in all models of T should be identified).

I once asked myself the question: How were the famous axiom systems, such as Euclid's for geometry, Zermelo's for set theory, Peano's for arithmetic, originally obtained? This was to me more than merely a historical question, as I wished to know how the basic concepts and axioms were to be singled out, and, once they were singled out, how one could establish their adequacy. One possible approach which suggests itself is to take typical theorems, proofs, definitions, and examine case by case what assumptions and concepts are involved. The obstacle in such an empirical study is, apart from the obvious demand of excessive time and energy, the lack of conclusiveness in both result and justification.

The attempt to find an answer to this question led me to some interesting fragments of history. For example, in 1899 Cantor distinguished consistent collections (the “sets”) from inconsistent collections ([1], p. 443), anticipating partly the distinction between the two kinds of classes stressed by von Neumann and Quine. Cantor had already proposed a form of the axiom of substitution ([1], p. 444, line 3), although Fraenkel and Skolem, more than twenty years later, had to adjoin it to Zermelo's list of axioms as a supplement. In another direction, the history of the development of axioms of geometry makes clear how natural it was for Hilbert to raise in 1900 the consistency question of analysis ([2], p. 299) quite independently of the emphasis on set-theoretical paradoxes.

By far the best piece of good fortune I had in these historical researches was, however, my findings with regard to Peano's axioms for arithmetic. It is rather well-known, through Peano's own acknowledgement ([3], p. 273), that Peano borrowed his axioms from Dedekind and made extensive use of Grassmann's work in his development of the axioms.

The notion of a D-ring, generalizing that of a differential or a differenee ring, is introduced, Quantifier elimination and a version of the Ax—Kochen—Eršov principle is proven for a theory of valued D-fields of residual characteristic zero.

Let L be a first order language. If M is an L-structure, let LM be the expansion of L obtained by adding constants for the elements of M.

Definition. A type is definable if and only if for any L-formula , there is an LM-formula so that for all iff M ⊨ dθ(¯). The formula dθ is called the definition of θ.

Definable types play a central role in stability theory and have also proven useful in the study of models of arithmetic. We also remark that it is well known and easy to see that for M ≺ N, the property that every M-type realized in N is definable is equivalent to N being a conservative extension of M, where

Definition. If M ≺ N, we say that N is a conservative extension of M if for any n and any LN -definable S ⊂ Nn, S ∩ Mn is LM-definable in M.

Van den Dries [Dl] studied definable types over real closed fields and proved the following result.

0.1 (van den Dries), (i) Every type over (R, +, -,0,1) is definable.

(ii) Let F and K be real closed fields and F ⊂ K. Then, the following are equivalent:

(a) Every element of K that is bounded in absolute value by an element of F is infinitely close (in the sense of F) to an element of F.

(b) K is a conservative extension of F.

Elementary axioms describe a category of categories. Theorems of category theory follow, including some on adjunctions and triples. A new result is that associativity of composition in categories follows from cartesian closedness of the category of categories. The axioms plus an axiom of infinity are consistent iff the axioms for a well-pointed topos with separation axiom and natural numbers are. The theory is not finitely axiomatizable. Each axiom is independent of the others. Further independence and definability results are proved. Relations between categories and sets, the latter defined as discrete categories, are described, and applications to foundations are discussed.

In an m-valued propositional calculus, or a formalization of such a calculus, truth-value functions are allowed to take any truth-value t where 1 ≦ t ≦ m and m ≧ 2. In working with such calculi, or formalizations thereof, it has been decided to distinguish those truth-values which it is desirable for provable formulas to have from those which it is not desirable for provable formulas to have. The first class of truth-values is called designated and the second undesignated. This specification of certain of the m truth-values as designated and the remainder as undesignated is one of the distinguishing characteristics of m-valued propositional calculi, and it should be observed at the outset that two m-valued propositional calculi will be considered to differ even if they differ only in respect to the number of truth-values which are taken as designated.

We study the intersection type assignment system as defined by Barendregt, Coppo and Dezani. For the four essential variants of the system (with and without a universal type and with and without subtyping) we show that the emptiness (inhabitation) problem is recursively unsolvable. That is, there is no effective algorithm to decide if there is a closed term of a given type. It follows that provability in the logic of “strong conjunction” of Mints and Lopez-Escobar is also undecidable.