§1. In [1] Gödel proves the non-existence of a finite matrix characteristic for the intuitionist propositional calculus IC by the use of the finite matrices , where n is a natural number and

The system of sentential calculus presented below has peculiarities which may be of some interest. It is complete in the sense that every classical (two-valued) tautology is provable. In spite of this it is not Post complete (nor is it absolutely complete), i.e., one can add to the system an unprovable formula without proving a sentential variable as a theorem (or without making every formula a theorem). Thus the system may be extended by adjoining an unprovable formula without making the system inconsistent in the Post (or in absolute) sense. There are many distinct extensions of this kind. For every formula α1 that is not a theorem and which adjoined to the system does not make the system Post (or absolutely) inconsistent there is a formula α2 such that adjunction of α2 to the original system leaves α1 unprovable.

In this paper it is shown that, if a certain form of Gödel-Bernays set theory which does not include the axiom of extensionality is consistent, then so is the whole system of set theory. The general line of argument is similar to that used in Part I. § 1 describes a reformulation of set theory in which the class-existence axioms are replaced by the use of abstracts. In § 2 some standard theorems, including the theory of the ancestral, are proved without using the axiom of extensionality. In § 3 the appropriate inner model is defined, and the validity in it of the most of the axioms is demonstrated. § 4 deals with the remaining axioms (of infinity and of choice).

The present paper attempts to state and prove a completeness theorem for the system S5 of [1], supplemented by first-order quantifiers and the sign of equality. We assume that we possess a denumerably infinite list of individual variables a, b, c, …, x, y, z, …, xm, ym, zm, … as well as a denumerably infinite list of n-adic predicate variables Pn, Qn, Rn, …, Pmn, Qmn, Rmn,…; if n=0, an n-adic predicate variable is often called a “propositional variable.” A formula Pn(x1, …,xn) is an n-adic prime formula; often the superscript will be omitted if such an omission does not sacrifice clarity.

In [1], it is conjectured that if S is a sentence in the first-order functional calculus with identity, and every subsystem of every finite relational system which satisfies S also satisfies S, then S is finitely equivalent to a universal sentence. (Two sentences are finitely equivalent if and only if they are satisfied by the same finite relational systems.) The following sentence S refutes that conjecture, and moreover S is satisfied by all finite subsystems of all (finite or infinite) relational systems which satisfy it.1S contains as predicate letters only the two-place predicate letters ≦, R (and the identity symbol =).

In this note we present an axiomatization of the classical two-valued propositional calculus, for which proofs of decidability, consistency, completeness, and independence, are almost trivial (given an understanding of truth tables).

Following a suggestion of Feys, we use “rigorous implication” as a translation of Ackermann's strenge Implikation ([1]). Interest in Ackermann's system stems in part from the fact that it formalizes the properties of a strong, natural sort of implication which provably avoids standard implicational paradoxes, and which is consequently a good candidate for a formalization of entailment (considered as a narrower relation than that of strict implication). Our present purpose will not be to defend this suggestion, but rather to present some information about rigorous implication. In particular, we show first that the structure of modalities (in the sense of Parry [4]) in Ackermann's system is identical with the structure of modalities in Lewis's S4, and secondly that (Ackermann's apparent conjecture to the contrary notwithstanding) it is possible to define modalities with the help of rigorous implication.

By quite elementary means, one can find “large” examples difficult, if not (for practical purposes) impossible, to be managed by that host of methods, after Quine, for minimizing expressions in alternational normal form. Because the workability rather than existence of an algorithm for minimizing logical formulae is generally critical, it may be pertinent to outline briefly the derivation of these “large” examples. Some more general insight may also be gained about simplification techniques.

Venn constructed diagrams of up to five simply connected regions that overlapped each other once in each possible way of overlapping. Although Venn did not prove that his diagrams were constructible for more than five simply connected regions — in fact, he preferred to have a doubly connected region in his 5-class diagram — he summarized his method of construction with an intuitive argument: “But for merely theoretical purposes the rule of formulation would be very simple. It would merely be to begin by drawing any closed figure, and then proceed to draw others, subject to the one condition that each is to intersect once and once only all the existing subdivisions produced by those which had gone before.” The method of construction given below leads to a simple topological proof that Venn diagrams can be constructed for any number of simply connected regions.

Eine auf neue Art und mit neuen symbolischen Mitteln durchgeführte Analyse des Prozesses der Prädikation ergibt, daβ das für die logisch-mengentheoretischen Paradoxa nach Art des Russellschen essentielle Moment weder das der Selbstprädikation als solches ist noch irgendetwas, was man anderweitig bisher für sie verantwortlich gemacht hat, sondern vielmehr der Umstand, daβ der Algorithmus der Prädikation ebensowohl wie zu einem natürlichen Abschluβ auch auf einen unendlichen Regreβ führen kann. Damit werden die genannten Paradoxa als den bekannten erledigten der mathematischen unendlichen Prozesse wesentlich gleichartig und der gleichen Behandlung zugänglich erkannt. Das neue Kalkülmittel der limitierten Variablen bewirkt – ohne irgendwelche metalogische Regulative ad hoc – die automatische Sicherung des logischen Kalküls gegen die früheren Verführungen.

By intermediate prepositional logics we mean prepositional logics between the intuitionistic and classical logics.

K. Gödel [1] proved that there is a set of intermediate prepositional logics which possesses the order type ω. The method enables us to define intermediate logics in terms of axioms and rules of inference. We shall call it the axiomatic method.

In [1] and [2] I investigated logics intermediate between intuitionistic and classical propositional logic. In the present paper I shall study inclusion and non-inclusion between certain intermediate predicate logics. All the logics considered result from intuitionistic predicate logic by addition of classically valid axiom schemes.

Independence of axioms was not investigated in [Faris]. We show that this quality is lacking, since 2 can be derived from the rest, which without it constitute an independent set. In the proofs of independence it is clearly more informative to decompose 9, C1abKN2abKN3abN5ab and 10, C3abKN2abN5ab into three and two propositions respectively.

Horn [2] obtained a sufficient condition for an elementary class to be closed under direct product. Chang and Morel [1] showed that this is not a necessary condition. We will show that, if consideration is restricted to identity theory, that is, a first-order predicate calculus with equality but no other relation symbols or operation symbols, Horn's condition is necessary and sufficient.

A model for identity theory consists of a non-empty domain A, but no relations or operations except equality. If I is an index set, and for each is a model for identity theory, then the direct product of the is a model for identity theory and has domain A, the cartesian product of the Ai.

Ackermann introduced in [1] a system of axiomatic set theory. The quantifiers of this set theory range over a universe of objects which we call classes. Among the classes we distinguish the sets. Here we shall show that, in some sense, all the theorems of Ackermann's set theory can be proved in Zermelo-Fraenkel's set theory. We shall also show that, on the other hand, it is possible to prove in Ackermann's set theory very strong theorems of the Zermelo-Fraenkel set theory.

According to Kleene [8] and Post [13] the definition of recursive relations (or sets) can be given most simply via the definition of recursively enumerable (r.e.) relations. The latter can be defined by finite systems of finite rules for deriving strings of symbols, each rule being of the form

each formula or being obtained by juxtaposition from atomic symbols and variables ranging over strings of atomic symbols.