Treatise on Intuitionistic Type Theory

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 ex

  • PDF / 1,617,603 Bytes
  • 203 Pages / 439.37 x 666.142 pts Page_size
  • 101 Downloads / 173 Views

DOWNLOAD

REPORT


LOGIC, EPISTEMOLOGY, AND THE UNITY OF SCIENCE VOLUME 22

Editors Shahid Rahman, University of Lille III, France John Symons, University of Texas at El Paso, U.S.A.

Editorial Board Jean Paul van Bendegem, Free University of Brussels, Belgium Johan van Benthem, University of Amsterdam, The Netherlands Jacques Dubucs, University of Paris I-Sorbonne, France Anne Fagot-Largeault, Collège de France, France Bas van Fraassen, Princeton University, U.S.A. Dov Gabbay, King’s College London, U.K. Jaakko Hintikka, Boston University, U.S.A. Karel Lambert, University of California, Irvine, U.S.A. Graham Priest, University of Melbourne, Australia Gabriel Sandu, University of Helsinki, Finland Göran Sundholm, Universiteit Leiden, The Netherlands Heinrich Wansing, Technical University Dresden, Germany Timothy Williamson, Oxford University, U.K.

Logic, Epistemology, and the Unity of Science aims to reconsider the question of the unity of science in light of recent developments in logic. At present, no single logical, semantical or methodological framework dominates the philosophy of science. However, the editors of this series believe that formal techniques like, for example, independence friendly logic, dialogical logics, multimodal logics, game theoretic semantics and linear logics, have the potential to cast new light on basic issues in the discussion of the unity of science. This series provides a venue where philosophers and logicians can apply specific technical insights to fundamental philosophical problems. While the series is open to a wide variety of perspectives, including the study and analysis of argumentation and the critical discussion of the relationship between logic and the philosophy of science, the aim is to provide an integrated picture of the scientific enterprise in all its diversity.

For further volumes: http://www.springer.com/series/6936

Johan Georg Granström

Treatise on Intuitionistic Type Theory

123

Johan Georg Granström Seestrasse 49 CH-8810 Horgen Switzerland [email protected]

ISBN 978-94-007-1735-0 e-ISBN 978-94-007-1736-7 DOI 10.1007/978-94-007-1736-7 Springer Dordrecht Heidelberg London New York Library of Congress Control Number: 2011929986 c Springer Science+Business Media B.V. 2011  No part of this work may be reproduced, stored in a retrieval system, or transmitted in any form or by any means, electronic, mechanical, photocopying, microfilming, recording or otherwise, without written permission from the Publisher, with the exception of any material supplied specifically for the purpose of being entered and executed on a computer system, for exclusive use by the purchaser of the work. Printed on acid-free paper Springer is part of Springer Science+Business Media (www.springer.com)

Contents Contents

v

List of Figures

vii

List of Tables

ix

Introduction

xi

Chapter I. Prolegomena § 1. A threefold correspondence § 2. The acts of the mind § 3. The principle of compositionality § 4. Lingua characteristica

1 1 4 6 9

Chapter II. Truth and Knowledge § 1. The meaning of meanin