| |
| |
| Preface | |
| |
| |
| Overview | |
| |
| |
| |
| Labelled Natural Deduction | |
| |
| |
| |
| The r�le of the labels | |
| |
| |
| |
| Dividing the tasks: A functional calculus on the labels, a logical calculus on the formula | |
| |
| |
| |
| Reassessing Frege's two-dimensional calculus | |
| |
| |
| |
| Canonical proofs and normalisation | |
| |
| |
| |
| Canonical proofs | |
| |
| |
| |
| Normalisation | |
| |
| |
| |
| The Functional Interpretation of Implication | |
| |
| |
| |
| Introduction | |
| |
| |
| |
| Origins | |
| |
| |
| |
| Types and propositions | |
| |
| |
| |
| A-abstraction and implication | |
| |
| |
| |
| Consistency proof | |
| |
| |
| |
| Systems of implication and combinators | |
| |
| |
| |
| Finale | |
| |
| |
| |
| The Existential Quantifier | |
| |
| |
| |
| Motivation | |
| |
| |
| |
| The pairing interpretation | |
| |
| |
| |
| Quantifiers and normalisation | |
| |
| |
| |
| Introducing variables for the Skolem dependency functions | |
| |
| |
| |
| The hiding principle | |
| |
| |
| |
| Other approaches to existential quantification | |
| |
| |
| |
| Systems of natural deduction based on direct existential instantiation | |
| |
| |
| |
| Axiomatic systems based on the notion of 'such that' | |
| |
| |
| |
| Model-theoretic semantics | |
| |
| |
| |
| Constants versus variables revisited | |
| |
| |
| |
| Eliminability and conservative extensions | |
| |
| |
| |
| Finale | |
| |
| |
| |
| Extensions to higher-order existentials | |
| |
| |
| |
| Further connections to model-theoretic interpretations | |
| |
| |
| |
| Examples of deduction | |
| |
| |
| |
| Generic examples | |
| |
| |
| |
| Specific examples | |
| |
| |
| |
| Normalisation | |
| |
| |
| |
| Introduction | |
| |
| |
| |
| Proof transformations in labelled deduction | |
| |
| |
| |
| Equivalences between proofs in LND | |
| |
| |
| |
| The term rewriting system for LND | |
| |
| |
| |
| Defining the LND-TRS | |
| |
| |
| |
| The sort decreasing property | |
| |
| |
| |
| Defining an order | |
| |
| |
| |
| Proving the termination property | |
| |
| |
| |
| Proving the confluence property | |
| |
| |
| |
| Examples of transformations between proofs | |
| |
| |
| |
| Final remarks | |
| |
| |
| |
| Natural Deduction for Equality | |
| |
| |
| |
| Introduction | |
| |
| |
| |
| Labelled deduction | |
| |
| |
| |
| Identifiers for (compositions of) equalities | |
| |
| |
| |
| The proof rules | |
| |
| |
| |
| Finale | |
| |
| |
| |
| Normalisation for the Equality Fragment | |
| |
| |
| |
| General rules | |
| |
| |
| |
| The 'subterm substitution' rule | |
| |
| |
| |
| The �- and �-rules | |
| |
| |
| |
| Term rewriting systems | |
| |
| |
| |
| Termination property | |
| |
| |
| |
| Confluence property | |
| |
| |
| |
| The completion procedure | |
| |
| |
| |
| The transformations between proofs in the equational fragment of the LND | |
| |
| |
| |
| Reductions on the rewrite sequence | |
| |
| |
| |
| Transformations on the rewrite reasons | |
| |
| |
| |
| The rewriting system for the LND equational logic | |
| |
| |
| |
| Termination property for the LND<sub>EQ</sub>-TRS | |
| |
| |
| |
| Confluence property for the LND<sub>EQ</sub>-TRS | |
| |
| |
| |
| The normalization theorems | |
| |
| |
| |
| The normalization procedure: some examples | |
| |
| |
| |
| Final remarks | |
| |
| |
| |
| Appendix: The �- and �-reductions for the LND system | |
| |
| |
| |
| �-type reductions | |
| |
| |
| |
| �-type reductions | |
| |
| |
| |
| �-type transformations: The permutative transformations | |
| |
| |
| |
| Termination property for LND<sub>EQ</sub>-TRS | |
| |
| |
| |
| Modal Logics | |
| |
| |
| |
| The functional interpretation | |
| |
| |
| |
| Handling assumptions with 'world' variables | |
| |
| |
| |
| Natural deduction with an extra parameter | |
| |
| |
| |
| Connections with Kripke's truth definition | |
| |
| |
| |
| Connections with Gentzen's sequent calculus | |
| |
| |
| |
| Modal logics and the functional interpretation | |
| |
| |
| |
| Chellas' RM rule for standard normative logics | |
| |
| |
| |
| Modal logic K | |
| |
| |
| |
| Modal logic D | |
| |
| |
| |
| Modal logic T | |
| |
| |
| |
| Modal logic B | |
| |
| |
| |
| Modal logic S4 and its parallel with intuitionistic logic | |
| |
| |
| |
| Grzegorczyk's extension of S4 | |
| |
| |
| |
| Modal logic S5 and its parallel with classical logic | |
| |
| |
| |
| Non-normal modal logics | |
| |
| |
| |
| Problematic cases: The scope of 'necessity' | |
| |
| |
| |
| Finale | |
| |
| |
| |
| Meaning and Proofs: A Reflection on Proof-Theoretic Semantics | |
| |
| |
| |
| Proof-theoretic semantics | |
| |
| |
| |
| Meaning, use and consequences | |
| |
| |
| |
| Meaning and purpose | |
| |
| |
| |
| Meaning and use | |
| |
| |
| |
| Meaning and the explanation of consequences | |
| |
| |
| |
| Use and the explanation of consequences | |
| |
| |
| |
| Early signs of 'meaning-use/usefulness-consequences' | |
| |
| |
| |
| Normalisation of proofs: the explanation of the consequences | |
| |
| |
| |
| Concluding remarks | |
| |
| |
| Bibliography | |
| |
| |
| Index | |