The main concern of this paper is the design of a noetherian and confluent normalization for LK2 (that is, classical second order predicate logic presented as a sequent calculus).

The method we present is powerful: since it allows us to recover as fragments formalisms as seemingly different as Girard's LC and Parigot's λμ, FD ([10, 12, 32, 36]), delineates other viable systems as well, and gives means to extend the Krivine/Leivant paradigm of ‘programming-with-proofs’ ([26, 27]) to classical logic; it is painless: since we reduce strong normalization and confluence to the same properties for linear logic (for non-additive proof nets, to be precise) using appropriate embeddings (so-called decorations); it is unifying: it organizes known solutions in a simple pattern that makes apparent the how and why of their making.

A comparison of our method to that of embedding LK into LJ (intuitionistic sequent calculus) brings to the fore the latter's defects for these ‘deconstructive purposes’.

LK is a natural modification of Gentzen sequent calculus for propositional logic with connectives ¬ and ∧,∨ (both of bounded arity). Then for every d ≥ 0 and n ≥ 2, there is a set of depth d sequents of total size O(n3+d) which are refutable in LK by depth d + 1 proof of size exp(O(log2n)) but such that every depth d refutation must have the size at least exp(nΩ(1)). The sets express a weaker form of the pigeonhole principle.

A proof that certain systems of formal logic are inconsistent, in the sense that every formula expressible in them is provable, was published by Kleene and Rosser under the above title in 1935. For the case where the underlying system satisfies an additional condition—viz. the possession of an operator analogous to Schönfinkel's K—I gave a simpler derivation of this condition in a previous paper. That argument, like the original one of Kleene and Rosser, was a refinement of the Richard paradox. The object of the present paper is to show that, if we use other paradoxes, an inconsistency will result from a very much simpler argument and on much less restrictive hypotheses. The contradiction can no longer be called “the paradox of Kleene and Rosser,” because it is based on an entirely different principle; but, in deference to the work of the original discoverers of the inconsistency, the paper is given the same title as that which their paper bears. The central idea of the new derivation was suggested by some work of R. Carnap.

This paper is based on the one above cited, which will be referred to as PKR. However, acquaintance with that paper will be presupposed only through 3.4, i.e., through the statement of the basic hypotheses and conventions for a combinatorially complete system—except that for the second (alternative) method of construction given below the substance of PKR through 9.6 is needed.

The system RM is the most well-understood (and to our opinion, also the most important) system among the logics developed by the Anderson and Belnap school. In this paper we investigate RM from a constructive point of view. For example, we give a new proof of the completeness of RM relative to the Sugihara matrix (first shown by Meyer), a proof in which a p.r. procedure is presented, applying which to a sentence A in RM language yields either a proof of it in RM or a refuting valuation for it in the Sugihara matrix SZ.

Two topics dealt with in this work deserve a special attention.

a) The admissibility of γ. This is a famous theorem of Meyer and Dunn. In [1] Anderson and Belnap emphasize that “the Meyer-Dunn argument … guarantees the existence of a proof of B, but there is no guarantee that the proof of B is related in any sort of plausible way to the proofs of A and Ā ∨ B.” In §2 we provide such a guarantee for the RM-case. In fact, we give there a direct method of obtaining a proof of B from given proofs of A and Ā ∨ B.

b) The relationships betweenRMand its full negation-implication fragment. RM is known ([1, pp. 148–149], and [3]) to be a conservative extension of (Sobociński 3-valued logic; see [4]). Anderson and Belnap admit [1, p. 149] that this fact came to them as a distinct surprise, since RM as a whole is far from being three-valued. In this paper, however, this “surprising” fact appears quite natural (see III.3). In fact, we show that , is the “hard core” of RM, since our proof of the completeness of RM is based in an essential way on the completeness of relative to the Sobociński matrix, and since the Gentzen-type calculus we develop for RM is a direct extension of a similar (but much simpler) calculus for . Because of the importance has in this work, we devote the first section to a constructive investigation of it.

We note, finally, that the Gentzen-type calculus mentioned above admits cut-elimination and normal-form techniques. (Such calculi were found till now only for RM without distribution.)

This paper presents a unified treatment of the propositional and first-order many-valued logics through the method of tableaux. It is shown that several important results on the proof theory and model theory of those logics can be obtained in a general way.

We obtain, in this direction, abstract versions of the completeness theorem, model existence theorem (using a generalization of the classical analytic consistency properties), compactness theorem and Löwenheim-Skolem theorem.

The paper is completely self-contained and includes examples of application to particular many-valued formal systems.

We give two proofs of strong normalisation for second order classical natural deduction. The first one is an adaptation of the method of reducibility candidates introduced in [9] for second order intuitionistic natural deduction; the extension to the classical case requires in particular a simplification of the notion of reducibility candidate. The second one is a reduction to the intuitionistic case, using a Kolmogorov translation.

Our principal result is that there exist two incomparable recursively enumerable degrees whose greatest lower bound in the upper semilattice of degrees is 0. This was conjectured by Sacks [5]. As a secondary result, we prove that on the other hand there exists a recursively enumerable degree a < 0(1) such that for no non-zero recursively enumerable degree b is 0 the greatest lower bound of a and b.

The proof of the main theorem involves a method that we have developed elsewhere [8] to deal with situations in which a partial recursive functional may interfere infinitely often with an opposed requirement of lower priority.

Consider those structures that consist of a countable universe and a finite number of predicates and functions. Let = ‹∣∣, P1, …, Pn, f1, …, fm› be such a structure. We will restrict our consideration to structures, , whose universe, ∣∣, is a set of natural numbers, and thus we will be able to apply the notions of recursion theory to structures. Using deg(S) to refer to the degree of unsolvability of a set S, we can assign a degree of unsolvability to the structure by defining deg() to be the least upper bound of the degrees of the universe, predicates, and functions of . If we view as a presentation of the class of all structures which are isomorphic to (in the usual sense), then the deg() can be called the degree of the presentation.

While deg() is a natural degree to assign to the structure , it is not the only possibility. Indeed since a structure may have isomorphic presentations with different degrees, deg() has the deficiency of not being isomorphically invariant. We can assign degrees to some (but not all) structures in an isomorphically invariant fashion by looking at the class of the degrees of all presentations isomorphic to . If this class of degrees has a least element, we define it to be the degree of the isomorphism class of which we write deg([]).

We prove that the statement “For every pair A, B, stationary subsets of ω2, composed of points of cofinality ω, there exists an ordinal α such that both A ∩ α and B ∩ α are stationary subsets of α is equiconsistent with the existence of weakly compact cardinal. (This completes results of Baumgartner and Harrington and Shelah.)

We also prove, assuming the existence of infinitely many supercompact cardinals, the statement “Every stationary subset of ωω+1 has a stationary initial segment.”

A categorical structure suitable for interpreting polymorphic lambda calculus (PLC) is defined, providing an algebraic semantics for PLC which is sound and complete. In fact, there is an equivalence between the theories and the categories. Also presented is a definitional extension of PLC including “subtypes”, for example, equality subtypes, together with a construction providing models of the extended language, and a context for Girard's extension of the Dialectica interpretation.

There are logicians who maintain that modal logic violates Leibniz's principle that if x and y are identical, then y has every property of x. The alleged difficulty is illustrated in the following example due to Quine.1

A. It is logically necessary that 9 is less than 10.

B. 9 = the number of the planets.

C. Therefore, it is logically necessary that the number of the planets is less than 10.

In previous articles ([4], [5]) it has been shown that the deductive system developed by Aristotle in his “second logic” (cf. Bochenski [2, p. 43]) is a natural deduction system and not an axiomatic system as previously had been thought [6]. It was also pointed out that Aristotle's logic is self-sufficient in two senses: First, that it presupposed no other logical concepts, not even those of propositional logic; second, that it is (strongly) complete in the sense that every valid argument formable in the language of the system is demonstrable by means of a formal deduction in the system. Review of the system makes the first point obvious. The purpose of the present article is to prove the second. Strong completeness is demonstrated for the Aristotélian system.

Suppose the ri-placed relation symbols Pi, 1 ≦ i ≦ k, are all the non-logical constants occurring in the closed formula , also written as , of Heyting's predicate calculus (HPC). Then HPC is called complete for provided , i.e.

Here D ranges over arbitrary species, and over arbitrary (possibly incompletely defined) subspecies of ;

We give a sound and complete axiomatization for the full computation tree logic. CTL*, of R-generable models. This solves a long standing open problem in branching time temporal logic.

Interpretability in reflexive theories, especially in PA, has been studied in many papers; see e.g. [3], [6], [7], [10], [11], [15], [26]. It has been shown that reflexive theories exhibit many nice properties, e.g. (1) if T, S are recursively enumerable reflexive, then T is interpretable in S iff every Π1 sentence provable in T is provable in S; and (2) if S is reflexive, T is recursively enumerable and locally interpretable in S (i.e. every finite part of T is interpretable in S), then T is globally interpretable in S (Orey's theorem, cf. [3]).

In this paper we want to study such statements for nonreflexive theories, especially for finitely axiomatizable theories (which are never reflexive). These theories behave differently, although they may be quite close to reflexive theories, as e.g. GB to ZF. An important fact is that in such theories one can define proper cuts. By a cut we mean a formula with one free variable which defines a nonempty initial segment of natural numbers closed under the successor function. The importance of cuts for interpretations in GB was realized already by Vopěnka and Hájek in [30]. Pioneering work was done by Solovay in [24]. There he developed the method of “shortening of cuts”. Using this method it is possible to replace any cut by a cut which is contained in it and has some desirable additional properties; in particular it can be closed under + and ·. This introduces ambiguity in the concept of arithmetic in theories which admit proper cuts, namely, which cut (closed under + and ·) should be called the arithmetic of the theory? Cuts played the crucial role also in [20].

The linear logic introduced in [3] by J.-Y. Girard keeps one of the so-called structural rules of the sequent calculus: the exchange rule. In a one-sided sequent calculus this rule can be formulated as

The exchange rule allows one to disregard the order of the assumptions and the order of the conclusions of a proof, and this means, when the proof corresponds to a logically correct program, to disregard the order in which the inputs and the outputs occur in a program.

In the linear logic introduced in [3], the exchange rule allows one to prove the commutativity of the multiplicative connectives, conjunction (⊗) and disjunction (⅋). Due to the presence of the exchange rule in linear logic, in the phase semantics for linear logic one starts with a commutative monoid. So, the usual linear logic may be called commutative linear logic.

The aim of the investigations underlying this paper was to see, first, what happens when we remove the exchange rule from the sequent calculus for the linear propositional logic at all, and then, how to recover the strength of the exchange rule by means of exponential connectives (in the same way as by means of the exponential connectives ! and ? we recover the strength of the weakening and contraction rules).

Dugundji has proved that none of the Lewis systems of modal logic, S1 through S5, has a finite characteristic matrix. The question arises whether there exist proper extensions of S5 which have no finite characteristic matrix. By an extension of a sentential calculus S, we usually refer to any system S′ such that every formula provable in S is provable in S′. An extension S′ of S is called proper if it is not identical with S. The answer to the question is trivially affirmative in case we make no additional restrictions on the class of extensions. Thus the extension of S5 obtained by adding to the provable formulas the additional formula p has no finite characteristic matrix (indeed, it has no characteristic matrix at all), but this extension is not closed under substitution—the formula q is not provable in it. McKinsey and Tarski have defined normal extensions of S4* by imposing three conditions. Normal extensions must be closed under substitution, must preserve the rule of detachment under material implication, and must also preserve the rule that if α is provable then ~◊~α is provable. McKinsey and Tarski also gave an example of an extension of S4 which satisfies the first two of these conditions but not the third. One of the results of this paper is that every extension of S5 which satisfies the first two of these conditions also satisfies the third, and hence the above definition of normal extension is redundant for S5. We shall therefore limit the extensions discussed in this paper to those which are closed under substitution and which preserve the rule of detachment under material implication. These extensions we shall call quasi-normal. The class of quasi-normal extensions of S5 is a very broad class and actually includes all extensions which are likely to prove interesting. It is easily shown that quasi-normal extensions of S5 preserve the rules of replacement, adjunction, and detachment under strict implication. It is the purpose of this paper to prove that every proper quasi-normal extension of S5 has a finite characteristic matrix and that every quasi-normal extension of S5 is a normal extension of S5 and to describe a simple class of characteristic matrices for S5.

This paper is a sequel to [7], and the terminology of [7] is largely presupposed here. In [7], the algebraic methods of McKinsey-Tarski were employed and extended to yield semantic results of a Kripke kind for a class of relatively weak modal logics, the strongest of which was the Feysvon Wright system T. Deontic versions of both T and E2, called T(D) and D2, and even weaker systems, were handled. The main aim of the present paper is to extend these results to stronger systems of modal logic. Thus the Lewis systems S2–S5, the Brouwersche system B of Kripke [4], the systems E3–E5 of [5], and Łukasiewicz's modal logic, as well as certain new systems, are considered.

Certain modifications of the method of [7] have proved convenient. Thus in Section I, some further results concerning model structures are proved in order that the relationship between S2 and E2, S3 and E3, can be properly stated; in particular, the notions of a refined and connected model structure play a pervasive role throughout.

The purpose of this paper is to analyze rational betting. In particular, we concentrate on one necessary feature of rational betting, the avoidance of certainty of losing to a clever opponent. If a bettor is quite foolish in his choice of the rates at which he will bet, ah opponent can win money from him no matter what happens.

This phenomenon is well known to professional bettors—especially bookmakers, who must as a matter of practical necessity avoid its occurrence. Such a losing book is called by them a “dutch book.” Our investigations are thus concerned with necessary and sufficient conditions that a book not be “dutch.”

De Finetti [3] has started with the same idea and used it as a foundation for the theory of probability. It is our aim to consider the same subject more precisely and attempt to answer some questions about desirable features of a confirmation function. We wish to connect the ideas of De Finetti with those of Carnap [1] and Hossiasson-Lindenbaum [6]. The results expressed by Theorem 1 are essentially contained in De Finetti's work. Theorems 3 and 4 seem to be new.

The confirmation functions which we consider will be functions with two sentences as arguments taking real numbers as values. Intuitively, C(h, e) will represent the rate at which a bettor would be willing to bet on the hypothesis h if he knew the information expressed by the sentence e, the evidence.

In monomodal logic there are a fair number of high-powered results on completeness covering large classes of modal systems; witness for example Fine [74], [85] and Sahlqvist [75]. Monomodal logic is therefore a well-understood subject in contrast to polymodal logic, where even the most elementary questions concerning completeness, decidability, etc. have been left unanswered. Given that in many applications of modal logic one modality is not sufficient, the lack of general results is acutely felt by the “users” of modal logics, contrary to logicians who might entertain the view that a deep understanding of one modality alone provides enough insight to be able to generalize the results to logics with several modalities. Although this view has its justification, the main results we are going to prove are certainly not of this type, for they require a fundamentally new technique. The results obtained are called transfer theorems in Fine and Schurz [91] and are of the following type. Let L ∌ ⊥ be an independently axiomatizable bimodal logic and L⎕ and L∎ its monomodal fragments. Then L has a property P iff L⎕ and L∎ have P. Properties which will be discussed are completeness, the finite model property, compactness, persistence, interpolation and Halldén-completeness. In our discussion we will prove transfer theorems for the simplest case when there are just two modal operators, but it will be clear that the proof works in the general case as well.