BIBLIOPOLIS, EDIZIONI DI FILOSOFIA E SCIENZE
Via Arangio Ruiz 83-80122 Napoli-Italy
Telephone +39-081-664606
Fax +39-081-7616273


P. Martin-Löf, Intuitionistic Type Theory, pp. XII-92, 1984.

ISBN 88-7088-105-9
   Esaurit

    
STUDIES IN PROOF THEORY - LECTURE NOTES

CONTENTS

Introductory remarks
Proposition and judgements
Explanations of the forms of judgement
Propositions
Rules of equality
Hypothetical judgements and substitution rules
Judgements with more  than one assumption and contexts
Sets and categories
General remarks on the rules
Cartesian product of a family of sets
Definitional equality
Applications of the cartesian product
Disjoint union of a family of sets
Application of disjoint union
The axiome of choice
The notion of such that
Disjoint union of two sets
Propositional equality
Finite sets
Consistency
Natural numbers
Lists
Wellorderings
Universes


[Homepage]