Logo - springer
Slogan - springer

Philosophy | Treatise on Intuitionistic Type Theory

Treatise on Intuitionistic Type Theory

Granström, Johan Georg

2011, XIV, 198 p.

Available Formats:
eBook
Information

Springer eBooks may be purchased by end-customers only and are sold without copy protection (DRM free). Instead, all eBooks include personalized watermarks. This means you can read the Springer eBooks across numerous devices such as Laptops, eReaders, and tablets.

You can pay for Springer eBooks with Visa, Mastercard, American Express or Paypal.

After the purchase you can directly download the eBook file or read it online in our Springer eBook Reader. Furthermore your eBook will be stored in your MySpringer account. So you can always re-download your eBooks.

 
$139.00

(net) price for USA

ISBN 978-94-007-1736-7

digitally watermarked, no DRM

Included Format: PDF

download immediately after purchase


learn more about Springer eBooks

add to marked items

Hardcover
Information

Hardcover version

You can pay for Springer Books with Visa, Mastercard, American Express or Paypal.

Standard shipping is free of charge for individual customers.

 
$179.00

(net) price for USA

ISBN 978-94-007-1735-0

free shipping for individuals worldwide

usually dispatched within 3 to 5 business days


add to marked items

Softcover
Information

Softcover (also known as softback) version.

You can pay for Springer Books with Visa, Mastercard, American Express or Paypal.

Standard shipping is free of charge for individual customers.

 
$179.00

(net) price for USA

ISBN 978-94-007-3639-9

free shipping for individuals worldwide

usually dispatched within 3 to 5 business days


add to marked items

  • The author was a PhD student of Per Martin-Löf, the inventor of intuitionistic type theory, and has unique insights in the field.
  • There are many interesting connections between philosophy, logic, and computer science.
  • A new and pedagogical treatment of the double negation interpretation is included.
Intuitionistic type theory can be described, somewhat boldly, as a fulfillment of the dream of a universal language for science.  In particular, intuitionistic type theory is a foundation for mathematics and a programming language.  This book expounds several aspects of intuitionistic type theory, such as the notion of set, reference vs. computation, assumption, and substitution.  Moreover, the book includes philosophically relevant sections on the principle of compositionality, lingua characteristica, epistemology, propositional logic, intuitionism, and the law of excluded middle. Ample historical references are given throughout the book.

Content Level » Research

Keywords » intuitionism - intuitionistic type theory - lingua characteristica - notion of knowledge - notion of truth

Related subjects » Computational Science & Engineering - Logic & Philosophy of Language - Mathematics - Philosophical Traditions - Philosophy - Theoretical Computer Science

Table of contents 

Contents.- List of Figures.- List of Tables.- Introduction.- Chapter I. Prolegomena. 1. A treefold correspondence.- 2. The acts of the mind.- 3. The principle of compositionality.- 4. Lingua characteristica.- Chapter II. Truth of Knowledge. 1. The meaning of meaning.- 2. A division of being.- 3. Mathematical entities.- 4. Judgement and assertion.- 5. Reasoning and demonstration.- 6. The proposition.- 7. The laws of logic.- 8. Variables and generality.- 9. Division of definitions.- Chapter III. The Notion of Set. 1. A History of set-like notions.- 2. Set-theoretical notation.- 3. Making universal concepts ito objects of thought.- 4. Canonical sets and elements.- 5. How to define a canonical set.- 6. More canonical sets.- Chapter IV. Reference and Computation. 1. Functions, algorithms, and programs.- 2. The concept of function.- 3. A formalization of computation.- 4. Noncanonical sets and elements.- 5. Nominal definitions.- 6. Functions as objects.- 7. Families of sets.- Chapter V. Assumption and Substitution. 1. The concept of function revisited.- 2. Hypothetical assertions.- 3. The calculus of substitutions.- 4. Sets and elements in hypothetical assertions.- 5. Closures and λ -calculas.- 6. The disjoint union of a family of sets.- 7. Elimination rukes.- 8. Propositions as sets.- Chapter VI. Intuitionism. 1. The intuitionistic interpretation of apagoge.- 2. the law of excluded middle.- 3. The philosophy of mathematics.- Bibliography.- Index of Proper Names.- Index of Subjects.-

Popular Content within this publication 

 

Articles

Read this Book on Springerlink

Services for this book

New Book Alert

Get alerted on new Springer publications in the subject area of Epistemology.