Let S2S [WS2S] respectively be the strong [weak] monadic second order theory of the binary tree T in the language of two successor functions. An S2S-formula whose free variables are just individual variables defines a relation on T (rather than on the power set of T). We show that S2S and WS2S define the same relations on T, and we give a simple characterization of these relations.

This is the first in a series of articles outlining a new approach to Semantics. The novelty in the approach is that the concept of an interpretation of a logical system is taken as the central concept of Semantics. I hope to show that by means of this approach a satisfactory definition can be given for such controversial concepts as analyticity, and at the same time the approach leads to a unified foundation for formalized Semantics.

As the possibility of such definitions has been questioned in recent years, it is an important task to try to give precise definitions. Clearly, this is the task of those philosophers who believe that concepts like analyticity should play a fundamental role in Semantics. On the other hand, the philosophers who have criticized these concepts will now be able to tell just exactly why these definitions are unacceptable to them — instead of being forced to talk in generalities. It seems to me that no further progress is possible until we have precise definitions available for discussion.

The fundamental semantic concepts fall into two classes: those, like truth, for which Tarski has offered definitions; and those additional ones, like analytic truth, for which we have Carnap's proposed definitions.

In this paper the canonical modal logics, a kind of complete modal logics introduced in K. Fine [4] and R. I. Goldblatt [5], will be characterized semantically using the concept of an ultrafilter extension, an operation on frames inspired by the algebraic theory of modal logic. Theorem 8 of R. I. Goldblatt and S. K. Thomason [6] characterizing the modally definable Σ⊿-elementary classes of frames will follow as a corollary. A second corollary is Theorem 2 of [4] which states that any complete modal logic defining a Σ⊿-elementary class of frames is canonical.

The main tool in obtaining these results is the duality between modal algebras and general frames developed in R. I. Goldblatt [5]. The relevant notions and results from this theory will be stated in §2. The concept of a canonical modal logic is introduced and motivated in §3, which also contains the above-mentioned theorems. In §4, a kind of appendix to the preceding discussion, preservation of first-order sentences under ultrafilter extensions (and some other relevant operations on frames) is discussed.

The modal language to be considered here has an infinite supply of proposition letters (p, q, r, …), a propositional constant ⊥ (the so-called falsum, standing for a fixed contradiction), the usual Boolean operators ¬ (not), ∨ (or), ∨ (and), → (if … then …), and ↔ (if and only if)—with ¬ and ∨ regarded as primitives—and the two unary modal operators ◇ (possibly) and □ (necessarily)— ◇ being regarded as primitive. Modal formulas will be denoted by lower case Greek letters, sets of formulas by Greek capitals.

We will study several weak axiom systems that use the Subtraction and Division primitives (rather than Addition and Multiplication) to formally encode the theorems of Arithmetic. Provided such axiom systems do not recognize Multiplication as a total function, we will show that it is feasible for them to verify their Semantic Tableaux, Herbrand, and Cut-Free consistencies. If our axiom systems additionally do not recognize Addition as a total function, they will be capable of recognizing the consistency of their Hilbert-style deductive proofs. Our axiom systems will not be strong enough to recognize their Canonical Reflection principle, but they will be capable of recognizing an approximation of it, called the “Tangibility Reflection Principle”. We will also prove some new versions of the Second Incompleteness Theorem stating essentially that it is not possible to extend our exceptions to the Incompleteness Theorem much further.

This article provides the proof-theoretic analysis of the transfinitely iterated fixed point theories and ; the exact proof-theoretic ordinals of these systems are presented.

In this paper we answer some of the questions left open in [2]. We use the terminology of [2]. In particular, a theory will be a formal system formulated within the first-order calculus with identity. A theory is identified with the set of Gödel numbers of the theorems of the theory. Thus Craig's theorem [1] asserts that a theory is axiomatizable if and only if it is recursively enumerable.

In [2], Feferman showed that if A is any recursively enumerable set, then there is an axiomatizable theory T having the same degree of unsolvability as A. (This result was proved independently by D. B. Mumford.) We show in Theorem 2 that if A is not recursive, then T may be chosen essentially undecidable. This depends on Theorem 1, which is a result on recursively enumerable sets of some independent interest.

Our second result, given in Theorem 3, gives sufficient conditions for a theory to be creative. These conditions are more general than those given by Feferman. In particular, they show that the system of Kreisel described in [2] is creative.

Syntactic translations of classical logic C into intuitionistic logic I are well known (see [Kol25], [Gli29], [Göd32], [Kre58b], [M063], [Cel69] and [Lei71]). Harvey Friedman [Fri78] used a translation of a similar nature, from I into itself, to reprove a theorem of Kreisel [Kre58a] that various theories based on I are closed under Markov's rule: if ¬¬∃x.α is a theorem, where x is a numeric variable and α is a primitive recursive relation, then ∃x.α is a theorem. Composing this with Gödel's translation from classical to intuitionistic theories, it follows that the functions provably recursive in the classical version of the theories considered are provably recursive already in their intuitionistic version. This conservation result is important in that it guarantees that no information about the convergence of recursive functions is lost when proofs are restricted to constructive logic, thus removing a potential objection to the use of constructive logic in reasoning about programs (see [C078] for example). Conversely, no objection can be raised by intuitionists to proofs of formulas that use classical reasoning, because such proofs can be converted to constructive proofs (this has been exploited extensively; see [Smo82]).

Proofs of closure under Markov's rule had required, until Friedman's proof, a relatively sophisticated mathematical apparatus. The chief method used Godel's “Dialectica” interpretation (see [Tro73, §3]). Other proofs used cut-elimination, provable reflection for subsystems [Gir73], and Kripke models [Smo73]. Moreover, adapting these proofs to new theories had required that the underlying meta-mathematical techniques be adapted first, not always a trivial step.

In 1981, Takeuti introduced quantum set theory as the quantum counterpart of Boolean valued models of set theory by constructing a model of set theory based on quantum logic represented by the lattice of closed subspaces in a Hilbert space and showed that appropriate quantum counterparts of ZFC axioms hold in the model. Here, Takeuti's formulation is extended to construct a model of set theory based on the logic represented by the lattice of projections in an arbitrary von Neumann algebra. A transfer principle is established that enables us to transfer theorems of ZFC to their quantum counterparts holding in the model. The set of real numbers in the model is shown to be in one-to-one correspondence with the set of self-adjoint operators affiliated with the von Neumann algebra generated by the logic. Despite the difficulty pointed out by Takeuti that equality axioms do not generally hold in quantum set theory, it is shown that equality axioms hold for any real numbers in the model. It is also shown that any observational proposition in quantum mechanics can be represented by a corresponding statement for real numbers in the model with the truth value consistent with the standard formulation of quantum mechanics, and that the equality relation between two real numbers in the model is equivalent with the notion of perfect correlation between corresponding observables (self-adjoint operators) in quantum mechanics. The paper is concluded with some remarks on the relevance to quantum set theory of the choice of the implication connective in quantum logic.

In investigations of the foundations of mathematics we can distinguish two separate tendencies. On the one hand, one may seek to define his subject with greatest possible explicitness: to obtain a formulation which satisfies the most exacting demands for precision, and which is at the same time free from paradoxes and adequate for the purpose. On the other hand, besides the problem of formulation, there is that of simplification; one can seek to find systems based upon processes of greater and greater primitiveness. The reduction of a piece of mathematics to a formal system, and still further to a completely formalized system (as explained, for example, in my New York address a year ago), is a step toward the first of these objectives. But it is evident that one can formalize in various ways, and that some of these ways constitute a more profound analysis than others. Although from some points of view one way of formalization is as good as any other, yet a certain interest attaches to the problem of simplification, as is shown by the attention which some of the greatest mathematicians have devoted to it.

The researches about which I am reporting today are directed toward the second of these objectives. In fact we are concerned with constructing systems of an extremely rudimentary character, which analyze processes ordinarily taken for granted. This is properly part of the business of mathematical logic. Of course there are those, even among logicians, who doubt the utility of this sort of thing—who profess to have no interest in improvements which do not lead to increases in deductive power or what not. However that may be, this second objective certainly has some interest in its own right; and it is this interest which has formed the primary motivation for these researches.

Some syntactically simple fragments of intuitionistic logic possess considerable expressive power compared with their classical counterparts.

In particular, we consider in this paper intuitionistic second order propositional logic (ISPL) a formalisation of which may be obtained by adding to the intuitionistic propositional calculus quantifiers binding propositional variables together with the usual quantifier rules and the axiom scheme (Ex), where is a formula not containing x.

The main purpose of this paper is to show that the classical first order predicate calculus with identity can be (isomorphically) embedded in ISPL.

It turns out an immediate consequence of this that the classical first order predicate calculus with identity can also be embedded in the fragment (PLA) of the intuitionistic first order predicate calculus whose only logical symbols are → and (.) (universal quantifier) and the only nonlogical symbol (apart from individual variables and parentheses) a single monadic predicate letter.

Another consequence is that the classical first order predicate calculus can be embedded in the theory of Heyting algebras.

The undecidability of the formal systems under consideration evidently follows immediately from the present results.

We shall indicate how the methods employed may be extended to show also that the intuitionistic first order predicate calculus with identity can be embedded in both ISPL and PLA.

For the purpose of the present paper it will be convenient to use the following formalisation (S) of ISPL based on [3], rather than the one given above.

In this paper we prove two theorems. They answer questions raised by Myhill in 1956. (We recall the well-known fact that Myhill's invention of the maximal set in 1956 [2] stemmed from his attempt to prove I below.)

I. There exists an axiomatizable, essentially undecidable theory in standard formalization such that all axiomatizable extensions of are finite extensions.

II. There exists an axiomatizable but undecidable theory in standard formalization such that

(a) has a consistent, complete, decidable extension ,

(b) If is an axiomatizable extension of then either

(i) is a finite extension of , or

(ii) is a finite extension of .

Nonprincipal ultrafilters are harder to define in ZFC, and harder to obtain in ZF + DC, than nonprincipal measures.

The function μ from P(X) to the closed interval [0, 1] is a measure on X if μ. is finitely additive on disjoint sets and μ(X) = 1. (P is the power set.) μ is nonprincipal if μ ({x}) = 0 for each x Є X. μ is an ultrafilter if Range μ= {0, 1}. The existence of nonprincipal measures and ultrafilters on any infinite X follows from the axiom of choice.

Nonprincipal measures cannot necessarily be defined in ZFC. (ZF is Zermelo–Fraenkel set theory. ZFC is ZF with choice.) In ZF alone they cannot even be proved to exist. This was first established by Solovay [14] using an inaccessible cardinal. In the model of [14] no nonprincipal measure on ω is even ODR (definable from ordinal and real parameters). The HODR (hereditarily ODR) sets of this model form a model of ZF + DC (dependent choice) in which no nonprincipal measure on ω exists. Pincus [8] gave a model with the same properties making no use of an inaccessible. (This model was also known to Solovay.) The second model can be combined with ideas of A. Blass [1] to give a model of ZF + DC in which no nonprincipal measures exist on any set. Using this model one obtains a model of ZFC in which no nonprincipal measure on the set of real numbers is ODR. H. Friedman, in private communication, previously obtained such a model of ZFC by a different method. Our construction will be sketched in 4.1.

We can use the compositional semantics of Hodges [9] to show that any compositional semantics for logics of imperfect information must obey certain constraints on the number of semantically inequivalent formulas. As a corollary, there is no compositional semantics for the ‘independence-friendly’ logic of Hintikka and Sandu (henceforth IF) in which the interpretation in a structure A of each 1 -ary formula is a subset of the domain of A (Corollary 6.2 below proves this and more). After a fashion, this rescues a claim of Hintikka and provides the proof which he lacked:

… there is no realistic hope of formulating compositional truth-conditions for [sentences of IF], even though I have not given a strict impossibility proof to that effect.

(Hintikka [6] page 110ff.) One curious spinoff is that there is a structure of cardinality 6 on which the logic of Hintikka and Sandu gives nearly eight million inequivalent formulas in one free variable (which is more than the population of Finland).

We thank the referee for a sensible change of notation, and Joel Berman and Stan Burris for bringing us up to date with the computation of Dedekind's function (see section 4). Our own calculations, utterly trivial by comparison, were done with Maple V.

The paper Hodges [9] (cf. [10]) gave a compositional semantics for a language with some devices of imperfect information. The language was complicated, because it allowed imperfect information both at quantifiers and at conjunctions and disjunctions.

It was shown by Cholak, Jockusch, and Slaman that every computable 2-coloring of pairs admits an infinite low2 homogeneous set H. We answer a question of the same authors by showing that H may be chosen to satisfy in addition C ≰rH, where C is a given noncomputable set. This is shown by analyzing a new and simplified proof of Seetapun's cone avoidance theorem for Ramsey's theorem. We then extend the result to show that every computable 2-coloring of pairs admits a pair of low2 infinite homogeneous sets whose degrees form a minimal pair.

Our purpose is to delineate the extensions (normal and otherwise) of the propositional modal logic K5. We associate with each logic extending K5 a finitary index, in such a way that properties of the logics (for example, inclusion, normality, and tabularity) become effectively decidable properties of the indices. In addition we obtain explicit finite axiomatizations of all the extensions of K5 and an abstract characterization of the lattice of such extensions.

This paper refines and extends the Ph.D. thesis [2] of the first-named author, who wishes to acknowledge his debt to Brian F. Chellas for his considerable efforts in directing the research culminating in [2] and [3]. We also thank W. J. Blok and Gregory Cherlin for observations which greatly simplified the proofs of Theorem 3 and Corollary 10.

By a logic we mean a set of formulas in the countably infinite set Var of propositional variables and the connectives ⊥, →, and □ (other connectives being used abbreviatively) which contains all the classical tautologies and is closed under detachment and substitution. A logic is classical if it is also closed under RE (from A↔B infer □A ↔□B) and normal if it is classical and contains □ ⊤ and □ (P → q) → (□p → □q). A logic is quasi-classical if it contains a classical logic and quasi-normal if it contains a normal logic. Thus a quasi-normal logic is normal if and only if it is classical, and if and only if it is closed under RN (from A infer □A).

Preservation and interpolation results are obtained for L∞ω and sublogics ⊆ L∞ω such that equivalence in can be characterized by suitable back-and-forth conditions on sets of partial isomorphisms.

Our main result is the equivalence of two notions of reducibility between structures. One is a syntactical notion which is an effective version of interpretability as in model theory, and the other one is a computational notion which is a strengthening of the well-known Medvedev reducibility. We extend our result to effective bi-interpretability and also to effective reductions between classes of structures.

We show that the theory ATR0 is equivalent to a second-order generalization of the theory . As a result, ATR0 is conservative over for arithmetic sentences, though proofs in ATR0 can be much shorter than their counterparts.

We develop Fraïssé theory, namely the theory of Fraïssé classes and Fraïssé limits, in the context of metric structures. We show that a class of finitely generated structures is Fraïssé if and only if it is the age of a separable approximately homogeneous structure, and conversely, that this structure is necessarily the unique limit of the class, and is universal for it.

We do this in a somewhat new approach, in which “finite maps up to errors” are coded by approximate isometries.