zbMATH — the first resource for mathematics

A new basic set of transformations between proofs. (English) Zbl 1272.03153
Artemov, Sergei (ed.) et al., We will show them! Essays in honour of Dov Gabbay on his 60th birthday. Volume 2. London: College Publications (ISBN 1-904987-12-5/pbk; 1-904987-26-5/hbk). Tributes 2, 499-528 (2005).
From the text: The functional interpretation of logical connectives, the so-called Curry-Howard interpretation, provides an adequate framework for the establishment of various calculi of logical inference. Being an ‘enriched’ system of natural deduction, in the sense that terms representing proof-constructions (the labels) are carried alongside formulas, it constitutes an apparatus of great usefulness in the formulation of logical calculi in an operational manner. By uncovering a certain harmony between a functional calculus on the labels and a logical calculus on the formulas, it proves to be instrumental in giving mathematical foundations for systems of logic presentation designed to handle meta-level features at the object-level via a labelling mechanism, such as, e.g., D. M. Gabbay’s [Labelled deductive systems. Vol. 1. Oxford: Clarendon Press. (1996; Zbl 0858.03004)] labelled deductive systems.
By using labels one can keep track of proof steps. This feature of labelled natural deduction systems helps to recover the ‘local’ control virtually lost in plain natural deduction systems.
We first present the syntax of the term-rewriting system TRS associated to labelled natural deduction, by means of an equational system with ordered sorts. Next, the TRS defined by the authors in [“Term rewriting systems with LDS”, in: Proc. of Brazilian symposium on artificial intelligence, 425–439 (1994)] is presented, and the proofs of termination and confluence are given.
For the entire collection see [Zbl 1202.03007].

03F05 Cut-elimination and normal-form theorems
03B40 Combinatory logic and lambda calculus
68Q42 Grammars and rewriting systems