Generally speaking, it appears correct to say that in a formulation of first order logic in which a large number of connectives are taken as primitive (e.g. ∼, Λ, ∨, ⊃, ∀, ∃ as opposed to ∼, ⊃, ∀, or still more economically, ↓, ∀ proofs within the formal system tend to be smoother and more natural, but the metatheory tends to be that much more elaborate. In [1] we introduced a unifying ‘α, β, γ, δ” notation (which we also used in [2]–[7] and which we briefly review in this paper) which allows us to have our cake and eat it too.

In [11] the constructive ordinals were extended to constructive finite number classes by using systems of notations where mappings at limit ordinals are just partial recursive functions. It turned out that these systems are equivalent, both in terms of ordinals represented and the forms of the sets of notations, to extensions obtained by using mappings at limit ordinals which are partial recursive in (sets of notations for) previously defined number classes. In this article these results are extended to constructive transfinite number classes. We present a system (F, ||) which, in terms of our analogy with the classical ordinals, provides notations for the ordinals less than the first “constructively inaccessible” ordinal, and show that the above equivalence holds at least this far.

The purpose of this paper is to present two new theorems concerning the degrees of coinfinite recursively enumerable (r.e.) sets which have no maximal supersets Let the class of all such degrees be denoted by A. Martin in [2] conjectured that there was some equality or inequality involving a′ or a″ characterizing the degrees a in A. Martin himself proved ([2, Corollary 4.1]) that a′ = 0″ is sufficient for ar r.e. degree a to be in A, and Robinson [3] announced that a′ ≥ 0″ is necessary. In this paper we improve both of these theorems by a factor of the jump, i.e., we shall show that a″ = 0″ is sufficient for an r.e. degree a to be in A, and that a″ ≥ 0″ is necessary.

As those of us who instruct him are well aware, customary accounts of validity and implication for quantificational logic often bewilder the novice. For his benefit, I present here an account of validity, due (in effect) to the late E. W. Beth, and two accounts of implication, one my own, the other Jaakko Hintikka's, which add up to what the better textbooks say, but, making no mention whatever of domains, say it far more simply.

In this note a proof is supplied of a fairly easily-made conjecture: that the system S3.5, formulated by Åqvist in [1] and proved complete with respect to some Kripke-style semantics by Cresswell in [2], is indeed the same system as S3(S), formulated by Lemmon in [3]. Any otherwise unexplained terms and notation are taken from the latter two papers.

This paper is an exposition of the author's [2] investigations of a class of infinitary first order logics. These logics are sometimes characterized by saying that the syntactical role played by the positive integers in first order predicate logic is taken over by a nonstandard model of arithmetic. The result is then called a nonstandard logic.1 In particular the operations of conjunction, disjunction and quantification may be iterated infinitely (nonstandard finitely) often.

When the nonstandard model of arithmetic is an ultra power, the natural class of structures in which to interpret the nonstandard wffs is a class of ultra products. Within this framework, many model-theoretic properties of ultra products become manifest in the logical structure of the nonstandard language.

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.

It is well known that Gödel's famous undecidability result may be viewed in the following strong form. Suppose we are given a specific presentation (i.e., a specific formulation in terms of axioms and rules of inference) of number theory. Then there exists an effective method which, when applied to a consistent axiomatizable extension of the theory yields an undecidable sentence of this extension. For distinct presentations the undecidable sentences obtained would be distinct. This is because the sentence constructed depends upon the notion of proof and hence ultimately upon the axioms and rules of inference—i.e., upon the specific presentation.

In the forthcoming monograph of Crossley [1] the question is raised whether the implication 2 + A = A ⇒ 1 + A = A is true for constructive order types. In this paper a partial answer to this question is given, in that a counterexample is constructed, using, however, not the definition of constructive order type (C.O.T.) given in [1], but an earlier one, namely that in Crossley [2]. The difference is that in [1] only orderings which can be imbedded in a standard dense r.e. ordering R by a partial recursive function are considered. The linear ordering constructed in this paper can be shown not to be such. The problem remains open in the case of orderings imbeddable in R.

It is known that Leśniewski constructed an interpretation of mereology in the real number system using binary expansions.2 Unfortunately, this construction is no longer extant. The following paper, except for a slight variation, is an attempt to reconstruct this interpretation.

Leśniewski probably considered sequences of 0's and I's (except for the sequence of all 0's) and defined a first sequence as an element of the second if every place in which the first has a I, so also does the second.

In this paper we define the notions of invariant implicit definability (i.i.d.) and semi-invariant implicit definability (s.i.i.d.) on ε-models, A, of a certain weak set theory. These notions are intended to be the analogs of recursiveness and recursive enumerability, respectively. Following Barwise, with each A is associated an infinitary language whose formulas are elements of A.

The well-known incompleteness results of Gödel assert that there is no recursively enumerable set of sentences of formalized first order arithmetic which entails all true statements of that theory. It is equally well known that by introducing sufficiently nonconstructive rules, such as the ω-rule of induction, completeness can be re-established.

Starting from the work of Turing [4] Feferman in [1] developed another method, viz. the study of transfinite recursive progressions of theories, for closing the gap between Gödel (recursively enumerable sets of axioms yield incompleteness) and Tarski (number-theoretic truth is not arithmetically definable).

Acquaintance with [11] and [8] will be assumed. Let be the alphabet →, &, ν, ┐, (,), A1, A2, … where →(I), &(C), ν (D) and ┐(N) are called the connectives. The letters appearing in parentheses are the names of the connectives. A1, A2 … are the atoms.

Definition 1.1. A string S is an ICDN word iff there is a finite sequence of strings S1 … Sn = S such that for i, 1 ≤ i ≤ n, either S1 is an atom or S1 is one of the forms (S1→Sk), (S1 & Sk), (S1, ν Sk) or ┐S1,j, k ≤ i.

I shall prove in this paper that Gentzen's Hauptsatz is extendible to simple type theory, i.e., to the predicate logic obtained by admitting quantification over predicates of arbitrary finite type and generalizing the second order quantification rules to cover quantifiers of other types. (That Gentzen's Hauptsatz is extendible to this logic has been known as Takeuti's conjecture; see [4].) Gentzen's Hauptsatz has been extended to second order logic in a recent paper by Tait [3]. However, as remarked by Tait, his proof seems not to be extendible to higher orders. The present proof is rather an extension of a different proof of the Hauptsatz for second order logic that I have presented in [1].

Kripke's model structure for D2 is a quadruple (G, K, R, N) where N is the set of normal elements, i.e., the subset of K such that for every H in N, HRH. (See [1, p. 220, p. 211].) In fact, however, this structure provides a model for E2, as the work of Lemmon shows ([2, pp. 58–62]).

To show the inadequacy of Kripke's model structure, we show that the E2 thesis □B ⊃ B, not a thesis of D2, is valid under Kripke's modelling for D2. Suppose, for a reductio argument, that □ B ⊃ B is false for some valuation ϕ in some D2 model structure. Thenyϕ(□B ⊃ B, G) = F; so by truth-functional assignments

§1. The set Cn(R, A + X) is the set of all expressions deducible, on the ground of formulas A, from the class X of formulas of the implicational propositional calculus, by means of rules belonging to the set R. In other words, Cn(R, A + X) is the set of expressions obtained from the set X by the help of a two-parameter function Cn[R, A]. The formula is called the classical deduction theorem.

The classical deduction theorem is true for the system 〈R, A〉 (where R is the set of primitive rules, A is the set of axioms of the propositional calculus) if it holds for the function Cn[R, A].

“Apart from merits or defects of PA1, however, its existence demonstrates the feasibility of a new approach to the logic of propositions involving the principle of subjunctive contrariety. We thus have good reason to investigate the effect this principle, and a concept of conditionality compatible with it, might exert if introduced into standard quantification theory, into set theory, into modal logic and into epistemology and the philosophy of science.”

Kanger [4] gives a set of twelve axioms for the classical prepositional calculus which, together with modus ponens and substitution, have the following nice properties:

(0.1) Each axiom contains =⊃, and no axiom contains more than two different connectives.

(0.2) Deletions of certain of the axioms yield the intuitionistic, minimal, and classical refutability1 subsystems of propositional calculus.

In [1], Lemmon provides us with his now well-known formulations of the Lewis-modal systems S1 through S4. This paper will present similar bases for the related systems S1° and S2° of Feys [2], and S3° and S4° of Sobocinski [3]. Notation and definitions here will be as in [1]. Standard bases for the Lewis-modal systems may be drawn from the following stock of axioms and rules, as is done in [1].

In the original formulations of Lewis's S1–S5 in [1], Feys's S1°, S2° in [2], and Sobociński's S3°, S4° in [3], a primitive rule is that of replacement for strict equivalents which it is enough to express formally as:

RI: where γ′ is like γ except for having β at one place where γ has α.