Cut Elimination in Categories
Proof theory and category theory were first drawn together by Lambek some 30 years ago but, until now, the most fundamental notions of category theory (as opposed to their embodiments in logic) have not been explained systematically in terms of proof theo
- PDF / 20,050,723 Bytes
- 240 Pages / 439.37 x 666.142 pts Page_size
- 30 Downloads / 221 Views
TRENDS IN LOGIC Studia Logica Library VOLUME 6 Managing Editor Ryszard W6jcicki, Institute of Philosophy and Sociology, Polish Academy of Sciences, Warsaw, Poland Editors Petr Hajek, Institute of Computer Sciences, Academy of Sciences of the Czech Republic, Prague, Czech Republic David Makinson, Ville d' Avray, France Daniele Mundici, Department of Computer Sciences, University of Milan, Italy Krister Segerberg, Department of Philosophy, Uppsala University, Uppsala, Sweden Alasdair Urquhart, Department of Philosophy, University of Toronto, Canada Assistant Editor Jacek Malinowski, Box 61, UPT 00-953, Warszawa 37, Poland
SCOPE OF THE SERIES Trends in Logic is a book series covering essentially the same area as the journal Studia Logica - that is, contemporary formal logic and its applications and relations to other disciplines. These include artificial intelligence, informatics, cognitive science, philosophy of science, and the philosophy of language. However, this list is not exhaustive, moreover, the range of applications, comparisons and sources of inspiration is open and evolves over time.
Volume Editor Krister Segerberg
KOSTA DOSEN University o/Toulouse Ill, Toulouse, France and Mathematical Institute, Belgrade, Yugoslavia
CUT ELIMINATION IN CATEGORIES
SPRINGER-SCIENCE+BUSINESS MEDIA, B.Y.
A C.l.P. Catalogue record for this book is available from the Library of Congress.
ISBN 978-90-481-5226-1
ISBN 978-94-017-1207-1 (eBook)
DOI 10.1007/978-94-017-1207-1
Printed on acid-free paper
All Rights Reserved © 1999 Springer Science+Business Media Dordrecht Originally published by K1uwer Academic Publishers in 1999 No part of the material protected by this copyright notice may be reproduced or utilized in any form or by any means, electronic or mechanical, including photocopying, recording or by any information storage and retrieval system, without written permission from the copyright owner.
TABLE OF CONTENTS
PREFACE
~
INTRODUCTION § 0.1. Aim and scope § 0.2. Summary of the work § 0.3. An introduction to cut elimination and adjointness § 0.3.1. Cut elimination § 0.3.2. Adjointness § 0.3.3. Cut elimination and adjointness § 0.3.4. Sequent systems and natural deduction § 0.3.5. Four types of sequent rules § 0.3.6. Identity atomization
1 1 3 5 5 6 8 11 12 15
CHAPTER 1. CATEGORIES § 1.1. Foundations § 1.2. Morphisms and naturalness § 1.3. Graphs, graph-morphisms and transformations § 1.4. Deductive systems, functors, natural transformations and categories § 1.5. Equivalence of categories § 1.6. Free deductive systems § 1.7. Free categories § 1.8. Cut elimination in free categories § 1.8.1. Cut Disintegration in free categories § 1.8.2. Necessary conditions for Cut Disintegration in free categories § 1.8.3. Particular and Total Cut Elimination § 1.9. Representing deductive systems and categories (Stone, Cayley and Yoneda) § 1.9.1. Cone graphs § 1.9.2. From graphs to deductive systems
17 17 18 19
v
22 24 26 29 31 32 34 35 36 38 39
vi From deductive systems to categories The image of left compositiona
Data Loading...
