Die Gründe, die C. I. Lewis [5], [6] bewogen haben, neben der gewöhnlichen Implikation eine strikte Implikation einzuführen, sind bekannt. In der vorliegenden Arbeit wird aus ähnlichen Gründen eine strenge Implikation eingeführt, die jedoch einen engeren Begriff darstellt als die strikte Implikation. Mit einer Arbeit von Arnold Schmidt [7] hat meine nur geringe Berührungspunkte, da der Verfasser sich mit der strikten Implikation beschäftigt. Für diese wird ein relativ einfaches Axiomensystem angegeben und gezeigt, wie man durch geeignete Definitionen von Notwendigkeit und Möglichkeit bei eventueller Hinzufügung von Zusatzaxiomen die bekannten Systeme des Modalitätenkalküls erhält. Den Hauptteil meiner Arbeit bildet die Einführung meines Implikationsbegriffs; im zweiten Teil der Arbeit komme ich dann auf dieser Basis auch zu einer Einführung der Modalitäten.

Um die Art der Einführung des Kalküls zu motivieren, wollen wir kurz auf das eingehen, das uns mehr oder weniger deutlich vorschwebt, wenn wir von der strengen Implikation sprechen. Die strenge Implikation, die wir durch A → B wiedergeben, soll ausdrücken, daß zwischen A und B ein logischer Zusammenhang besteht, daß der Inhalt von B ein Teil des Inhaltes von A ist, oder wie wir es sonst ausdrücken wollen. Das hat mit der Richtigkeit oder Falschheit von A und B nichts zu tun. So würde man die Allgemeingültigkeit einer Formel A → (B → A) ablehnen, da sie den Schluß von A auf B → A einschließt und da die Richtigkeit von A nichts damit zu tun hat, ob zwischen B und A ein logischer Zusammenhang besteht.

1.1 The system K* of basic logic, as presented in a previous paper, will be shown to be formalizable in an alternative way according to which the rule [E],

is replaced by the rule [F],

1.2. General recursive functions will be shown to be definable in K* in a way that retains functional notation, so that the equation,

will be formalized in K* by the formula,

where ‘f’, ‘p1’, … ‘pn’ respectively denote φ, x1, …, xn, and where ‘≐’ plays the role of numerical equality. Partial recursive functions may be handled in a similar way. The rule [E] is not required for dealing with primitive recursive functions by this method.

1.3. An operator ‘G’ will be defined such that ‘[Ga ≐ p]’ is a theorem of K* if and only if ‘p’ denotes the Gödel number of ‘a’.

1.4. In reformulating K* we assume ‘o0’, ‘o1,’ ‘o2’, …, have been so chosen that we can determine effectively whether or not a given U-expression is the mth member of the above series. The revised rules for K* are then as follows. (Double-arrow forms of these rules are derivable, except in the case of rule [V].)

This is the first in a series of articles outlining a new approach to Semantics. The novelty in the approach is that the concept of an interpretation of a logical system is taken as the central concept of Semantics. I hope to show that by means of this approach a satisfactory definition can be given for such controversial concepts as analyticity, and at the same time the approach leads to a unified foundation for formalized Semantics.

As the possibility of such definitions has been questioned in recent years, it is an important task to try to give precise definitions. Clearly, this is the task of those philosophers who believe that concepts like analyticity should play a fundamental role in Semantics. On the other hand, the philosophers who have criticized these concepts will now be able to tell just exactly why these definitions are unacceptable to them — instead of being forced to talk in generalities. It seems to me that no further progress is possible until we have precise definitions available for discussion.

The fundamental semantic concepts fall into two classes: those, like truth, for which Tarski has offered definitions; and those additional ones, like analytic truth, for which we have Carnap's proposed definitions.

Recent discussion serves to bring out, amply and convincingly, the utility of observing the ordinary correct use of words and phrases for the purpose of clearing up philosophical problems. In this paper, I shall endeavour to show, by means of an example, that the reverse method may have its interest, too. An attempt will be made to cultivate a minor deviation from the accepted ways of using certain words and phrases in idiomatic English as well as in the formalized “languages” of the logicians. The words and phrases in question are those for the formalization of which a logician employs (free or bound) variables. Cases in point are the words customarily called quantifiers. The deviation I have in mind affects the relation of these words to the notion of identity. The deviation is illustrated by the following sentences:

(1a) Any two points of a straight line completely determine that line;

(2a) He is John's brother if he has the same parents as John;

(3a) Mazzini did more for the emancipation of his country than any living man of his time.

These examples may be contrasted with the following closely related sentences:

(1b) Any two distinct points of a straight line completely determine that line;

(2b) He is John's brother if he has the same parents as John and if he is not John himself;

(3b) Mazzini did more for the emancipation of his country than any other living man of his time.

The following remarks apply to many functional calculi, each of which can be variously axiomatized, but for clarity of exposition we shall confine our attention to one particular system Σ. This system is to have the usual primitive symbols and formation rules of the pure first-order functional calculus, and the following formal axiom schemata and formal rules of inference.

Axiom schema 1. Any tautologous wff (well-formed formula).

Axiom schema 2. (a) A ⊃ B, where A is any wff, a and b are any individual variables, and B arises from A by replacing all free occurrences of a by free occurrences of b.

Axiom schema 3. (a)(A ⊃ B)⊃(A⊃ (a)B). where A and B are any wffs, and a is any individual variable not free in A.

Rule of Modus Ponens: applies to wffs A and A ⊃ B, and yields B.

Rule of Generalization: applies to a wff A and yields (a)A, where a is any individual variable.

A formal proof in Σ is a finite column of wffs each of whose lines is a formal axiom or arises from two preceding lines by the Rule of Modus Ponens or arises from a single preceding line by the Rule of Generalization. A formal theorem of Σ is a wff which occurs as the last line of some formal proof.

1. This paper grew out of an attempt to answer a question raised in [4]. Let a logic L containing “numerals” z1, z2, … and a certain statement N(x) (intended to express the proposition that x is a natural number) be called ω-inconsistent if there is a statement such that ⊦ F(zk) for k = 1, 2, …, and ⊦ ∼(x)·N(x) ⊃ F(x); then it is evident that L cannot have a model in which N(x) is satisfied by the images of the numerals and nothing else if L is ω-inconsistent.

Question: If L is ω-consistent, i.e. not ω-inconsistent, must there be such a model? Calling a model of the kind just described a special model, we ask for necessary and sufficient conditions on L to insure the existence of a special model. We give several sets of such conditions, applicable to a certain very inclusive class of logics, in Theorem 1 and Theorems 3 and 4. Theorem 2 shows that a logic may be ω-consistent but still not have a special model.

This paper was close to completion when [3] appeared. For systems with only denumerably many symbols our results include Henkin's, for, by adjoining a new predicate N(x) to each of the systems considered in [3] which have only a denumerable number of constant symbols and then adding as an axiom (x)N(x), these systems become special cases of the systems we consider. It is easily seen that Henkin's Theorem 7 essentially proves the equivalence of conditions (2) and (3) in our Theorem 1, and Theorem 3 of [3] corresponds to our Theorem 2. Incidentally, our argument of Theorem 2 could also serve to prove Henkin's Theorem 6.

In this note we point out that two concepts which have been introduced separately into the theory of models are extensionally equivalent. The basic ideas can be expressed conveniently in the terminology of Tarski's theory of arithmetical classes. It will be recalled that an arithmetical class is a class consisting of all algebraic structures which satisfy some fixed sentence of the first-order functional calculus. A more general concept is that of a quasi-arithmetical class, whose elements are all algebraic structures which satisfy some fixed set of first-order sentences.

Now where H and K are any two classes of algebraic structures, Abraham Robinson has defined the relation H is persistent with respect to K to mean that (i) H∩K is non-empty, and (ii) whenever M ϵ H∩K, M′ is an extension of M, and M′ ϵ K, then M′ ϵ H. Concerning this notion Robinson has established the following theorem: If K is the class of abelian groups (or of commutative fields) and H is an arithmetical class which is persistent with respect to K, then H∩K contains a group (or field) which is finite. This leads us to the following definition.

Professor Prior (Formal logic (1955), pp. 305–307) gives alternative postulate sets for Lewis's S5, one substantially Lewis's own set (p. 305, 6.1) and another, considerably simpler, due to Prior himself (pp. 306–307, 6.5). This note aims at showing that the systems based on these two postulate sets are in fact equivalent. We label the system based on Lewis's postulates ‘S5’, as usual, and that on Prior's postulates ‘P’.

The form of the postulate set for P considered here is as follows. We add to the full propositional calculus one definition:

Df. M: M = NLN;

and two special rules:

L1: ⊦Cαβ → ⊦CLαβ;

L2: ⊦Cαβ → ⊦CαLβ, if α is fully modalized (a propositional formula is fully modalized, if and only if all occurrences of propositional variables in it lie within the scope of a modal operator).

Prior's text (pp. 201–205) indicates sufficiently how it could be shown that any thesis of S5 is a thesis of P and that the rules and definitions of S5 are obtainable as derived rules of P. We turn, therefore, to the problem of showing that any thesis of P is a thesis of S5 and that the rules and definition of P are obtainable as derived rules of S5.

1. The purpose of this paper is to show that, if the axioms of a system G of set theory are consistent, then it is impossible to prove from them the following weak form of the axiom of choice: (H1) For every denumerable set x of disjoint two-element sets, there is a set y, called a choice set for x, which contains exactly one element in common with each element of x. Among the axioms of the system G, we take, with minor modifications, Axioms A, B, C of Gödel [6]. Clearly, the independence of H1 implies that of all stronger propositions, including the general axiom of choice and the generalized continuum hypothesis.

The proof depends upon ideas of Fraenkel and Mostowski, and proceeds in the following manner. Let a be a denumerable set of objects Δ0, Δ1, Δ2, …, the exact nature of which will be specified later. Let μj = {Δ2j, Δ2j+1} for each j, c = {μ0, μ1, μ2, …}, and b = [the sum set of a]. By transfinite induction, construct the class Vc which is the closure of b under the power-set operation. For each j, it is possible to define a 1–1 mapping of Vc onto itself with the following properties. The mapping preserves the ε-relation, or, more precisely, .

The following are some consequences of a recent result concerning the prime implicants of disjunctive normal formulas.

I. Introduce the void fundamental formula λ, and define the consensus of αϕ and as in [5], but allowing ϕ or ψ or both to be λ. Then a normal formula Φ is valid if and only if the operations of dropping subsuming clauses and adjoining consensus formulas end by transforming Φ into the single formula λ. (For under the notions of fundamental formula and consensus as now extended, λ is a (unique) prime implicant of all valid formulas and of no others; and the argument of [5] now shows that the operations mentioned transform every normal formula, whether valid or not, into the disjunction of its prime implicants.)

II. A normal formula ψ implies a normal formula Φ if and only if every clause of ψ subsumes one of the prime implicants of Φ, which are found as in I above. (The condition is clearly sufficient. It is necessary, for if ψ implies Φ, then every clause of ψ implies Φ and subsumes a shortest fundamental formula implying Φ.) In this condition, the prime implicants of Φ may be replaced by the clauses of the result of merely adjoining, as long as possible, consensus formulas to Φ.

The main purpose of this note is to prove (theorem 11, § 5) that, in any interpretation of the formalisation of Aristotelian syllogistic given by Łukasiewicz [4], it is always possible to associate with each element a a non-null sub-class φ(a) of some ‘universal’ class V in such a way that ‘Aab’ (all a are b), ‘Iab’ (some a are b) are equivalent respectively to ‘φ(a) is contained in φ(b)’, ‘φ(a) has a non-null intersection with φ(b)’. Similarly (theorem 6, §4) we show that in Wedberg's system [14] with primitives ‘Aab’, ‘a’ (not a), it is possible to find a mapping a → φ(a) as above such that ‘Aab’ is equivalent to ‘φ(a) is contained in φ(b)’ and φ(a‘ is equal to φ(a)’, the complement of φ(a) with respect to V. Thus, if we make the preliminary step of identifying elements a, b such that Aab and Aba both hold (i.e. taking equivalence classes with respect to the relation Aab & Aba), we are left with essentially only one kind of interpretation for these systems, namely the ‘normal’ interpretation by classes. Slupecki [11], [12] has proved that Łukasiewicz's system is a complete and decidable theory of the relations of inclusion and intersection of non-null classes, and Wedberg [14] has proved that his system is a complete and decidable theory of the relation of inclusion and the operation of complementation for nonnull, non-universal classes. Using the above-mentioned embedding theorem, we are able to obtain (theorems 9, 6, §§ 5, 4) very simple proofs of these results.

A statement X in the lower predicate calculus is said to be persistent with respect to the set of statements K ([2], [3]), if whenever X holds in a model M of K then X holds also in all extensions of M which are models of K. If X is persistent with respect to the empty set, then it may be said to be absolutely persistent.

A statement X is called existential, if it is in prenex normal form and does not contain any universal quantifiers. This includes the possibility that X does not contain any quantifiers at all.

Let E be the class of all existential statements. Then it is not difficult to see that E is quasi-disjunctive. That is to say, given statements Y1, Y2 in E, there exists a statement Y in E such that

is provable.

L. Henkin [1] has raised the question how to characterise the statements X which are persistent with respect to a given set K (e.g. a set of axioms for a field or a group) by a syntactical condition. He has shown that, in order that a statement X be absolutely persistent, it is necessary and sufficient that there exist a statement Y ϵ E such that

is provable.

Leo Simons has shown that H1—H6 below constitute a set of independent axiom schemata for S3, with detachment for material implication “→” as the only primitive rule. He also showed that addition of the scheme (◇ ◇ α ⥽ ◇ α) yields S4, and that these schemata for S4 are independent. The question for S5 was left open. We shall show (presupposing familiarity with Simons' paper) that H1—H6 and S, below, constitute a set of independent axiom schemata for S5, with detachment for material implication as the only primitive rule.

Let S5′ be the system generated from H1—H6 and S with the help of the primitive rule. It is easy to see that Simons' derivations of the rules (a) adjunction, (b) detachment for strict implication, and (c) intersubstitutability of strict equivalents, may be carried out for S5′. We know that (1) (∼ ◇ ∼ α ⥽ ◇ α) is provable in S2, hence also in S3 and S5′; and (1) and S yield (2) (α ⥽ ∼ ◇ ∼ ◇ α). Perry has shown that addition of (2) to S3 yields S5, so S5 is a subsystem of S5′. And it is easy to prove S in S5; hence the systems are equivalent.

Commonly, when we succeed in showing a formula of quantification theory to be consistent, we do so by producing a true interpretation. Sometimes we achieve the same effect without even exceeding the resources of quantification theory itself: we show a formula consistent by producing a valid formula from it by substitution. Example: ‘(∃x)Fx ⊃ (x)(∃y) (Gxy ▪ Fy)’ is seen consistent by noting its valid substitution case ‘(∃x)Fx ⊃ (x)(∃y)(Fx ∨ Fy ▪ Fy)’. How generally available is this latter method? I shall show that it is available if and only if the formula whose consistency is shown is satisfiable in a one-member universe.

The “only if” part is immediate. For, if ψ is a substitution case of ϕ, then ϕ is satisfiable wherever ψ is; and ψ, if valid, is satisfiable in a one-member universe.

Conversely, suppose a true interpretation of ϕ in a one-member universe. Each predicate letter of ϕ is thereby interpreted outright as true or false, in effect, since there is no varying the values of ‘x’, ‘y’, etc. Now form ψ from ϕ by substitution as follows: change each atomic formula ϕi(e.g. ‘Fx’, ‘Fy’, ‘Gxy’) to ⌜ϕi⊃ϕi⌝ if its predicate letter is one that was interpreted as true, or to ⌜ϕi ▪ − ⊃ϕi⌝ if its predicate letter is one that was interpreted as false. Clearly ψ under all interpretations even in large universes, will receive the truth value that ϕ received under the supposed interpretation in the one-member universe. So ψ is valid.

In part I of this paper it is shown that if the simple theory of types (with an axiom of infinity) is consistent, then so is the system obtained by adjoining axioms of extensionality; in part II a similar metatheorem for Gödel-Bernays set theory will be proved. The first of these results is of particular interest because type theory without the axioms of extensionality is fundamentally rather a simple system, and it should, I believe, be possible to prove that it is consistent.

Let us consider — in some unspecified formal system — a typical expression of the axiom of extensionality; for example:

where A(h) is a formula, and A(f), A(g) are the results of substituting in it the predicate variagles f, g for the free variable h. Evidently, if the system considered contains the predicate calculus, and if h occurs in A(h) only in parts of the form h(t) where t is a term which lies within the range of the quantifier (x), then 1.1 will be provable. But this will not be so in general; indeed, by introducing into the system an intensional predicate of predicates we can make 1.1 false. For example, Myhill introduces a constant S, where ‘Sϕψχω’ means that (the expression) ϕ is the result of substituting ψ for χ in ω.

We presuppose the terminology of [1], and we give a negative answer to the following problem ([1], p. 19): Does every essentially undecidable axiomatizable theory have an essentially undecidable finitely axiomatizable subtheory?

We use the following theorem of Kleene ([2], p. 311). There exist two recursively enumerable sets α and β such that (1) α and β are disjoint (2) there is no recursive set η for which α ⊂ η, β ⊂ η′. By the definition of recursive enumerability, there are recursive predicates Φ and Ψ for which

We now specify a theory T which will afford a counter-example to the given problem of Tarski. The only non-logical constants of T are two binary predicates P and Q, one unary operation symbol S, and one individual constant 0. As in ([1], p. 52) we define

The only non-logical axioms of T are the formulae P(Δm, Δn) for all pairs of integers m, n satisfying Δ(m, n); the formulae Q(Δm, Δn) for all pairs of integers m, n satisfying Ψ(m, n); and the formula

T is consistent, since it has a model. It remains to show that (1) every consistent extension of T is undecidable (2) if T1 is a finitely axiomatizable subtheory of T, there exists a consistent and decidable extension of T1 which has the same constants as T1.

According to McKinsey and Tarski [3], who introduced the notion, a closure algebra Γ = (K, ∪, ∩, –, C) is a Boolean algebra (K, ∪, ∩, –) with an additional unary operator C, closed in K, such that, for every x, y ϵ K, x ⊆ Cx, CCx = Cx, C(x∪y) = Cx∪Cy, CΛ = Λ. McKinsey [2] has proved that a matrix Γ = (K, D, ∪, ∩, –, C) is a representation (normal matrix) of S4, if and only if (1) (K, ∪, ∩, –, C) is a closure algebra, (2) D is an additive ideal of K, (3) if – Cx ϵ D then x = Λ, D being the distinguished proper subset of K and ∪, ∩, –, C having been made to correspond to ∨, ·, ∼, ◊, respectively. Following McKinsey, one proves immediately

Theorem 1. A matrix Γ is a representation of S5, if and only if it is a closure algebra and

(α) for every x ϵ K, –C–Cx = Cx, and

(β) D is an additive ideal of K such that, for every x ϵ D, Cx = V.

This raises the question of alternative characterizations of S5. Because of (β), one may without substantial loss of generality put D = {V}. The question then becomes one for conditions that are in closure algebras equivalent to (α). One such characterization has been given by McKinsey and Tarski [4]. Defining x∸y = C(x∩–y) and ¬x = V∸x, these authors have shown that the closed elements K* of a closure algebra Γ form a Brouwerian algebra Γ* = (K*, ∪, ∩, ∸), and furthermore that Γ* is a Boolean algebra under ∪, ∩, ¬, if and only if, for every x ϵ K*,

I will give precise versions of the foregoing verbal definitions, by formalizing them within a formal metalanguage.

In order to avoid the necessity of formulating a meta-language, I will make use of VI 112, (i.e., Gödel's The consistency of the continuum hypothesis). Actually, the system there developed is unnecessarily strong for the limited purpose of this illustration. It will suffice to choose for the system of VI 112 without axioms C4 and E (axioms of replacement and choice); this system will be the logical basis of , and to this I will add some set-constants and some meaning postulates. The logical basis is roughly as strong as Zermelo's system with an axiom of infinity.

Within I will set up analogues of the previous definitions, applicable to a wide variety of object-languages. For the sake of concreteness it will be convenient to think of as having Zermelo set theory, without the axiom of infinity, as its logical basis – but it must be kept in mind that this is not an essential feature of the forthcoming definitions.

Our is certainly strong enough to have all primitive recursive functions calculable within it. This supplies us with the needed tool for talking about , within , by introducing a number of primitive recursive functions, properties, and relations describing the structure of . The exact definitions of these will depend on the exact form of , but for the forthcoming definitions it will suffice to know that these functions, properties, and relations are representable in for the given . This makes the resulting definitions most useful, since they can be applied to any of the type described.