UDC 517.12

MATHEMATICS

L. L. MAKSIMOVA

SOME QUESTIONS OF ACKERMANN’S CALCULUS

(Presented by Academician A. I. Mal’tsev on 25 X 1966)

The article considers the calculus of “strict implication” introduced by Ackermann ([1]). His aim was to obtain an implication reflecting, as far as possible, the properties of the connective “if ..., then.” As is known, in classical logic the so-called paradoxes of material implication are true: “from falsehood anything follows,” “truth follows from any statement”; the truth of material implication does not presuppose a semantic connection between the antecedent and the consequent.

In Ackermann’s calculus \(\Pi'\), the paradoxes of material implication already turn out to be underivable. The same is true for \(E\), a modification of the calculus \(\Pi'\) proposed by Anderson and Belnap ([2]).

The decision problem for the calculi under consideration has not yet been solved. In the present article some necessary conditions are established for the provability of formulas in \(SI\) (\(SI\) is the common designation for the formal systems \(\Pi'\) and \(E\)).

As was shown independently by Belnap ([4]) and Donchenko ([5]), the formula \(\mathfrak A \to \mathfrak B\) is underivable in \(SI\) if \(\mathfrak A\) and \(\mathfrak B\) have no letters in common. For derivability, an even stronger dependence between the formulas \(\mathfrak A\) and \(\mathfrak B\) is needed.

Theorem 1. If \(\vdash \mathfrak A \to \mathfrak B\), then there is a variable which occurs positively in \(\mathfrak A\) and \(\mathfrak B\), or negatively in both formulas.

Positive and negative occurrences of subformulas are defined here in the usual way: \(\mathfrak A\) is a positive subformula of \(\mathfrak A\); if \(\neg \mathfrak B\) occurs positively (negatively) in \(\mathfrak A\), then \(\mathfrak B\) occurs in \(\mathfrak A\) negatively (positively); if \(\mathfrak B \& \mathfrak C\) or \(\mathfrak B \vee \mathfrak C\) occurs positively (negatively) in \(\mathfrak A\), then \(\mathfrak B\) and \(\mathfrak C\) both occur positively (negatively); if \(\mathfrak B \to \mathfrak C\) occurs positively (negatively), then \(\mathfrak B\) occurs negatively (positively) and \(\mathfrak C\) occurs positively (negatively).

Theorem 1 is proved with the aid of the Ackermann matrix ([5]) given in ([4]).

Theorem 2. Let the formula \(\mathfrak A\) contain no positive subformulas of the form \(\mathfrak B \vee \mathfrak C\) and no negative ones of the form \(\mathfrak B \& \mathfrak C\). If \(\vdash \mathfrak A\), then every variable occurring in \(\mathfrak A\) occurs at least once positively and at least once negatively.

Indeed, if the formula \(\mathfrak A\) satisfies the conditions of the theorem and some variable \(A\) occurs in \(\mathfrak A\) only positively (negatively), then \(\mathfrak A\) cannot be proved in \(SI\), since it is refuted by the following Ackermann matrix: the base set is \(\{-2,-1,+1,+2\}\), the designated values are \(\{+1,+2\}\),

\[ \bar{x}=-x, \]

\[ x \& y=\min (x,y), \]

\[ x \vee y=\max (x,y); \]

\[ x \to y = \begin{cases} \bar{x}\vee y, & \text{if } x \leqslant y,\\ \bar{x}\& y, & \text{if } x>y. \end{cases} \]

It is enough to assign to the variable \(A\) the value \(-2\) (respectively \(+2\)), and to all the remaining variables the value \(+1\). Then the formula \(\mathfrak A\) will receive the undesignated value \(-2\).

Thus, all occurrences of variables turn out to be, in a certain sense, connected; in particular, there can be no variable that occurs in the formula to be proved of the indicated form only once.

For the implicative fragment of the systems \(SI\) the theorem was proved by Anderson and Belnap \(\left({}^{3}\right)\).

Ackermann \(\left({}^{1}\right)\) proved the theorem: the formula \(\mathfrak A \to (\mathfrak B \to \mathfrak C)\) is not provable if \(\mathfrak A\) does not contain implication. This theorem can be strengthened in the following direction.

Let \(\mathfrak M\) be the set of formulas in which a positive occurrence of implication occurs only under the sign of another implication.

We define the class of admissible formulas as the class containing all axioms, formulas of the form \(\mathfrak A \to \mathfrak B\), where \(\mathfrak A,\mathfrak B\) belong to \(\mathfrak M\), and closed under the operations of inference \((\alpha),(\beta),(\delta)\left({}^{1}\right)\).

Theorem 3. If \(\mathfrak A_1,\ldots,\mathfrak A_k\) \((k \geq 0)\) are admissible formulas, \(\mathfrak A \in \mathfrak M\), then the formula

\[ \mathfrak A_1 \to \left(\mathfrak A_2 \to \cdots \left(\mathfrak A_k \to \left(\mathfrak A \to (\mathfrak B \to \mathfrak C)\right)\right)\cdots\right) \]

is not provable in \(SI\).

For the proof, consider the Ackermann matrix with basic set \(\{\pm1,\pm2,\pm3,\pm4,\pm5\}\) and designated elements \(\{+1,+2,+3,+4,+5\}\).

Table 1

\(x \to y\)

The implication \(x \to y\) is given by Table 1, and the remaining operations as follows:

\[ \bar{x}=-x, \]

\[ x \& y=\max z\,(z \to x>0 \text{ and } z \to y>0), \]

\[ x \vee y=\min z\,(x \to z>0 \text{ and } y \to z>0). \]

If all propositional variables take the value \(+3\), then formulas belonging to \(\mathfrak M\) take values from the set \(\{-1,-2,-3,+3,+4,+5\}\); admissible formulas take values from the set of ...

the set \(\{-1,-2,-3,-4,+2,+3,+4,+5\}\); the formula
\(\mathfrak A_1 \to (\mathfrak A_2 \to \ldots (\mathfrak A_k \to (\mathfrak A \to (\mathfrak B \to \mathfrak C))) \ldots )\) takes the value \(-5\) and, consequently, is not derivable in \(SI\).

It is not hard to see that all formulas provable in \(SI\) are also derivable in the classical propositional calculus, but the converse is not true. However, it is possible to single out a class of formulas for which derivability in \(SI\) is equivalent to classical provability.

Theorem 4. If a formula \(\mathfrak A\) contains no positive subformulas of the form \(\mathfrak B \to \mathfrak C\), then \(\mathfrak A\) is derivable in \(SI\) if and only if it is derivable in the classical calculus.

Institute of Mathematics
Siberian Branch of the Academy of Sciences of the USSR

Received
20 X 1966

REFERENCES

1. W. Ackermann, J. Symbolic Logic, 21, 113 (1956).
2. A. R. Anderson, N. D. Belnap, J. Symbolic Logic, 23, 457 (1958).
3. A. R. Anderson, N. D. Belnap, J. Symbolic Logic, 27, 19 (1962).
4. N. D. Belnap, J. Symbolic Logic, 25, 144 (1960).
5. V. V. Donchenko, in: Problems of Logic, Publishing House of the Academy of Sciences of the USSR, 1963.