zbMATH — the first resource for mathematics

The functional interpretation of logical deduction. (English) Zbl 1248.03003
Advances in Logic 5. Hackensack, NJ: World Scientific (ISBN 978-981-4360-95-1/hbk; 978-981-4360-96-8/ebook). xxxii, 266 p. (2012).
When working in natural deduction, one must keep track of the dependence of a formula on others. The authors advocate labeling for this purpose. To the assumption formula \(A\), one attaches a free variable \(x\) as its label \((x:A)\). After some deduction one gets \(B\) with its label \(b(x)\), which is a complex term reflecting the deduction. Then, discharge \(A\) and obtain \(A\to B\). Its label is \(\lambda x.b(x)\), where \(x\) is not free anymore, indicating that \(A\to B\) does not depend on any other formulas. The manner in which \(x:A\) is discharged determines different kinds of logics – classical, relevant, etc. (For instance, many occurrences of \(x:A\) can be discharged, or not.) Universalization starts from \(x:D\) (\(x\) belongs to the domain \(D\)). When \(f(x):F(x)\) is obtained – with the label \(f(x)\) and the formula \(F(x)\) – \(\Lambda xf(x):\forall x^D.F(x)\) can be concluded. The modal operator \(\square\) is handled as the second-order quantifier; namely, \(\square A\) is short for \(\forall W^{\mathbf D}.A(W)\), where \(W\) runs over the worlds \({\mathbf D}\). The label of \(\square A\) is \(\forall WF(W)\) when \(F(W)\) labels \(A(W)\). Again, the manner of discharging gives different modal systems. Labeling \(\exists\) and \(\forall\) is much harder, and the authors spend one whole chapter discussing various approaches. They choose an \(\varepsilon\)-term, \(\varepsilon x(f(x),a)\), as the label of \(\exists x^D.F(x)\) retaining the witness \(a\) from \(f(a):F(a)\). These labels obey reduction rules that reflect transformations of proofs. This functional interpretation, i.e., the dual development of label calculus and of proof transformation, is carried out for the equality fragment with technical details. But, throughout the book, particularly in the first half and in the last chapter, the authors verbally talk about the subject: its purpose, merits, history, and so on. There are a lot of quotations from the literature, comments on and criticisms of them, etc.
This book is a synthesis of the authors’ many papers. The stitching together is not perfect. For instance, pp. 166–167 and pp. 172–173 are duplication, and “the past ten years or so”, p. 155, line 8, refers to about 1990. The derivation of the Grzegorczyk formula, pp. 218–219, is not there.

03-02 Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations
03B45 Modal logic (including the logic of norms)
03F03 Proof theory in general (including proof-theoretic semantics)
03F10 Functionals in proof theory
Full Text: Link