The Functional Interpretation of Logical Deduction

The following sections are included:

• Contents

• Preface

• Overview

The following sections are included:

• 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
    • β-type reductions
    • β-equality
    • η-type reductions
    • η-equality
    • ζ-type reductions: The permutative reductions turned unidirectional
    • ζ-type equality

The following sections are included:

• Introduction

• Origins

• Types and propositions

• λ-abstraction and implication

• Consistency proof

• Systems of implication and combinators

• Finale

The following sections are included:

• Preamble

• 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
    • Quine's system
    • Fine's generalised system
    • Incorporating annotations into the object language
  • Axiomatic systems based on the notion of ‘such that’
    • Hilbert's η- and ε-calculi
    • Hailperin's ν-calculus

• Model-theoretic semantics
  • Constants versus variables revisited
    • Skolem resolution
    • Herbrand resolution
  • Eliminability and conservative extensions

• Finale
  • Extensions to higher-order existentials
  • Further connections to model-theoretic interpretations

• Examples of deduction
  • Generic examples
  • Specific examples
    • Inclusive logics
    • Classical logic and Skolem functions

The following sections are included:

• Preamble

• 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
    • Analyzing the ζ-reductions
  • Proving the termination property
    • Proof for the subset of β reductions
    • Proof for the subset of η reductions
    • Proof for the subset of ζ reductions
  • Proving the confluence property

• Examples of transformations between proofs

• Final remarks

• Appendix: Proof of confluence of LND-TRS

The following sections are included:

• Introduction

• Labelled deduction
  • Identifiers for (compositions of) equalities
  • The proof rules

• Finale

The following sections are included:

• Preamble

• 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
    • Symmetry
    • Transitivity
    • Substitution
    • The β_rewr reduction
    • The η_rewr reduction
  • Transformations on the rewrite reasons
    • Symmetry
    • Transitivity

• The rewriting system for the LND equational logic
  • Termination property for the LND_EQ-TRS
  • Confluence property for the LND_EQ-TRS
  • The normalization theorems

• The normalization procedure: some examples

• Final remarks

• Appendix: The β- and η-reductions for the LND system
  • β-type reductions
    • β-equality
  • η-type reductions
    • η-equality
  • ζ-type transformations: The permutative transformations
    • ζ-equality

• Termination property for LND_EQ-TRS

The following sections are included:

• Preamble

• The functional interpretation
  • Handling assumptions with ‘world’ variables
  • Natural deduction with an extra parameter
    • Montague's types, and world-variables as senses
    • Open assumptions and the 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

The following sections are included:

• 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

The following sections are included:

• Bibliography

• Index