Truth, Proof and Infinity

A Theory of Constructions and Constructive Reasoning

  • Peter Fletcher

Part of the Synthese Library book series (SYLI, volume 276)

Table of contents

  1. Front Matter
    Pages i-ix
  2. Philosophical Foundations

    1. Peter Fletcher
      Pages 1-12
    2. Peter Fletcher
      Pages 13-23
    3. Peter Fletcher
      Pages 24-40
    4. Peter Fletcher
      Pages 41-50
    5. Peter Fletcher
      Pages 51-69
    6. Peter Fletcher
      Pages 70-76
    7. Peter Fletcher
      Pages 77-81
    8. Peter Fletcher
      Pages 82-97
    9. Peter Fletcher
      Pages 98-116
    10. Peter Fletcher
      Pages 117-127
    11. Peter Fletcher
      Pages 128-139
  3. The Theory of Constructions

    1. Peter Fletcher
      Pages 140-141
    2. Peter Fletcher
      Pages 142-149
    3. Peter Fletcher
      Pages 150-161
    4. Peter Fletcher
      Pages 199-208
    5. Peter Fletcher
      Pages 209-211
    6. Peter Fletcher
      Pages 216-230

About this book

Introduction

Constructive mathematics is based on the thesis that the meaning of a mathematical formula is given, not by its truth-conditions, but in terms of what constructions count as a proof of it. However, the meaning of the terms `construction' and `proof' has never been adequately explained (although Kriesel, Goodman and Martin-Löf have attempted axiomatisations). This monograph develops precise (though not wholly formal) definitions of construction and proof, and describes the algorithmic substructure underlying intuitionistic logic. Interpretations of Heyting arithmetic and constructive analysis are given.
The philosophical basis of constructivism is explored thoroughly in Part I. The author seeks to answer objections from platonists and to reconcile his position with the central insights of Hilbert's formalism and logic.
Audience: Philosophers of mathematics and logicians, both academic and graduate students, particularly those interested in Brouwer and Hilbert; theoretical computer scientists interested in the foundations of functional programming languages and program correctness calculi.

Keywords

Arithmetic algorithms constructivism logic programming language proof sequent calculus set theory

Authors and affiliations

  • Peter Fletcher
    • 1
  1. 1.Department of MathematicsKeele UniversityUK

Bibliographic information

  • DOI https://doi.org/10.1007/978-94-017-3616-9
  • Copyright Information Springer Science+Business Media B.V. 1998
  • Publisher Name Springer, Dordrecht
  • eBook Packages Springer Book Archive
  • Print ISBN 978-90-481-5105-9
  • Online ISBN 978-94-017-3616-9
  • About this book