Some remarks on Novikoff’s calculus

Thierry Coquand, Hugo Herbelin

January 21, 1996

Abstract

We give a short presentation of a revised version of Novikoff’s infinitary propositional calculus. We show on examples that this calculus is well adapted for analysing the computational content of proofs in classical arithmetic. In particular, we introduce a notion of “symmetric product” on proofs, that allows a natural operation of “multi cut-elimination”.

Introduction

Novikoff [7] introduced an infinitary propositional calculus, with a notion of regular, or cut-free, proofs and a constructive proof that modus-ponens is admissible. It seems to be the first published use of an infinitary logic for analysing proofs in arithmetic (that can be found for instance in [5, 6, 8].

We present a simplified version of Novikoff’s calculus. As such, it appears to be a fragment of Tait’s infinitary propositional calculus [8]. We think that this version however has at least two advantages. First, we show that the main properties, admissibility of contractions and of cuts, have simple and direct proofs, even more direct that the ones in [8]. Second, we argue that this version represents more faithfully cut-free proofs as they appear in mathematical examples.

Finally, we show that this calculus has a natural operation of products on proofs. From this product, we derive a notion of “multi cut-elimination”. We show on one example that this operation cannot be reduced to successice cut-eliminations.

1 Formulae and validity

The positive and negative formulae are defined inductively [1].

• if A_{i} is a family of negative formulae over a countable set, then ⋁ A_{i} is a positive formula,

• if A_{i} is a family of positive formulae over a countable set, then ⋀ A_{i} is a negative formula,

We can define inductively the negation of a formula: \overline{A} is ⋀ \overline{A_{i}} (resp. ⋁ \overline{A_{i}}) if A is ⋁ A_{i} (resp. ⋀ A_{i}). Notice that we can represent the false positive formula by taking 0 = ⋁ A_{i} where (A_{i}) is the empty family of negative formulae. The negative formula 1 is dually defined as 1 = ⋀ A_{i} where (A_{i}) is the empty family of positive formulae. To each negative formula A corresponds a positive formula [A] that we get by considering the family of negative formula with only one element A.

The notion of classical validity, as described by Novikoff [7], defines inductively when a finite multiset of positive formulae is valid. We shall denote by L, M, N, … such multisets, and write L, A the addition of the positive formula A to the multiset L. We write also L, M the addition of the multisets L and M.

The multiset L, ⋁ A_{i} is valid iff there exists i_{0} such that A_{i_{0}} is an universal formula ⋀ A_{i_{0}j} such that, for all j, the multiset L, A, A_{i_{0}j} is valid.

2 Main properties

In this section, we survey the basic properties of this notion of validity.

Proposition 1: If L is a multiset of positive formulae, and A = ⋁ A_{i} a positive formula, then the multiset L, A, \overline{A_{i}} is valid.

Proof: By induction on the formula A. We have A_{i} = ⋀ \overline{A_{ij}} and, by induction hypothesis, the multiset L, A, \overline{A_{i}}, A_{ij} is valid for all j. Hence the multiset L, A, \overline{A_{i}} is valid by definition. □

Proposition 2: If L is a valid multiset of positive formulae, and A = ⋁ A_{i} a positive formula, then the multiset L, A is valid.

Proof: Direct by induction on the proof of validity of L. □

To simplify the presentation of the proofs, we will say that a multiset L, M is valid because of the L part, if it is valid because L can be written L′, B where B = ⋁ B_{j} is a positive formula such that L′, M, B_{j_{0}l} is valid for one index j_{0} and all index l.

Proposition 3: If L is a multiset of positive formulae, and A = ⋁ A_{i} a positive formula, then the multiset L, A, A is valid iff L, A is valid.

Proof: One direction follows from proposition 2. Conversely, let us prove by induction on the proof of validity of L, A, A that L, A is valid.

This is direct if L, A, A is valid because of the L part.

Otherwise, it is because there exists an index i_{0} such that L, A, A, A_{i_{0}k} is valid for all k. By induction hypothesis, L, A, A_{i_{0}k} is then valid for all k and hence L, A is valid. □

Notice that for propositions 2 and 3, we did not have to do an induction on formulae, but only on proofs of validity.

Proposition 4: If A = ⋁ A_{i} is such that L, A is valid and M, \overline{A_{i}} is valid for all i, then L, M is valid.

Proof: By induction, first on the proposition A, then on the proof that L, A is valid. It is direct if L, A is valid because of the L part. If it is valid because there exists an index i_{0} such that L, A, A_{i_{0}j} is valid for all j, then by induction hypothesis, we have that L, M, A_{i_{0}j} is valid for all j. By induction on the formula, we have that L, M, M is valid. By proposition 3, we deduce that L, M is valid. □

This direct inductive proof of the admissibility of cut has to be contrasted with the argument of [8], that needs first an inversion lemma.

3 A symmetric product

There is a natural product operation on negative formulae. The product of the formulae A = ⋀_{i∈I} A_{i} and B = ⋀_{j∈J} B_{j} is

AB = ⋀_{k∈I+J} C_{k}

with C_{inl(i)} = A_{i} and C_{inr(j)} = B_{j}.

We can then define a product, or conjunction, operation on positive formulae A = ⋁_{i∈I} A_{i} and B = ⋁_{j∈J} B_{j} as being

A ∧ B = ⋁_{(i,j)∈I×J} A_{i}B_{j}.

Proposition 5: If L, A and M, B are valid, then so is L, M, A ∧ B.

Proof: By induction on both proofs of validity. It is thus direct if L, A is valid because of the L part, or M, B is valid because of the M part.

If there exists i_{0} such that L, A, A_{i_{0}k} is valid for all k, and j_{0} such that M, B, B_{j_{0}l} is valid for all l, we proceed as follow. By applying the induction hypothesis on L, A, A_{i_{0}k} and M, B we see that L, M, A ∧ B, A_{i_{0}k} is valid for all k. By applying the induction hypothesis on M, B, B_{j_{0}l} and L, A we see that L, M, A ∧ B, B_{j_{0}l} is valid for all l. We can then conclude that L, M, A ∧ B is valid by definition. □

4 Ternary cut-elimination

The interest of the proposition 5 is less in its statement than in its proofs. From it, we indeed deduce the following operation that may be called “ternary cut-elimination”.

Suppose that A, B are positive formulae such that the multisets

M, A L, B N, \overline{A_{i}}, \overline{B_{j}}

are valid for all i and j. We shall contrast three possible ways of proving the validity of the multiset L, M, N.

The first two possible ways are by applying essentially twice proposition 4. By applying it first to M, A and N, \overline{A_{i}}, \overline{B_{j}}, for a fixed j, we deduce that M, N, \overline{B_{j}} is valid. We can then apply proposition 4 to L, B and M, N, \overline{B_{j}} to deduce the validity of L, M, N. A simple variation is first to prove the validity of L, N, \overline{A_{i}} for all i, and then to deduce the validity of L, M, N.

The third way, the “ternary cut-elimination”, is to notice that the validity of N, \overline{A_{i}}, \overline{B_{j}} is equivalent to the validity of N, \overline{(A ∧ B)_{(i,j)}}. We apply then first proposition 5 to deduce the validity of L, M, A ∧ B and then proposition 4 to deduce the validity of L, M, N.

5 Example

In this section, we want to illustrate on one example that our formalism is well suited for representing proofs in classical arithmetics and for analysing their computational content. The mathematical content of the example may seem trivial, but it has revealed what seems to be a deep problem of symmetry in the operation of cut-elimination or negative interpretation [2], problem that is handled by the ternary cut-elimination.

Here is the non constructive argument, of which we shall analyse its constructive content(s). Given a function f on integers that takes only the value 0 or 1, there exists i < j such that f(i) = f(j). Either there exists infinitely many 0’s in the range of f, or infinitely many 1’s. In the first case, choose i, j two distinct numbers on which f is 0. In the other case, choose i, j two distinct numbers on which f is 1.

This is a highly nonconstructive proof. It is composed of one main lemma: the function f takes infinitely many times the value 0, or infinitely many times the value 1, and two symmetric lemmas: if the function f takes infinitely many time the value b, which can be 0 or 1, then there exists i < j such that f(i) = f(j).

For the translation of this proof in our formalism, we represent each decidable formula as the positive formula 0 if it is false, and the positive formula [1] if it is false.

We define

• A_{n} = ⋁_{m≥n} .f(m) = 0,

• B_{n} = ⋁_{m≥n} .f(m) = 1,

• C = ⋁_{i<j} f(i) = f(j).

The main lemma can be seen as stating the validity of A_{n_{0}}, B_{n_{1}} for all n_{0}, n_{1} and the two other lemmas as stating the validity of ⋁ \overline{A_{n}}, C and ⋁ \overline{B_{n}}, C.

The validity of A_{n_{0}}, B_{n_{1}} is clear by computing f(max(n_{0}, n_{1})).

The validity of ⋁ \overline{A_{n}}, C can be seen as follows. We prove the validity of \overline{A_{0m}}, ⋁ \overline{A_{n}}, C for all m ≥ 0. This is direct if f(m) ≠ 0. Otherwise, we show the validity of \overline{A_{(m+1)m′}}, \overline{A_{0m}}, ⋁ \overline{A_{n}}, C for all m′ ≥ m + 1. This is direct if f(m′) ≠ 0. Otherwise, we have found f(m) = f(m′) = 0 and m < m′, and so we have a witness for the formula C.

The validity of ⋁ \overline{B_{n}}, C is established in the same way.

The following multisets

C, ⋁ \overline{A_{n}} C, ⋁ \overline{B_{n}} A_{n_{0}}, B_{n_{1}}

are valid. We can apply the ternary cut-elimination to conclude that the multiset C, C is valid. By proposition 3, the multiset C is valid.

Since our reasoning is schematic in the parameter f, we can interpret it computationally as a program that, given a function f, computes i < j such that f(i) = f(j). As can be intuitively expected, this program respects the symmetry 0/1: it gives the same output when applied to f or 1 − f.

Interestingly, if we don’t apply the ternary cut-elimination, but instead apply two sucessive cuts (and there are two ways of doing it), we will find two programs that do not respect the symmetry 0/1, and are respectively equivalent to the programs we get by applying a negative interpretation [2]. This phenomenon is closely connected to the problem of ∧ introduction discussed in [4].

This shows concretely that the ternary cut-elimination is not equivalent (even extensionally) to two successive ordinary cut-eliminations.

Conclusion

These results appear in substance in [3], but they are there formulated in a game-theoretical framework, interpreting a formula as a game and proof of validity of this formula as a winning strategy for this game. The present formulation is much simpler.

We hope to have shown that our formulation of infinitary propositional logic is natural and allow for clear and direct proofs. Furthemore, it reveals the existence of a notion of multi cut-elimination, that is somewhat hidden in the usual formulation of sequent calculus.

Acknowledgement

The 0/1 example, and the remark that the negative translation breaks the symmetry of its proof, are due to Gabriel Stolzenberg.

References

[1] P. Aczel. An introduction to inductive definitions. In J. Barwise, editor, Handbook of Mathematical Logic, 739 - 782, (1977), Elsevier.

[2] R. Constable and C. Murthy. Finding Computational Content in Classical Proofs. In G.Huet and G. Plotkin, editors, Logical Frameworks, 341 - 362, (1991), Cambridge University Press.

[3] Th. Coquand. A semantics of evidence for classical arithmetic. Journal of Symbolic Logic, to appear, 1994.

[4] J-Y. Girard. A new constructive logic: classical logic. Mathematical Structures in Computer Science, 1(3), (1991), P. 255-296.

[5] K. Lorenzen. Algebraische und logistische Untersuchung über freie Verbände. Journal of Symbolic Logic, V. 16, (1951), 81 - 106

[6] K. Lorenzen. Métamathématique. Edition Gauthier-Villars, 1962.

[7] Novikoff P.S. On the consistency of certain logical calculus. Matematiceskij sbornik (Recueil Mathématique) T. 12 (54), p. 230-260, 1943.

[8] W.W. Tait. Normal Derivability in Classical Logic. Springer Lecture Notes in Mathematics 72 (1968), J. Barwise ed., p. 204-236.