Nominal logic is a variant of first-order logic in which abstract syntax with names and binding is formalized in terms of two basic operations: name-swapping andfreshness. It relies on two important principles: equivariance (validity is preserved by name-swapping), and fresh name generation (“new” or fresh names can always be chosen). It is inspired by a particular class of models for abstract syntax trees involving names and binding, drawing on ideas from Fraenkel-Mostowski set theory: finite-support models in which each value can depend on only finitely many names.

Although nominal logic is sound with respect to such models, it is not complete. In this paper we review nominal logic and show why finite-support models are insufficient both in theory and practice. We then identify (up to isomorphism) the class of models with respect to which nominal logic is complete: ideal-supported models in which the supports of values are elements of a proper ideal on the set of names.

We also investigate an appropriate generalization of Herbrand models to nominal logic. After adjusting the syntax of nominal logic to include constants denoting names, we generalize universal theories to nominal-universal theories and prove that each such theory has an Herbrand model.

Relativization—the principle that says one can carry over proofs and theorems about partial recursive functions and Turing degrees to functions partial recursive in any given set A and the Turing degrees of sets in which A is recursive—is a pervasive phenomenon in recursion theory. It led H. Rogers, Jr. [15] to ask if, for every degree d, (≥ d), the partial ordering of Turing degrees above d, is isomorphic to all the degrees . We showed in Shore [17] that this homogeneity conjecture is false. More specifically we proved that if, for some n, the degree of Kleene's (the complete set) is recursive in d(n) then ≇ (≤ d). The key ingredient of the proof was a new version of a result from Nerode and Shore [13] (hereafter NS I) that any isomorphism φ: → (≥ d) must be the identity on some cone, i.e., there is an a called the base of the cone such that b ≥ a ⇒ φ(b) = b. This result was combined with information about minimal covers from Jockusch and Soare [8] and Harrington and Kechris [3] to derive a contradiction from the existence of such an isomorphism if deg() ≤ d(n).

One of the major problems of model theory is the spectrum problem, i.e. the development of structure theorems for the spectrum of models of a given theory. I hope that this paper will make a (small) contribution to the solution of this problem.

Broadly speaking, in this paper we take a fixed (but arbitrary) theory T and consider a particular class ℰ of models of T. The structures in ℰ (which are known as existentially closed structures) are connected with the model complete extensions of T. These structures have already appeared several times in the literature.

In §1 we survey the notation and terminology that we use, as well as the well known facts that we require. We also consider several concepts which are not new here but which may not be well known.

In §2 we define, and give the basic results concerning existentially closed structures. For most theories, T, the class ℰ is not elementary and hence is not directly amenable to a model theoretic study. Because of this we consider a smaller class of structures—the uniformly existentially closed structures. These are discussed in §3.

In §4 we look at model complete theories via existentially closed structures. This section is essentially a refinement of parts of [6].

In §5 we look at model companions of theories via existentially closed structures.

Finally, in §6 we make some remarks on the relevance of existentially closed structures to the spectrum problem.

The concepts of ω-consistency and ω-completeness are closely related. The former concept has been generalized to notions of Γ-consistency and strong Γ-consistency, which are applicable not only to formal systems of number theory, but to all functional calculi containing individual constants; and in this general setting the semantical significance of these concepts has been studied. In the present work we carry out an analogous generalization for the concept of ω-completeness.

Suppose, then, that F is an applied functional calculus, and that Γ is a non-empty set of individual constants of F. We say that F is Γ-complete if, whenever B(x) is a formula (containing the single free individual variable x) such that ⊦ B(α) for every α in Γ, then also ⊦ (x)B(x). In the paper “Γ-con” a sequence of increasingly strong concepts, Γ-consistency, n = 1,2, 3,…, was introduced; and it is possible in a formal way to define corresponding concepts of Γn-completeness, as follows. We say that F is Γn-complete if, whenever B(x1,…, xn) is a formula (containing exactly n distinct free variables, namely x1…, xn) such that ⊦ B(α1,…,αn) for all α1,…,αn in Γ, then also ⊦ (X1)…(xn)B(x1,…,xn). However, unlike the situation encountered in the paper “Γ-con”, these definitions are not of interest – for the simple reason that F is Γn-complete if and only if it is Γ-complete, as one easily sees.

If S is a finite set, let ∣S∣ be the cardinality of S. We show that if m ∈ ω, A ⊆ ω, B ⊆ ω, and ∣i: ≤ i ≤ 2m & xi ∈ A}∣ can be computed by an algorithm which, for all x1, …, x2m, makes at most m queries to B, then A is recursive in the halting set K. If m = 1, we show that A is recursive.

Let We be the eth recursively enumerable (r.e.) set in a standard enumeration. The fixed point form of Kleene's recursion theorem asserts that for every recursive function f there exists e which is a fixed point of f in the sense that We = W f(e). In this paper our main concern is to study the degrees of functions with no fixed points. We consider both fixed points in the strict sense above and fixed points modulo various equivalence relations on recursively enumerable sets.

Our starting point for the investigation of the degrees of functions without (strict) fixed points is the following result due to M. M. Arslanov [A1, Theorem 1] and known as the Arslanov completeness criterion. Proofs of this result may also be found in [So1, Theorem 1.3] and [So2, Chapter 12], and we will give a game version of the proof in §5 of this paper.

Theorem 1.1 (Arslanov). Let A be an r.e. set. Then A is complete (i.e. A has degree 0′) iff there is a function f recursive in A with no fixed point.

We present a cut elimination argument that witnesses the conservativity of the compositional axioms for truth (without the extended induction axiom) over any theory interpreting a weak subsystem of arithmetic. In doing so we also fix a critical error in Halbach’s original presentation. Our methods show that the admission of these axioms determines a hyper-exponential reduction in the size of derivations of truth-free statements.

I falsely claimed, as an aside remark in [8] and also implicitly in the abstract [9], that the slow-growing hierarchy

“catches up” with the fast-growing hierarchy

at level Γ0, i.e. that, for all x > 0,

where x′ is some simple (even linear) function of x.

Girard [4] gave the first correct analysis of the deep relationship which exists between G and F, based on his extensive category-theoretic framework for -logic. This analysis indicates that the first point at which G catches up with F is the ordinal of the theory ID<ω(0 of arbitrary finite iterations of an inductive definition. This is very far beyond Γ0! In particular, in order to capture F at level ∣IDn∣ the slow-growing hierarchy must be generated up to ∣IDn+1∣, i.e. one extra iteration of an inductive definition is needed in order to generate sufficient new ordinals.

In the theory of conversion it is important to have a formally defined function which assigns to any positive integer n the least integer not less than n which has a given property. The definition of such a formula is somewhat involved: I propose to give the corresponding formula in λ-K-conversion, which will (naturally) be much simpler. I shall in fact find a formula þ such that if T be a formula for which T(n) is convertible to a formula representing a natural number, whenever n represents a natural number, then þ(T, r) is convertible to the formula q representing the least natural number q, not less than r, for which T(q) conv 0.2 The method depends on finding a formula Θ with the property that Θ conv λu·u(Θ(u)), and consequently if M→Θ(V) then M conv V(M). A formula with this property is,

The formula þ will have the required property if þ(T, r) conv r when T(r) conv 0, and þ(T, r) conv þ(T, S(r)) otherwise. These conditions will be satisfied if þ(T, r) conv T(r, λx·þ(T, S(r)), r), i.e. if þ conv {λptr·t(r, λx·p(t, S(r)), r)}(þ). We therefore put,

This enables us to define also a formula,

such that (T, n) is convertible to the formula representing the nth positive integer q for which T(q) conv 0.

The paper is a continuation of [The SCH revisited], In § 1 we define a forcing with countably many nice systems. It is used, for example, to construct a model “GCH below κ, c f κ = ℵ0, and 2κ > κ+ω” from 0(κ) = κ+ω. In §2 we define a triangle iteration and use it to construct a model satisfying “{μ ≤ λ∣c f μ = ℵ0 and pp(μ) > λ} is countable for some λ”. The question of whether this is possible was asked by S. Shelah. In §3 a forcing for blowing the power of a singular cardinal without collapsing cardinals or adding new bounded subsets is presented. Answering a question of H. Woodin, we show that it is consistent to have “c f κ = ℵ0. GCH below κ, 2κ > κ+, and ”. In §4 a variation of the forcing of [The SCH revisited, §1] is defined. It behaves nicely in iteration processes. As an application, we sketch a construction of a model satisfying:

“κ is a measurable and 2κ ≥ κ+α for some α, κ < c f α < α” starting with 0(κ) = κ+α. This answers the question from Gitik's On measurable cardinals violating the continuum hypothesis.

By [12] we know that transfinite induction up to ΘεΩN+10 is not provable in IDN, the theory of N-times iterated inductive definitions. In this paper we will show that conversely transfinite induction up to any ordinal less than ΘεΩN+10 is provable in IDNi, the intuitionistic version of IDN, and extend this result to theories for transfinitely iterated inductive definitions.

In [14] Schütte proves the wellordering of his notational systems using predicates is wellordered) with Mκ ≔ {x ∈ and 0 ≤ κ ≤ N. Obviously the predicates are definable in IDNi with the defining axioms:

where Prog [Mκ, X] means that X is progressive with respect to Mκ, i.e.

The crucial point in Schütte's wellordering proof is Lemma 19 [14, p. 130] which can be modified to

where TI[Mκ + 1, a] is the scheme of transfinite induction over Mκ + 1 up to a.

The theory of relations was discussed, along with the theory of classes, by Peirce and Schröder. While the calculus of classes has subsequently been presented (by Couturat, and by Huntington) as an abstract mathematical system, no similar formulation has been published of the calculus of relations. Professor Alfred Tarski has proposed to me, the problem of developing a similar formulation for the theory of relations. In this paper I present a set of postulates for the calculus of relations.

The postulates have been chosen so as to enable us to prove Theorem A, below, which asserts a kind of completeness of the system. A set of postulates is called semi-categorical, if every two realizations which involve the same number of elements are isomorphic. From Theorem A one can easily prove that my postulates are semi-categorical, if one assumes the following theorem from Mengenlehre: if α and β are cardinal numbers such that , then α=β. This theorem has not been proved, however, except on the assumption of the axiom of choice and the generalized continuum hypothesis, and is not assumed in the present paper.

It should be pointed out, that the sort of completeness I have chosen is not the only sort, or even necessarily the most interesting sort, of completeness which a set of postulates for the calculus of relations could possess. For example, the question arises, whether it would be possible to find a set of postulates from which all true equations (involving free variables and the operations used by Schröder) could be derived, and which was the weakest possible such set. The present work should therefore be regarded only as a first step in the investigation of the axiomatization of the calculus of relations.

Professor C. I. Lewis, in Lewis and Langford's Symbolic logic, designates the system (S2) determined by the postulates used in Chapter VI—namely, 11.1–7 (B1–7) and

as the system of strict implication. For certain reasons, he prefers it to either the earlier system (S3) determined by the stronger set of postulates of his Survey of symbolic logic, as emended, namely, A1–7 and

or the system (S1) determined by the weaker set of postulates B1–7 or A1–7.

But Lewis and others, following O. Becker, have also given consideration to systems which contain some additional principle effecting the reduction of complex modalities to simpler ones. Notable are the system (S4) determined by B1–7 plus

which includes (is stronger than) S3; and the system (S5) determined by B1–7 plus

which includes S4.

It seems worth while to investigate further the system of the Survey (emended), S3, which is intermediate between S2 and S4. This is the purpose of the present paper. We first prove some additional theorems in S2 and S3. These enable us to reduce all the complex modalities in S3 to a finite number, viz. 42; and it is shown that no further reduction is possible. Finally, several systems which include S3 are considered.

In §1 is given a characterization of strongly hypersimple sets in terms of weak arrays which is in appearance more restrictive than the original definition. §1 also includes a new characterization of hyperhypersimple sets. This one is interesting because in §2 a characterization of dense simple sets is shown which is identical in all but the use of strong arrays instead of weak arrays. Another characterization of hyperhypersimple sets, in terms of descending sequences of sets, is given in §3. Also a theorem showing strongly contrasting behavior for simple sets is presented. In §4 a r-maximal set which is not contained in any maximal set is constructed.

We define classes Φn of formulae of first-order arithmetic with the following properties:

(i) Every φ ϵ Φn is classically equivalent to a Πn-formula (n ≠ 1, Φ1 := Σ1).

(ii)

(iii) IΠn and iΦn (i.e., Heyting arithmetic with induction schema restricted to Φn-formulae) prove the same Π2-formulae.

We further generalize a result by Visser and Wehmeier. namely that prenex induction within intuitionistic arithmetic is rather weak: After closing Φn both under existential and universal quantification (we call these classes Θn) the corresponding theories iΘn still prove the same Π2-formulae. In a second part we consider iΔ0 plus collection-principles. We show that both the provably recursive functions and the provably total functions of are polynomially bounded. Furthermore we show that the contrapositive of the collection-schema gives rise to instances of the law of excluded middle and hence .

We here examine the expressive power of first order logic with generalized quantifiers over finite ordered structures. In particular, we address the following problem: Given a family Q of generalized quantifiers expressing a complexity class C, what is the expressive power of first order logic FO(Q) extended by the quantifiers in Q? From previously studied examples, one would expect that FO(Q) captures LC, i.e., logarithmic space relativized to an oracle in C. We show that this is not always true. However, after studying the problem from a general point of view, we derive sufficient conditions on C such that FO(Q) captures LC. These conditions are fulfilled by a large number of relevant complexity classes, in particular, for example, by NP. As an application of this result, it follows that first order logic extended by Henkin quantifiers captures LNP. This answers a question raised by Blass and Gurevich [Ann. Pure Appl. Logic, vol. 32, 1986]. Furthermore we show that for many families Q of generalized quantifiers (including the family of Henkin quantifiers), each FO(Q)-formula can be replaced by an equivalent FO(Q)-formula with only two occurrences of generalized quantifiers. This generalizes and extends an earlier normal-form result by I. A. Stewart [Fundamenta Inform, vol. 18, 1993].

‘How can we recognize, given axioms and inference rules of a calculus, whether the calculus has such-and-such property?’ A question of this kind arises whenever we deal with a new logic system. For large families of logics, this question may be considered as an algorithmic problem, and a property is called decidable in a given family if there exists an algorithm which is capable of deciding, for a finite axiomatics of a calculus in the family, whether or not it has the property.

In the class of intermediate propositional logics, for instance, nontrivial properties such as the tabularity, pretabularity, and interpolation property (Maksimova [1972, 1977]) are decidable. However, for many other important properties—decidability, finite model property, disjunction property, Halldén-completeness, etc.—effective criteria were not found in spite of considerable efforts.

In this paper we show that the difficulties in investigating these properties in the classes of intermediate logics and normal modal logics containing S4 are of principal nature, since all of them turn out to be algorithmically undecidable. In other words, there are no algorithms which, given a finite set of axioms of an intermediate or modal calculus, can recognize whether or not it is decidable, Halldén-complete, has the finite model or disjunction property.

The first results concerning the undecidability of properties of calculi seem to have been obtained by Linial and Post [1949], who proved the undecidability of the problem of equivalence to classical calculus in the class of all propositional calculi with the same language as the classical one and the two inference rules: modus ponens and substitution. Kuznetsov [1963] generalized this result having proved the undecidability of the problem of equivalence to any fixed intermediate calculus (for instance, to intuitionistic calculus or even the inconsistent one). However, these results will not hold if we confine ourselves only to the class of intermediate logics, though the problem of equivalence to the undecidable intermediate calculus of Shehtman [1978] is clearly undecidable in this class as well.

We give several characterizations of Schnorr trivial sets, including a new lowness notion for Schnorr triviality based on truth-table reducibility. These characterizations allow us to see not only that some natural classes of sets, including maximal sets, are composed entirely of Schnorr trivials, but also that the Schnorr trivial sets form an ideal in the truth-table degrees but not the weak truth-table degrees. This answers a question of Downey. Griffiths and LaForte.

What I am offering here is a reconsideration, and in the end a solution, of the ancient paradox of the Epimenides. What has provoked this new assault on so old a stronghold is L. Jonathan Cohen's [2], in which it is rightly pointed out that the Epimenidean as contrasted with the Eubulidean version of the Liar paradox is the one that threatens logicians who attempt to formalise the use of indirect rather than direct discourse. Among these he includes myself, referring to the system sketched on pp. 130–131 of my [4], and suggesting that I ought to have shown how a person interpreting this system in the obvious way can avoid semantic antinomies. Here too he is right, and my main purpose now is not to criticise his paper, but to fill in this lacuna in my own work to which he has drawn attention. I do want, however, to make one small criticism at the start, namely that Cohen fails to notice what it is that is really paradoxical about the Epimenides, and in consequence fails to perceive the same paradoxical character in a proposition which he is himself quite happy to accept as a ‘logical truth.’

The point about the Epimenides, as was noted by Church in [1], is not that when we examine the truth value of a Cretan's assertion that nothing true is ever asserted by a Cretan we are led to contradictory conclusions, for we are not; the paradox is rather that such examination makes it seem possible to settle an empirical question on logical grounds. If we treat the Cretan's assertion as true, and so assume that nothing true is ever asserted by a Cretan, it follows immediately that the Cretan's assertion is false. If, however, we treat it as false, there is no way of deducing from this assumption that it is true. We can, therefore, consistently suppose it to be false, and this is all that we can consistently suppose. But to suppose it false (considering what the assertion actually is) is to suppose that something asserted by a Cretan is true; and this of course can only be some other assertion than the one mentioned. We thus reach the peculiar conclusion that if any Cretan does assert that nothing asserted by a Cretan is true, then this cannot possibly be the only assertion made by a Cretan — there must also be, beside this false Cretan assertion, some true one.