zbMATH — the first resource for mathematics

Proof identity for classical logic: Generalizing to normality. (English) Zbl 1133.03032
Artemov, Sergei N. (ed.) et al., Logical foundations of computer science. International symposium, LFCS 2007, New York, NY, USA, June 4–7, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-72732-3/pbk). Lecture Notes in Computer Science 4514, 332-348 (2007).
Summary: The problem of the identity criteria for proofs can be traced to Hilbert and Prawitz. One of the approaches, which uses the concept of generality of proofs, was suggested in 1968 by Lambek. Following his ideas, we propose a language and a logic to represent Hilbert-style proofs for classical propositional logic by adapting the Logic of Proofs (LP) introduced by Artemov in 1994. We prove that proof polynomials, the objects representing Hilbert derivations in LP, are sufficient to realize all propositional derivations, with or without hypotheses. We also show that proof polynomials respect the ideas of generality and provide an algorithm for determining whether two given proof polynomials represent the same proof. These results naturally extend similar properties of combinatory logic demonstrated by Hindley. The language of LP allows us to formally capture more structure of Hilbert-style proofs. In particular, we show how the well-known phenomenon of proof composition in classical logic manifests itself in the case of Hilbert proofs.
For the entire collection see [Zbl 1121.03005].
Reviewer: Reviewer (Berlin)

03F05 Cut-elimination and normal-form theorems
Full Text: DOI