Recent attempts to analyse or explicate assertion-statements and other kinds of indirect discourse in formal terms seem to have overlooked an even greater difficulty than the familiar problems arising about equivalence, synonymy, translatability, etc. This difficulty is created by the fact that in judicial, journalistic, or historical fact-finding, as well as in everyday conversation, we frequently cite statements about a witness's truthfulness alongside the report of his testimony as the premisses from which we argue about the facts. It is then an essential part of our argument that it should appear to jump from one level of statement to another, and perhaps back again. So that the difficulty emerges: how can the formalisation of such an argument adopt any of the usual hierarchy-principles as a guarantee against semantical antinomies?

Consider, for example,

The inferences countenanced by the traditional rules of modus ponens, modus tollens, disjunctive syllogism, hypothetical syllogism, and the complex types of dilemma may be regarded as single applications of one rule of inference, “the rule of complementary elimination”. In the present paper, we shall discuss this rule informally and illustrate it in application to expressions written in the language of Principia Mathematica. Our illustrations will contain no connectives except for those for conjunction, disjunction, and negation; we use parentheses in place of dots; and we allow disjunction and conjunction to have any number of operands more than two.

In applying complementary elimination to a set of premises, we take the following three steps, (i) We form, merely by disjoining the premises, an expression which we shall call a premise disjunction, (ii) If we have n premises, we eliminate n minus one (or fewer) pairs of the following sort from our premise disjunction: each pair is such that one of its members is the negation of the other and both members are specific occurrences of disjuncts of our premise disjunction. We shall call such pairs complementary pairs, (iii) The formula obtained by means of our second step is one that may be made well-formed merely by eliminating parentheses or connectives other than negation; we make such elimination, and any formula we thus obtain is a consequence of our premises.

There are axiomatizations of the sentential calculus which, in effect, assert the inferential equivalence (mutual deducibility) of classes of sentences. A well known axiomatization of this sort consists of

Another one, closely connected with A1–A3, is comprised of

B1–B3 jointly assert the inferential equivalence of a sentence of the form (p ⊃ q) ⊃ r and two sentences of the forms q ⊃ r and ∼p ⊃ r respectively. This axiomatization requires the rule of substitution and the rule of detachment for conditionals.

The existence of such axiomatizations suggests a possibility of formulating natural deduction by means of inferential equivalence instead of the usual one-sided inference, customarily represented by ‘⊦’. ‘H’ will stand here for inferential equivalence. It may be looked upon as a combination of signs ‘⊦’ and ‘⊣’. ‘H’ is thought of as a metasystematic constant functor of two arguments each of which is a class of names of sentences. For purposes of this paper the first argument may be just a single name of a sentence, the second a pair (not necessarily ordered) of names of sentences. The role ‘H’ plays is determined by **1 –*5 below. Besides that ‘H’ remains here uninterpreted. In particular, it is not directly postulated that it is an identity relation.

In this paper we show how a modification of results due to Simons ([6]) yields a set of independent axiom schemata for von Wright's M ([8], p. 85), with a single primitive rule of inference. We first describe a system M*, then show its equivalence with M, and finally show that our schemata are independent.

1. Axiomatization ofM*. We adopt the notational conventions of McKinsey and Tarski ([4], p. 2), as amended by Simons ([6], p. 309), except that we take “(α ⊰ β)” as an abbreviation for “˜◇˜(α 0→ β)”, rather than for “˜◇(α ∧ ˜β)”. Our only rule of inference is:

Rule. If ⊦ α and ⊦ (˜◇˜α → β). then ⊦ β.

We have six axiom schemata:

We require a number of theorems for the proof of equivalence of M* with M.

Theorem 1. If ⊦ α and ⊦ (α → β), then ⊦ β.

Theorem 2. If ⊦ α and ⊦ (α ⊰ β), then ⊦ β.

Proof by hypothesis, A5, and Theorem 2 (twice).

Theorem 3. If ⊦ (α ⊰ β), then (˜◇β → ˜ ◇α).

Proof by hypothesis, A6, and Theorem 2.

Theorem 4. If ⊦(α ⊰ β), then ⊦[˜˜(γ ∧ α) ⊰ ˜˜(β ∧ γ)].

This note is a sequel to the previous paper of mine which was entitled Identity, variables, and impredicative definitions and published in this Journal, vol. 21 (1956), pp. 225–245. That early paper served to call attention to the dependency of the set-theoretic paradoxes on the interpretation of the variables that may occur in the critical abstraction principle:

where K is a well-formed formula containing free occurrences of y but not those of x.

A partial reinterpretation of the variables occurring in the above formalization of the abstraction principle yields Frege's unsuccessful way out of Russell's antinomy:

with the same kind of K as above. Another gives us the alternative schema

where K+ is obtained from a K of the kind described above by replacing every well-formed part of the form (∃z)L by (∃z)(z≠x & L) and every well-formed part of the form (z)L by (z)(z≠x ⊃ L). Still a third choice of an interpretation yields the schema

where K+ is subject to the same conditions as in (1) and z1, z2, …, zk are all the free variables of (2). These three interpretations are only some of the most conspicuous ones among a multitude of possible ways of interpreting the variables that may occur in the abstraction principle.

In Herbrand's Theorem [2] or Gentzen's Extended Hauptsatz [1], a certain relationship is asserted to hold between the structures of A and A′, whenever A implies A′ (i.e., A ⊃ A′ is valid) and moreover A is a conjunction and A′ an alternation of first-order formulas in prenex normal form. Unfortunately, the relationship is described in a roundabout way, by relating A and A′ to a quantifier-free tautology. One purpose of this paper is to provide a description which in certain respects is more direct. Roughly speaking, ascent to A ⊃ A′ from a quantifier-free level will be replaced by movement from A to A′ on the quantificational level. Each movement will be closely related to the ascent it replaces.

The new description makes use of a set L of rules of inference, the L-rules. L is complete in the sense that, if A is a conjunction and A′ an alternation of first-order formulas in prenex normal form, and if A ⊃ A′ is valid, then A′ can be obtained from A by an L-deduction, i.e., by applications of L-rules only. The distinctive feature of L is that each L-rule possesses two characteristics which, especially in combination, are desirable. First, each L-rule yields only conclusions implied by the premisses.

One task of metamathematics is to relate suggestive but nonelementary modeltheoretic concepts to more elementary proof-theoretic concepts, thereby opening up modeltheoretic problems to proof-theoretic methods of attack. Herbrand's Theorem (see [8] or also [9], vol. 2) or Gentzen's Extended Hauptsatz (see [5] or also [10]) was first used along these lines by Beth [1]. Using a modified version he showed that for all first-order systems a certain modeltheoretic notion of definability coincides with a certain proof theoretic notion. In the present paper the Herbrand-Gentzen Theorem will be applied to generalize Beth's results from primitive predicate symbols to arbitrary formulas and terms.

This may be interpreted as showing that (apart from some relatively minor exceptions which will be made apparent below) the expressive power of each first-order system is rounded out, or the system is functionally complete, in the following sense: Any functional relationship which obtains between concepts that are expressible in the system is itself expressible and provable in the system.

A second application is concerned with the hierarchy of second-order formulas. A certain relationship is shown to hold between first-order formulas and those second-order formulas which are of the form (∃T1)…(∃Tk)A or (T1)…(Tk)A with A being a first-order formula. Modeltheoretically this can be regarded as a relationship between the class AC and the class PC⊿ of sets of models, investigated by Tarski in [12] and [13].