The Functional Interpretation of Logical Deduction

This comprehensive book provides an adequate framework to establish various calculi of logical inference. Being an ‘enriched’ system of natural deduction, it helps to formulate 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 allows mathematical foundations for systems of logic presentation designed to handle meta-level features at the object-level via a labelling mechanism, such as the D Gabbay's Labelled Deductive Systems. The book truly demonstrates that introducing ‘labels’ is useful to understand the proof-calculus itself, and also to clarify its connections with model-theoretic interpretations. Contents:Labelled Natural DeductionThe Functional Interpretation of ImplicationThe Existential QuantifierNormalisationNatural Deduction for EqualityNormalisation for the Equality FragmentModal LogicsMeaning and Proofs: A Reflection on Proof-Theoretic Semantics Readership: Researchers, professionals, academics and graduate students in theoretical computer science, (analytic) philosophy, and logic and set theory. Keywords:Proof Theory;Natural Deduction;Functional Interpretation;Labelled Deduction;Curry-Howard InterpretationKey Features:The first book that explains how one can look at the Curry-Howard functional interpretation in a more general perspectiveCovers the important aspects of the interplay between terms and formulas, proof constructions and deductionsConsists of numerous examples in setting the desired parameters in a deductive calculus