In this paper we shall use a logic with truth values ranging over all the real numbers x such that 0 ≦ x ≦ 1.1 will be “complete truth” and 0 will be “complete falsity.” The primitive sentential connectives are ‘⊃’ and ‘∼’; other connectives are ‘∨’ and ‘·’. Assume that ‘p’ and ‘q’ are sentential variables, whose truth values are respectively x and y. Then

1.1. ‘p ⊃ q’ has the value min(1 − x + y, 1),

1.2. ‘∼p’ has the value 1 − x,

1.3. ‘p∨q’ has the value max(x, y), and

1.4. ‘p·q’ has the value min (x, y).

‘∨’ and ‘·’ can be defined as follows:

It is the purpose of this paper to prove a theorem which will be stated in the next section. The following symbolism and convention will be used throughout the paper:

S is a logical formula.

ν (S) is the value of S.

‘p’, ‘pi1, ’p2, …, ‘q’, are sentential variables.

ν(p) = x and ν(x1) = x1, etc.

ν(S) = σ and ν(S1) = σ1, etc.

If S contains the sentential variables ‘p1’, ‘p2’, …, then we write for S, S(p1, P2, …). Also ν{S(p1, p2, …)) = σ(x1, x2, …).

A logical formula is defined in the usual manner. 1. A sentential variable is a logical formula; 2. if S is a logical formula then ·S is a logical formula; and 3. if S and S′ are logical formulae then (S ⊃ S′) is a logical formula.

One of the standard ways of proving the consistency of additional hypotheses with the basic axioms of an axiom system is by the construction of what may be described as ‘inner models.’ By starting with a domain of individuals assumed to satisfy the basic axioms an inner model is constructed whose domain of individuals is a certain subset of the original individual domain. If such an inner model can be constructed which satisfies not only the basic axioms but also the particular additional hypothesis under consideration, then this affords a proof that if the basic axiom system is consistent then so is the system obtained by adding to this system the new hypothesis. This method has been applied to axiom systems for set theory by many authors, including v. Neumann (4), Mostowski (5), and more recently Gödel (1), who has shown by this method that if the basic axioms of a certain axiomatic system of set theory are consistent then so is the system obtained by adding to these axioms a strong form of the axiom of choice and the generalised continuum hypothesis. Having been shown in this striking way the power of this method it is natural to inquire whether it has any limitations or whether by the construction of a sufficiently ingenious inner model one might hope to decide other outstanding consistency questions, such as the consistency of the negations of the axiom of choice and continuum hypothesis. In this and two following papers we prove some general theorems concerning inner models for a certain axiomatic system of set theory which lead to the result that as far as a fairly large family of inner models are concerned this method of proving consistency has been exhausted, that no essentially new consistency results can be obtained by the use of this kind of model.

1. The purpose of the present paper is to formulate the problem of non-finitist proofs, and to solve it for certain extensions of the predicate calculus, and for analysis with the exclusion of the theory of sets of points. The corresponding problem for general formal systems is discussed in another publication [1].

To fix ideas we introduce the problem by examples from analysis. The general formulation is given in the text. Also, we shall use in the introduction the concepts decidable, verifiable, finitist without much formal explanation, because the reader is probably familiar with them, and they are defined early on in the text.

The paper presupposes some knowledge of the methods and results in the theory of proofs. These enable one to state the general problem rather more precisely.

Die Verbandstheorie ist bekanntlich von Dedekind an Hand seiner idealtheoretischen Untersuchungen begründet worden. Es hat sich in letzter Zeit herausgestellt, daß die wesentliche Eigenschaft des Dedekind'schen Idealsystems darin liegt, daß die Ideale einen Halbverband (§1) bilden. Die Idealtheorie führt so auf die Frage nach alien Halbverbänden über einer beliebigen halbgeordneten Menge M. Die einfache Antwort enthält §2. Ebenso einfach ist die Frage nach alien distributiven Verbänden uber M zu beantworten. In beiden Fällen ist unter den Halbverbänden bzw. distributiven Verbänden über M einer dadurch ausgezeichnet, daß alle anderen homomorph zu ihm sind. Diesen ausgezeichneten Halbverband bzw. distributiven Verband nennen wir den freien Halbverband bzw. freien distributiven Verband über M.

Zu neuen Fragen kommt man bei der Untersuchung speziellerer Halbverbände über M. Es ist z.B. bekannt, daß M stets zu einem vollständigen Boole'schen Verband erweitert werden kann. Gibt es unter diesen Erweiterungen stets den freien vollständigen Boole'schen Verband über M, der dadurch ausgezeichnet ist, daß alle anderen zu ihm homomorph sind ?

In §3 wird zunächst die Existenz des freien orthokomplementären Halbverbandes über M bewiesen. Mit Hilfe der hier benutzten Methode läßt sich auch der Existenzbeweis für den freien abzählbar-vollständigen Boole'schen Verband über M führen.

It is well known that certain sentences corresponding to similar algebras are invariant under direct union; that is, are true of the direct union when true of each factor algebra. An axiomatizable class of similar algebras, such as the class of groups, is closed under direct union when each of its axioms is invariant. In this paper we shall determine a wide class of invariant sentences. We shall also be concerned with determining sentences which are true of a direct union provided they are true of some factor algebra. In the case where all the factor algebras are the same, a further result is obtained. In §2 it will be shown that these criteria are the only ones of their kind. Lemma 7 below may be of some independent interest.

We adopt the terminology and notation of McKinsey with the exception that the sign · will be used for conjunction. Expressions of the form ∼∊, where ∊ is an equation, will be called inequalities. In accordance with the analogy between conjunction and disjunction with product and sum respectively, we shall call α1, …, αn the terms of the disjunction

and the factors of the conjunction

Every closed sentence is equivalent to a sentence in prenez normal form,

where x1, …, xm distinct individual variables, Q1, …, Qm are quantifiers, and the matrix S is an open sentence in which each of the variables x1, …, xm actually occurs. The sentence S may be written in either disjunctive normal form:

where αi,j is either an equation or an inequality, or in conjunctive normal form:

.

Classical syntax and semantics make fundamental use of variables ranging over classes, relations, etc. In syntax, one speaks exclusively of such objects as symbols, formulae, terms, in short of what may be called (following Carnap) sign-designs. A sign-design is a class of similar concrete marks or sign-events or inscriptions or sequences of typographical characters. In semantics, in addition to sign-designs, one also speaks of the objects denoted or designated by the sign-designs called constants or of the objects which are values for the sign-designs called variables.

Interest in the possibility of a syntax and semantics based upon sign-events or inscriptions rather than upon sign-designs appears to have originated with Lesniewski and Tarski. Not until recently, however, in a paper by Goodman and Quine, has a purely inscriptional syntax been explicitly formulated. The discussion in that paper is confined to the syntax of one object language, but the methods developed are applicable to other systems as well and should suffice for many of the purposes of syntax.

In the present paper we make an attempt to construct a purely inscriptional semantics, in which, as with Goodman and Quine, sign-designs or classes of similar inscriptions in no way figure as values for variables. In rejecting such entities it might appear that the resulting semantics would be drastically curtailed. That the methods used here are of sufficient power to be of interest, however, is shown by constructing a definition of a semantical concept of truth for a given sample elementary object language L. The definition of a predicate for truth in L is given, and the predicate is shown to be adequate in essentially the sense due to Leśniewski, Kotarbiński, and Tarski.

We consider here the pure functional calculus of first order as formulated by Church.

Church, l.c., p. 79, gives the definition of the validity of a formula in a given set I of individuals and shows that a formula is provable in if and only if it is valid in every non-empty set I. The definition of validity is preceded by the definition of a value of a formula; the notion of a value is the basic “semantical” notion in terms of which all other semantical notions are definable.

The notion of a value of a formula retains its meaning also in the case when the set I is empty. We have only to remember that if I is empty, then an m-ary propositional function (i.e. a function from the m-th cartesian power Im to the set {f, t}) is the empty set. It then follows easily that the value of each well-formed formula with free individual variables is the empty set. The values of wffs without free variables are on the contrary either f or t. Indeed, if B has the unique free variable c and ϕ is the value of B, then the value of (c)B according to the definition given by Church is the propositional constant f or t according as ϕ(j) is f for at least one j in I or not. Since, however, there is no j in I, the condition ϕ(j) = t for all j in I is vacuously satisfied and hence the value of (c)B is t.

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.

In part I of the present paper axiom schemes and rules of inference were defined for m-valued functional calculi of first order with s(m > s > 1) designated truth-values. A proof of plausibility was given, and it was shown that it is not difficult to extend to m-valued functional calculi of first order certain concepts that are closely analogous to the ordinary 2-valued notions of “consistency with respect to an operator” and “absolute consistency.” The purpose of the present paper is to show that the concept of “deductive completeness” may be extended to m-valued functional calculi of first order. For this purpose we define “analytic formula” for the m-valued case and show that if a formula is analytic, then it is provable in our formalization of m-valued functional calculi of first order.

In proving deductive completeness for the m-valued case, it is possible to use a method which is analogous to that used by Gödel in establishing the completeness of 2-valued functional calculi of first order. However, in the present paper we will indicate only very briefly how the Gödel procedure may be extended to the m-valued case. Our chief concern will be the problem of extending to our formalization of m-valued functional calculi the more elegant proof of deductive completeness for the 2-valued case which has recently been developed by Leon Henkin.

There has recently been developed a method of formalising any fragment of the propositional calculus, subject only to the condition that material implication is a primitive function of the fragmentary system considered. Tarski has stated, without proof, that when implication is the only primitive function a formulation which is weakly complete (i.e., has as theorems all expressible tautologies) is also strongly complete (i.e., provides for the deduction of any expressible formula from any which is not a tautology). The methods used by Henkin suggest the following proof of the

Theorem. If in a fragment of the propositional calculus material implication can be defined in terms of the primitive functions, then any weakly complete formalisation of the fragmentary system which has for rules of procedure the substitution rule and modus ponens is also strongly complete.

13.1. If ‘[p f a]’ is in K′, we will say that ‘p’ is a value of ‘f’ at ‘a’.

13.2. If ‘a’ and ‘b’ are rational U-reals and if ‘b’ is not less than ‘a’, then ‘{a, b}’ will be called a rational U-interval.

13.3. If ‘f’ has a value at ‘d’, if ‘d’ is within a U-interval ‘{c, e}’, and if all values of ‘f’ at U-reals with ‘{c, e}’ are within the U-interval ‘{r, t}’, then we will say that ‘{c, e}’ restricts ‘f’ to ‘{r, t}’ at ‘d’, and that ‘{c, e}’ is an ‘f’-restrictive correlate of ‘d’ with respect to ‘{r, t}’.

13.4. If ‘d’ is within ‘{a, b}’, we will say that ‘{a, b}’ “contains” ‘d’.

13.5. If ‘f’ has a value at ‘d’ and if corresponding to every U-interval ‘{r, t}’ that contains a value of ‘f’ at ‘d’ there is an ‘f’-restrictive correlate of ‘d’ with respect to ‘{r, t}’, then ‘f’ will be said to be “continuous” at ‘d’. Without loss of generality the ‘f’-restrictive correlate can be required to be a rational U-interval.

13.6. If ‘f’ is continuous at every U-real in ‘{a, b}’, we will say that ‘f’ is continuous in ‘{a, b}’.

13.7. Theorem. If ‘k’ is a positive U-real and ‘f’ is continuous in a U-interval ‘{a, b}’, then ‘{a, b}’ is covered by the class S of rational U-intervals that are ‘f’-restrictive correlates of rational U-reals in ‘{a, b}’ with respect to those rational U-intervals ‘{r, t)’ that contain values of ‘f’ at rational U-reals in ‘{a, b}’ and that are such that’∣t − r∣‘ is equal to ‘k’ (in the sense of 10.10).

The purpose of this paper is to construct a non-finitary system of logic S, based on the theory of types, in which classical quantification theory holds without restriction and the axiom of reducibility holds with such slight restriction as is perhaps unlikely to interfere with the construction of classical mathematics. The system will be shown to be consistent.

For purposes of orientation, a rough description of the ontology of the system will first be given. The ‘individuals’ are expressions built up in the following way: ‘0’ is an individual, and if ϕ and ψ are individuals, so is ˹*ϕψ˺. The usual apparatus of truth functional connectives and quantifiers is employed, and one primitive four place predicate ‘S’. ˹Sϕψχω˺ says that ϕ is the result of writing ψ for all occurrences of χ in ω, where ϕ, ψ, χ and ω may be formulae, individuals, or members of a wider category called ‘expressions’ which includes individuals, formulae, and other things as well. (At first sight this looks like a confusion of use and mention, but the formation rules and rules of inference are so phrased that no ambiguity arises.)

The individuals are divided into types concentrically, so that type 0 has them all as members and type n includes type m for m > n. There is no highest type, but we shall find it convenient from the point of view of exposition to construct an infinity of ‘auxiliary’ systems Q(k), restricted to types ≦ k, before presenting the system S.

If F is a field, and α is an element of F, we say that α is arithmetically definable in F if there is a formula containing one free variable and any number of bound variables, involving only the concepts of elementary logic and the operations of addition and multiplication, which is satisfied by α and by no other element of F. The range of the bound variables is understood to be F. Without changing the sense of the above definition, we can allow in our formulas symbols for specific integers, or even (if F has characteristic zero) symbols for specific rational numbers, since these are arithmetically definable.

As an example, consider the field F = R(2¼), obtained by adjoining the positive fourth root of 2 to the field R of rationals. Notice that 2¼ is not defined arithmetically by the formula x2 = 2, since this equation has two roots in F.

However, 2¼ may be defined arithmetically by the equivalence

where we have used the logical symbols ↔ (if and only if), ∨ (there exists), and ∧ (and). For the equation y4 = 2 is satisfied by no elements of F except y = ±2¼, and in both cases y2 = 2¼. On the other hand, 2¼ is not arithmetically definable in F, since there is an automorphism of F which takes 2¼ into −2¼, so that every arithmetical condition satisfied by 2¼ is also satisfied by −2¼.

In any field F, a necessary condition for the arithmetical definability of an element α is that α should be fixed for all automorphisms of F. That this condition is not always sufficient is shown by considering the field of real numbers. Here there is no automorphism but the identity, but there can of course be but a denumerable infinity of arithmetically definable real numbers. Tarski has shown that only the algebraic numbers are arithmetically definable.

A general system of axioms has been given by Henkin for a fragment of the propositional calculus having as primitive symbols, in addition to the usual parentheses, variables, and implication sign ⊃, an arbitrarily given truth function symbol ϕ. This system of axioms, which we shall denote by S(⊃, ϕ), contains the following three axiom schemata

plus the 2m further axiom schemata involving the symbol ϕ

where ϕ is an m-placed function symbol. We refer to Henkin's paper, p. 43, for the detailed description of the axiom schemata (4).

The remark was made in the above mentioned paper that each of the 2m axiom schemata of (4) is trivially independent of the rest of the axioms of S(⊃, ϕ), and it was conjectured that the axiom schemata (1), (2) and (3) are also independent. In this note, we prove the general independence of the axiom schemata (1) and (2). As for (3), we show on the one hand its independence in the systems S(⊃) and S(⊃, f), and, on the other hand, its dependence in the system S(⊃, ∼). The net result is, therefore, that in any of these systems of axioms S(⊃, ϕ) all the axiom schemata are independent, except possibly the axiom schema (3).