The following describes a calculus of sequents (SLK) patterned after the calculus LK of Gentzen in [1] but restricted to the formulas of propositional logic and modified so that the only connective is the Sheffer stroke. The ‘elimination theorem’ (Hauptsatz) is proved for SLK and a decision procedure is specified for determining whether a given formula in stroke notation is tautologous. In addition, SLK is proved consistent and complete. Subsequent remarks indicate briefly how the calculus can be modified so as to employ the dagger as the only connective.

By functional equation we mean an equation of the form

(1)A1 … Aκ = B1 … B1.

Here the A's and B's are functions of one variable from and to the natural numbers and FG is the function obtained from F and G by composition, i.e. FG(x) = F(G(x)) for all natural numbers x. We wish to investigate finite systems of functional equations. Now if all the A's and B's of (1) are equal to the identity function I (or all equal to the zero function O), then the equation (1) is satisfied trivially. Thus, in order to make the problem of solvability of systems of equations interesting, we must have some function given which will be held fixed throughout. We take the successor function S to be this given function.

In this paper we study some of the consequences of adding as new axioms to consistent re (recursively enumerable) extensions T of Peano arithmetic P sentences undecidable in T of the Π10 variety, as are those one naturally comes upon. The question arises: how much can two extensions “differ” when each is obtained by adding just once distinct Π10 sentences undecidable in T? We shall show that if T is as stated above, we can find extensions T1 and T2, constructed very simply from T, having the property that if (A, B) is any pair of re sets with recursive intersection, there can be found a Π10 formula of P which represents A in T1 and B in T2.

We wish to make a correction to our paper On definability of ordinals in logic with infinitely long expressions (this journal, vol. 31 (1966), pp. 365–375). Let Ω be an infinite singular cardinal and Ω+ the smallest cardinal >Ω. For the proof of the second half of Theorem 3, we incorrectly assumed that an ordinal γ is not definable in LΩ, if γ is not cofinal with any ordinal ≤Ω. However, Ω+ is indeed definable in LΩ and Theorem 3 should read:

If Ω singular, then an ordinal α is definable in Lα, if and only if σ ≤ exp(Ω+, Ω+), where exp (β,γ) denotes ordinal exponentiation βγ.

It is well known that the familiar Sheffer stroke function of the 2-valued propositional calculus is functionally complete (i.e., for any m, all 22m truth functions of m variables can be defined1 in terms of the stroke function). Indeed, it is not difficult to show that of the 16 2-valued functions of two variables, exactly two of them are functionally complete.

The presence of a rule for existential instantiation (EI) in a system of natural deduction often causes some difficulties, in particular, when it comes to formulate necessary restrictions on the rule for universal generalization (UG). A system containing rules for EI and UG that avoided Quine's rather cumbersome restrictions on these rules was formulated by Copi [2], but the system was found to be inconveniently restrictive. A less restrictive system was therefore suggested by Copi [3]. Also that system forces some deductions to be unnecessarily long as is shown in Prawitz [5, Appendix C, p. 104], where a way to liberalize Copi's restriction on UG is suggested (p. 105). However, the system suggested by Copi [3] is also incorrect (i.e. unsound) as has recently been shown by Parry [4] in this Journal.

The law of infinite conjunction (Quine's name, see Methods of logic, rev. ed., Holt & Co., New York, p. 254) says that a set of truthfunctional formulas is satisfiable provided every finite subset is. We give a proof of the law which uses some properties of the perfect disjunctive normal form.

Any satisfiable formula can be written as a disjunction of conjunctions of literals (a literal is a statement-letter or the negation of one) in which a statement-letter which occurs in any conjunction occurs exactly once in each; a literal by itself counts as a conjunction and a conjunction by itself as a disjunction.

In [1] Ludwik Borkowski takes a quantifier symbol ‘Q1’ (e.g., the familiar ‘∀’) to permit definition of another quantifier symbol ‘Q1’ if, where ‘f’ is a singulary predicate variable, there exists a formula A of QC1—a first-order quantificational calculus (without identity and individual constants) having ‘Q1’ as its one primitive quantifier symbol—such that: (1) under the intended interpretations of ‘Q1’ and ‘Q1’ the biconditional (Q1X)f(X) = A is valid, (2) no individual variable occurs free in A, and (3) A contains no propositional variable, and no predicate variable other than ‘f.’

Student. I've been studying the logic of classes, and can't see how any class can be included in its own complement.

Teacher. Surely you've heard of the null class, which is included in every class, and hence in its own complement?

Student. That also strikes me as somehow implausible. How do you define ‘inclusion’?

Teacher. In the usual way. a is included in b if and only if the intersection of a with the complement of b is null.

This paper answers affirmatively the open question of Massey [1] concerning the existence of binary connectives functionally complete by themselves in two-valued truth tabular logic, i.e. in the modal theory S5. Since {∼, ⊃, ◊} is a functionally complete set of connectives (Massey [1, § 4]), the following definitions show that the binary operator ф, the semantics of which is given below, is functionally complete by itself:

It is left to the reader to verify, by means of complete sets of truth tables (see Massey [1, §§ 1 and 3]), that the foregoing definitions are correct.

T0 will denote Gödel's theory T[3] of functionals of finite type (f.t.) with intuitionistic quantification over each f.t. added. T1 will denote T0 together with definition by bar recursion of type o, the axiom schema of bar induction, and the schema

of choice. Precise descriptions of these systems are given below in §4. The main results of this paper are interpretations of T0 in intuitionistic arithmetic U0 and of T1 in intuitionistic analysis is U1. U1 is U0 with quantification over functionals of type (0,0) and the axiom schemata AC00 and of bar induction.

At the Princeton Bicentennial in 1946 Tarski posed the question as to whether or not certain problems connected with partial propositional calculi were recursively solvable. Since that time the specific problems mentioned by Tarski as well as a number of related problems have been shown to be recursively unsolvable. Such results are due to Post and Linial [5], Yntema [9], Gladstone [2], Ihrig [3] and Singletary [7], [8].

The notion of strong reduction is introduced in Curry and Feys' book Combinatory logic [1] as an analogue, in the theory of combinatore, to reduction (more exactly, βη-reduction) in the theory of λ-conversion. The existence of an analogue and its possible importance are suggested by an equivalence between the theory of combinatore and λ-conversion, and the Church-Rosser theorem in λ-conversion. This theorem implies that if a formula X is convertible to a formula X* which cannot be further reduced—is irreducible, or in normal form—then X is convertible to X* by a reduction alone. Moreover, the reduction may be performed in a certain prescribed order.

As anyone who is familiar with the literature knows, there is a great deal of controversy concerning which, if any, of the extant theories of propositional modal logic correctly formalizes the logic of certain logical concepts such as analyticity and logical necessity. Most of the controversy concerns certain principles that involve iterated modalities (where one modal operator occurs within the scope of another). For example, there is considerable disagreement about whether the principle (□p⊃□□p) should be considered valid. However, when philosophers and logicians apply modal logic to concrete problems, they rarely need principles which involve iterated modalities. For most practical purposes, principles involving only one layer of modalities are all that are needed. This suggests that if we try to construct a theory of modal logic in which there are no iterated modalities, we can avoid most of the controversy and still have a theory that is strong enough for all of the normal uses to which modal logic is put.

1.1. The aim of this paper is the construction of a demonstrably consistent system of set theory that (1) contains roughly the same amount of mathematics as the writer's system K′ [3], including a theory of continuous functions of real numbers, and (2) provides a way for expressing in the object language various propositions which, in the case of K′, could be expressed only in the metalanguage, for example, general propositions about all real numbers. It was not originally intended that the desired system should be a modal logic, but the modal character of the system appears to be a natural outgrowth of the way it is constructed. A detailed treatment of the natural, rational, and real numbers is left for a subsequent paper.