The functional interpretation of logical deduction / Ruy J.G.B. de Queiroz, Anjolina G. de Oliveira, Dov M. Gabbay.

Includes bibliographical references (pages 253-264) and index.

1. Labelled natural deduction. 1.1. The role of the labels. 1.2. Canonical proofs and normalisation -- 2. The functional interpretation of implication. 2.1. Introduction. 2.2. Origins. 2.3. Types and propositions. 2.4. [symbol]-abstraction and implication. 2.5. Consistency proof. 2.6. Systems of implication and combinators. 2.7. Finale -- 3. The existential quantifier. 3.1. Motivation. 3.2. Quantifiers and normalisation. 3.3. Other approaches to existential quantification. 3.4. Model-theoretic semantics. 3.5. Finale. 3.6. Examples of deduction -- 4. Normalisation. 4.1. Introduction. 4.2. Proof transformations in labelled deduction. 4.3. Equivalences between proofs in LND. 4.4. The term rewriting system for LND. 4.5. Examples of transformations between proofs. 4.6. Final remarks -- 5. Natural deduction for equality. 5.1. Introduction. 5.2. Labelled deduction. 5.3. Finale -- 6. Normalisation for the equality fragment. 6.1. General rules. 6.2. The 'subterm substitution' rule. 6.3. The [symbol]- and [symbol]-rules. 6.4. Term rewriting systems. 6.5. The transformations between proofs in the equational fragment of the LND. 6.6. The rewriting system for the LND equational logic. 6.7. The normalization procedure: some examples. 6.8. Final remarks. 6.9. Appendix: The [symbol]- and [symbol]-reductions for the LND system. 6.10. Termination property for LND(EQ)-TRS -- 7. Modal logics. 7.1. The functional interpretation. 7.2. Modal logics and the functional interpretation. 7.3. Finale -- 8. Meaning and proofs: a reflection on proof-theoretic semantics. 8.1. Proof-theoretic semantics. 8.2. Meaning, use and consequences. 8.3. Meaning and purpose. 8.4. Meaning and use. 8.5. Meaning and the explanation of consequences. 8.6. Use and the explanation of consequences. 8.7. Early signs of 'meaning-use/usefulness-consequences'. 8.8. Normalisation of proofs: the explanation of the consequences. 8.9. Concluding remarks.

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.

eBooks on EBSCOhost EBSCO eBook Subscription Academic Collection - Worldwide