+612 9045 4394
$7.95 Delivery per order to Australia and New Zealand
100% Australian owned
Over a hundred thousand in-stock titles ready to ship
History and Philosophy of Constructive Type Theory : Synthese Library - Giovanni Sommaruga

History and Philosophy of Constructive Type Theory

Synthese Library

Hardcover Published: 31st July 2000
ISBN: 9780792361800
Number Of Pages: 367

Share This Book:


or 4 easy payments of $73.38 with Learn more
Ships in 10 to 15 business days

Earn 587 Qantas Points
on this Book

Other Available Editions (Hide)

  • Paperback View Product Published: 7th December 2010
    Ships in 10 to 15 business days

A comprehensive survey of Martin-Lof's constructive type theory, considerable parts of which have only been presented by Martin-Lof in lecture form or as part of conference talks. Sommaruga surveys the prehistory of type theory and its highly complex development through eight different stages from 1970 to 1995. He also provides a systematic presentation of the latest version of the theory, as offered by Martin-Lof at Leiden University in Fall 1993. This presentation gives a fuller and updated account of the system. Earlier, brief presentations took no account of the issues related to the type-theoretical approach to logic and the foundations of mathematics, while here they are accorded an entire part of the book.
Readership: Comprehensive accounts of the history and philosophy of constructive type theory and a considerable amount of related material. Readers need a solid background in standard logic and a first, basic acquaintance with type theory.

The Present Version of Constructive Type Theory (1995)p. 1
Types and Objects (Non-Dependent and Non-Function)p. 9
Dependent Types and Dependent Objects (or Families of Types and Fcts. in the Oldfashioned Sense)p. 19
Function Types and Function Objects (or Function Types and Fcts. in the Modern Sense)p. 24
Digression. Explicit Substitutionsp. 33
Digression. Explicit (Abbreviatory) and Partial (Conditional) Definitions in Constructive Type Theoryp. 45
Sets and Elementsp. 49
Propositions and Proof-Objectsp. 59
Digression, Syntax and Semantics/the Theory of Indirect Reference in Constructive Type Theoryp. 67
Constructive Set Theory: Ground Sets, Dependent Sets and Sets of Different Sizesp. 74
Constructive Logicp. 125
The Curry - Howard Isomorphism or the Propositions-as-Sets Interpretationp. 158
An Extension of the Curry - Howard Isomorphism to Sequents or the Sequents-as-Types Interpretationp. 161
Metatheoretical Considerationsp. 167
The Identity Issue: The Many Faces of Identity in Constructive Type Theoryp. 167
The Judgement Issuep. 177
Traditional Metamathematical Issues: Consistency, Completeness, Decidability, in a New Frameworkp. 203
Constructive Type Theory and the Traditional Points of View on the Foundations of Mathematicsp. 211
History of Constructive Type Theory (1970-95)p. 219
Forms of Symbolic Expressions/Sentences/Judgementsp. 219
The Nation of Type and the Splitting of Type (Set/Type)p. 222
From Metamathematical Semantics to Direct Semantics and Other Semantical Mattersp. 224
Constructive Type Theory as a Mathematical Language to be Usedp. 249
Kinds of Equality/Identityp. 271
Universesp. 283
Variations on the Basic Stock Rules [Pi], [Sigma], +, N[Subscript n], Np. 291
Monomorphism/Polymorphism and Decidability/Undecidability of Type Checkingp. 299
Appendix. The Battle with the Direct Semantical Turn: From Type Theory to Logical Theory and Backp. 300
Philosophical and Technical Prehistory of Constructive Type Theory (1880-1970)p. 311
Philosophical Sources of Constructive Type Theory: Two Approaches to Logicp. 311
Technical Sources of Constructive Type Theoryp. 318
Conclusionp. 347
Referencep. 349
Table of Contents provided by Blackwell. All Rights Reserved.

ISBN: 9780792361800
ISBN-10: 0792361806
Series: Synthese Library
Audience: General
Format: Hardcover
Language: English
Number Of Pages: 367
Published: 31st July 2000
Country of Publication: NL
Dimensions (cm): 24.74 x 16.87  x 2.74
Weight (kg): 0.74

Earn 587 Qantas Points
on this Book