Let C be an axiom system formalized within the first order functional calculus, and let C′ be related to C as the Bernays-Gödel set theory is related to the Zermelo-Fraenkel set theory. (An exact definition of C′ will be given later.) Ilse Novak [5] and Mostowski [8] have shown that, if C is consistent, then C′ is consistent. (The converse is obvious.) Mostowski has also proved the stronger result that any theorem of C′ which can be formalized in C is a theorem of C.

The proofs of Novak and Mostowski do not provide a direct method for obtaining a contradiction in C from a contradiction in C′. We could, of course, obtain such a contradiction by proving the theorems of C one by one; the above result assures us that we must eventually obtain a contradiction. A similar process is necessary to obtain the proof of a theorem in C from its proof in C′. The purpose of this paper is to give a new proof of these theorems which provides a direct method of obtaining the desired contradiction or proof.

The advantage of the proof may be stated more specifically by arithmetizing the syntax of C and C′.

This paper deals mainly with quantifier-free second order systems (i.e., with free variables for numbers and functions, and constants for numbers, functions, and functionals) whose basic rules are those of primitive recursive arithmetic together with definition of functionals by primitive recursion and explicit definition. Precise descriptions are given in §2. The additional rules have the form of definition by transfinite recursion up to some ordinal ξ (where ξ is represented by a primitive recursive (p.r.) ordering). In §3 we discuss some elementary closure properties (under rules of inference and definition) of systems with recursion up to ξ. Let Rξ denote (temporarily) the system with recursion up to ξ. The main results of this paper are of two sorts:

Sections 5–7 are concerned with less elementary closure properties of the systems Rξ. Namely, we show that certain classes of functional equations in Rη can be solved in Rη for some explicitly determined η < ε(η) (the least ε-number > ξ). The classes of functional equations considered all have roughly the form of definition by recursion on the partial ordering of unsecured sequences of a given functional F, or on some ordering which is obtained from this by simple ordinal operations. The key lemma (Theorem 1) needed for the reduction of these equations to transfinite recursion is simply a sharpening of the Brouwer-Kleene idea.

In his doctor's thesis [1], Henkin has shown that if a formal logic is consistent, and sufficiently complex (for instance, if it is adequate for number theory), then it must admit a non-standard model. In particular, he showed that there must be a model in which that portion of the model which is supposed to represent the positive integers of the formal logic is not in fact isomorphic to the positive integers; indeed it is not even well ordered by what is supposed to be the relation of ≦.

For the purposes of the present paper, we do not need a precise definition of what is meant by a standard model of a formal logic. The non-standard models which we shall discuss will be flagrantly non-standard, as for instance a model of the sort whose existence is proved by Henkin. It will suffice if we and our readers are in agreement that a model of a formal logic is not a standard model if either:

(a) The relation in the model which represents the equality relation in the formal logic is not the equality relation for objects of the model.

(b) That portion of the model which is supposed to represent the positive integers of the formal logic is not well ordered by the relation ≦.

(c) That portion of the model which is supposed to represent the ordinal numbers of the formal logic is not well ordered by the relation ≦.

In this paper we prove undecidability of first-order definability of propositional formulas. The main result is proved for intuitionistic formulas, but it remains valid for other kinds of propositional formulas by analogous arguments or with the help of various translations.

For general background on correspondence theory the reader is referred to van Benthem [1], [2] (see [3] for a survey of recent results).

The method for the proofs of undecidability in this paper will be to simulate calculations of a Minsky machine by intuitionistic formulas. §3 concerns this simulation. Effective procedures for the construction of simulating modal formulas can be found in the literature (cf. [4]).

The principal results of the paper are in §4. §5 gives some further undecidability results, that will be proved in another paper by modification of the method of this paper.

I am indebted to the referee for drawing my attention to some errors in an earlier version of this paper.

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.

This note is an addendum to an incompleteness result of Feferman and Spector [1]: for any such progression satisfying the (natural) conditions listed in [1] there is a true Π10-formula which cannot be derived in the progression. The idea of their proof yields a stronger result.

If each numerical instance A[x/n] of the formula A (with the free numerical variable x) is decided in a recursive progression along a Π11-path then the set {n: ⊦ A[x/n]} is recursive.

In other words, only recursively solvable problems are decidable in such progressions. This yields the incompleteness result of [1] when specialized to some Π10 formula A which defines a nonrecursive set, since then some instance A[x/n] must be undecided and A[x/n] is a closed Π10 formula. The stronger result is needed to extend Church's thesis for total functions reckonable in formal systems to (total) functions reckonable in recursive progressions onΠ11-paths. A partially reckonable function always has a Π11 graph (and if its graph is Δ11 then it is by C. Jockusch, r.e.; so some Π11 sets are not partially reckonable). The relevance of these facts for the model of mathematical reasoning provided by (variants of) Turing's ordinal logics is analyzed in (b) (ii) of Part II, which goes into our current knowledge about Church's thesis.

Working in the language of first-order arithmetic we consider models of the base theory P−. Suppose M is a model of P− and let M satisfy induction for Σ1-formulas. First it is shown that the Friedberg-Muchnik finite injury argument can be performed inside M, and then, using a blocking method for the requirements, we prove that the Sacks splitting construction can be done in M. So, the “amount” of induction needed to perform the known finite injury priority arguments is Σ1-induction.

Pretopologies were introduced in [S], and there shown to give a complete semantics for a propositional sequent calculus BL, here called basic linear logic, as well as for its extensions by structural rules, ex falso quodlibet or double negation. Immediately after Logic Colloquium '88, a conversation with Per Martin-Löf helped me to see how the pretopology semantics should be extended to predicate logic; the result now is a simple and fully constructive completeness proof for first order BL and virtually all its extensions, including the usual, or structured, intuitionistic and classical logic. Such a proof clearly illustrates the fact that stronger set-theoretic principles and classical metalogic are necessary only when completeness is sought with respect to a special class of models, such as the usual two-valued models.

To make the paper self-contained, I briefly review in §1 the definition of pretopologies; §2 deals with syntax and §3 with semantics. The completeness proof in §4, though similar in structure, is sensibly simpler than that in [S], and this is why it is given in detail. In §5 it is shown how little is needed to obtain completeness for extensions of BL in the same language. Finally, in §6 connections with proofs with respect to more traditional semantics are briefly investigated, and some open problems are put forward.

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

Rational Pavelka logic extends Łukasiewicz infinitely valued logic by adding truth constants r̄ for rationals in [0. 1]. We show that this is a conservative extension. We note that this shows that provability degree can be defined in Łukasiewicz logic. We also give a counterexample to a soundness theorem of Belluce and Chang published in 1963.

In [5] Henkin defined a quantifier, which we shall denote by QH: linking four variables in one formula. This quantifier is related to the notion of formulas in which the usual universal and existential quantifiers occur but are not linearly ordered. The original definition of QH was

Here (QHx1x2y1y2)φ is true if for every x1 there exists y1 such that for every x2 there exists y2, whose choice depends only on x2 not on x1 and y1 such that φ(x14, x2, y1, y2). Another way of writing this is

In [5] it was observed that the logic L(QH) obtained by adjoining QH defined as in (1) is more powerful than first-order logic. In particular, it turned out that the quantifier “there exist infinitely many” denoted Q0 was definable from QH because

Introduction. This paper is a sequel to our paper [3]. In that paper we introduced the notion of a finite approximation to an infinitely long formula, in a language L with infinitely long expressions of the type considered by Henkin in [2]. The results of the paper [3] show relationships between the models of an infinitely long sentence and the models of its finite approximations. In the present paper we shall apply the main result of [3] to prove a number of theorems about ordinary finitely long sentences; these theorems are of a type which one might call “preservation theorems”. The following two known results are typical preservation theorems: A sentence φ is preserved under substructures if and only if φ is (logically) equivalent to some universal sentence (Łoś [7] and Tarski [11]); φ is preserved under homomorphic images if and only if φ is equivalent to some positive sentence (Lyndon [8]). An expository account of preservation theorems may be found in Lyndon [9].

We shall use freely all of the notation introduced in [3], and shall not attempt to make this paper selfcontained. However, the reader should have no difficulty following this paper after he has read [3]. In § 1 we cover some preliminary topics. In § 2 and § 3 we shall illustrate our method in familiar situations by proving anew the two preservation theorems mentioned above. We shall then obtain four new preservation theorems in §§ 4, 5, and 6, involving respectively direct powers and roots, strong homomorphisms and retracts, and direct factors. The result in § 6 was stated in the abstract [4], while the results in § 5 were stated in the abstract [5].

In this third and last paper on inner models we consider some of the inherent limitations of the method of using inner models of the type defined in 1.2 for the proof of consistency results for the particular system of set theory under consideration. Roughly speaking this limitation may be described by saying that practically no further consistency results can be obtained by the construction of models satisfying the conditions of theorem 1.5, i.e., conditions 1.31, 1.32, 1.33, 1.51, viz.:

This applies in particular to the ‘complete models’ defined in 1.4. Before going on to a precise statement of these limitations we shall consider now the theorem on which they depend. This is concerned with a particular type of complete model examples of which we call “proper complete models”; they are those complete models which are essentially interior to the universe, those whose classes are sets of the universe constituting a class thereof, i.e., those for which the following proposition is true:

The main theorem of this paper is that the statement that there are no models of this kind can be expressed formally in the same way as the axioms A, B, C and furthermore it can be proved that if the axiom system A, B, C is consistent then so is the system consisting of axioms A, B, C, plus this new hypothesis that there exist no proper complete models. When combined with the axiom ‘V = L’ introduced by Gödel in (1) this new hypothesis yields a system in which any normal complete model which exists has for its universal class V, the universal class of the original system.

The aim of this paper is to give, using the Kripke semantics for intuitionism, a representation of finitely generated free Heyting algebras. By means of the representation we determine in a constructive way some set of “special elements” of such algebras. Furthermore, we show that many algebraic properties which are satisfied by the free algebra on one generator are not satisfied by free algebras on more than one generator.

The real importance of cut-free proofs is not the elimination of cuts per se, but rather that such proofs obey the subformula principle. In this paper we accomplish this latter objective in a different manner.

In the usual formulations of Gentzen systems, there is only one axiom scheme; all the other postulates are inference rules. By contrast, we consider here some Gentzen type axiom systems for propositional logic and Quantification Theory in which there is only one inference rule; all the other postulates are axiom schemes. This admits of an unusually elegant axiomatization of logic.

We characterize the structure of computably categorical trees of finite height, and prove that our criterion is both necessary and sufficient. Intuitively, the characterization is easiest to express in terms of isomorphisms of (possibly infinite) trees, but in fact it is equivalent to a -condition. We show that all trees which are not computably categorical have computable dimension ω. Finally, we prove that for every n ≥ 1 in ω, there exists a computable tree of finite height which is Σ30-categorical but not Δn3-categorical

We prove that the problem of determining the minimum propositional proof length is NP-hard to approximate within a factor of . These results are very robust in that they hold for almost all natural proof systems, including: Frege systems, extended Frege systems, resolution. Horn resolution, the polynomial calculus, the sequent calculus, the cut-free sequent calculus, as well as the polynomial calculus. Our hardness of approximation results usually apply to proof length measured either by number of symbols or by number of inferences, for tree-like or dag-like proofs. We introduce the Monotone Minimum (Circuit) Satisfying Assignment problem and reduce it to the problems of approximation of the length of proofs.

We consider the problem of finding and classifying representations in algebraic logic. This is approached by letting two players build a representation using a game. Homogeneous and universal representations are characterized according to the outcome of certain games. The Lyndon conditions defining representable relation algebras (for the finite case) and a similar schema for cylindric algebras are derived. Finte relation algebras with homogeneous representations are characterized by first order formulas. Equivalence games are defined, and are used to establish whether an algebra is ω-categorical. We have a simple proof that the perfect extension of a representable relation algebra is completely representable.

An important open problem from algebraic logic is addressed by devising another two-player game, and using it to derive equational axiomatisations for the classes of all representable relation algebras and representable cylindric algebras.

Other instances of this approach are looked at, and include the step by step method.

We say that an uncountable metric space is computably categorical if every two computable structures on this space are equivalent up to a computable isometry. We show that Cantor space, the Urysohn space, and every separable Hilbert space are computably categorical, but the space [0, 1] of continuous functions on the unit interval with the supremum metric is not. We also characterize computably categorical subspaces of ℝn, and give a sufficient condition for a space to be computably categorical. Our interest is motivated by classical and recent results in computable (countable) model theory and computable analysis.

This work results from an attempt to give the vague notion of relevance a concrete semantical interpretation. The idea is that propositions may be divided into different “domains of relevance”. Each “domain” has its own “T” and “F” values, and propositions “belonging” to one domain can never entail propositions “belonging” to another, unconnected one.

The semantics we have developed were found to correspond to an already known system, which we call here RMI⥲. Its axioms are the implication-negation axioms of the system RM ([1, Chapter 5]). However, as Meyer has shown, RM is not a conservative extension of RMI⥲, since RMI⥲ has the sharing-of-variables property ([5], and [1, pp. 148–149[), which the implication-negation fragment of RM has not.

RMI⥲ has four advantages in comparison to its more famous sister R⥲ (the pure intentional fragment of the system R; see [1]):

a) It has a very natural (from a relevance point of view) many-valued semantics, the simple form of which we describe here.

b) RMI⥲, ⊢ A1 → [A2 → (… → (An → A) …)] iff there is a proof of A from the set {A1, …, An} that actually uses all the members of this set. In R⥲, this holds only if we talk about “sequences” instead of “sets”. This is somewhat less intuitive (see [1, pp. 394–395]).

c) RMI⥲ is a maximal “natural” relevance logic, in the sense that every proper extension of it limits the number of “domains of relevance” (§III).