Consider the following intriguing conjecture formulated by Dag Prawitz (``Ideas and Results in Proof Theory''Proceedings of the Second Scandinavian Logic Symposium, 1971) for intuitionistic natural deduction LJ:
two natural deduction derivations in LJ represent the same informal argument
if and only if they are equivalent up to normalization
Is Prawitz's conjecture true? Is it even plausible?
• There are serious arguments against it, on consideration of the length of proofs, as pointed out by George Boolos ``Don't eliminate cut'' Journal of Philosophical Logic 13 1984, pp. 373-378; see also Wittgenstein Remarks on the Foundations of Mathematics III, 2.

• Nevertheless, normalization and other techniques can be used to extract the algorithm implicit in a proof (unwinding). In this activity it is assumed that the same algorithm is implicit in the original proof and explicit in the transformation to normal form. Equivalence up to normalization may be too coarse a notion to capture the identity of intuitive arguments, but it does identify an interesting property of proofs.

• There is an analogue difficult question concerning algorithms: given a programming language,
  under which conditions do two programs represent the same algorithm?

  Here we may consider the lambda-calculus, with certain notions of reduction, as the programming language.

  • The Curry-Howard isomorphism establishes a correspondence between proofs in intuitionistic natural deduction LJ and lambda-terms, and between proof-normalization and beta-reduction.

  • Thus the analogue of Prawitz's conjecture is the statement that beta-equivalence defines algorithmic identity.

  But this is certainly wrong: a normal lambda-term corresponds to the output of the computation, and we do not want to identify algorithms only by their input-output behaviour.

• What is a calculus for classical logic, for which we may formulate the analogue of Prawitz's conjecture?
  • Certainly not classical natural deduction NK, since it makes essential use of Goedel's double negation interpretation; rather than classical proofs, it formalizes their intuitionistic translations.

  • Certainly not classical sequent calculus LK, since it has neither the strong normalization nor the Church-Rosser property.

• Nevertheless, recent research on classical logic (and also on linear logic) shows that the Church-Rosser property and the strong normalization theorem can be obtained for a notion of reduction which prohibits the permutations of inferences in the sequent calculus LK.
  • Isn't the resulting notion of identity of proofs too rigid? Aren't we taking accidental features of the syntax as defining the identity of a proof?

    Recent work by Stefano Berardi and others shows that the algorithm implicit in a classical proof may change if inferences are permuted.

  It would seem that Gentzen's proof-theory has not become yet a theory of proofs: we do not know yet how to identify its objects.

• Does current research on the typed lambda-calculus and linear logic, in particular the game theoretic semantics, provide more refined tools to attack these problems?

  One attractive feature of such a semantics is that it would allow us to define the notion of identity of proofs and also of (sequential) algorithms. Also for this reason a philosophical investigation of recent development in game-theoretic semantics seems urgent.

• Are we going to see the dawn of a theory of proofs? Or is the question is premature? Perhaps, borrowing an image by Kreisel, one could say that a genuine {\it theory of proofs} needs the study of significant examples, in the same way as a general theory of cristallography has been preceded by the collection and consideration of precious stones.

• The paper ``Ramsey Interpreted: A Paramtrized version of Ramsey's Theorem'' Bellin 1990 shows that the infinite, the finite and the Paris-Harrington version of Ramsey's theorem all follow from a parametric version of Ramsey's theorem, by different selection of the parameters defining the prehomogeneous sets. This result is therefore concerned with the problem of similarity of proofs and is an extensive case study by proof-theoretic techniques. The genuine philosophical interest of this kind of investigations is recognized, as soon as we realize that a solution to the problem of the identity of proofs can only come from the analysis of the structure of informal proofs in everyday mathematics.

back home