Intuitionistic Type Theory Per Martin-Lo¨f Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980 Contents Introductory remarks. . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 Propositions and judgements . . . . . . . . . . . . . . . . . . . . . . . 2 Explanations of the forms of judgement . . . . . . . . . . . . . . . . . 4 Propositions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 Rules of equality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 Hypothetical judgements and substitution rules . . . . . . . . . . . . . 9 Judgements with more than one assumption and contexts . . . . . . . 10 Sets and categories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 General remarks on the rules . . . . . . . . . . . . . . . . . . . . . . . 13 Cartesian product of a family of sets . . . . . . . . . . . . . . . . . . . 13 Definitional equality . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 Applications of the cartesian product . . . . . . . . . . . . . . . . . . . 16 Disjoint union of a family of sets . . . . . . . . . . . . . . . . . . . . . 20 Applications of the disjoint union . . . . . . . . . . . . . . . . . . . . . 22 The axiom of choice . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 The notion of such that . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Disjoint union of two sets . . . . . . . . . . . . . . . . . . . . . . . . . 29 Propositional equality . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Finite sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 Consistency . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 Natural numbers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 Lists . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 Wellorderings . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 Universes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 Preface These lectures were given in Padova at the Laboratorio per Ricerche di Di- namica dei Sistemi e di Elettronica Biomedica of the Consiglio Nazionale delle Ricerche during the month of June 1980. I am indebted to Dr. Enrico Pagello of that laboratory for the opportunity of so doing. The audience was made up by philosophers, mathematicians and computer scientists. Accordingly, I tried to say something which might be of interest to each of these three cate- gories. Essentially the same lectures, albeit in a somewhat improved and more advanced form, were given later in the same year as part of the meeting on Konstruktive Mengenlehre und Typentheorie which was organized in Munich byProf.Dr.HelmutSchwichtenberg, towhomIamindebtedfortheinvitation, during the week 29 September – 3 October 1980. ThemainimprovementoftheMunichlectures,ascomparedwiththosegiven in Padova, was the adoption of a systematic higher level (Ger. Stufe) notation which allows me to write simply Π(A,B), Σ(A,B), W(A,B), λ(b), E(c,d), D(c,d,e), R(c,d,e), T(c,d) instead of (Πx∈A)B(x), (Σx∈A)B(x), (Wx∈A)B(x), (λx)b(x), E(c,(x,y)d(x,y)), D(c,(x)d(x),(y)e(y)), R(c,d,(x,y)e(x,y)), T(c,(x,y,z)d(x,y,z)), respectively. Moreover, the use of higher level variables and constants makes it possibletoformulatetheeliminationandequalityrulesforthecartesianproduct insuchawaythattheyfollowthesamepatternastheeliminationandequality rules for all the other type forming operations. In their new formulation, these rules read Π-elimination (y(x)∈B(x) (x∈A)) c∈Π(A,B) d(y)∈C(λ(y)) F(c,d)∈C(c) and Π-equality (x∈A) (y(x)∈B(x) (x∈A)) b(x)∈B(x) d(y)∈C(λ(y)) F(λ(b),d)=d(b)∈C(λ(b)) respectively. Here y is a bound function variable, F is a new non-canonical (eliminatory) operator by means of which the binary application operation can be defined, putting Ap(c,a) ≡ F(c,(y)y(a)), and y(x)∈B(x) (x∈A) is an assumption, itself hypothetical, which has been putwithinparenthesestoindicatethatitisbeingdischarged. Aprogramofthe newformF(c,d)hasvalueeprovidedchasvalueλ(b)andd(b)hasvaluee. This rule for evaluating F(c,d) reduces to the lazy evaluation rule for Ap(c,a) when theabovedefinitionisbeingmade. ChoosingC(z)tobeB(a),thusindependent of z, and d(y) to be y(a), the new elimination rule reduces to the old one and the new equality rule to the first of the two old equality rules. Moreover, the second of these, that is, the rule c∈Π(A,B) c=(λx)Ap(c,x)∈Π(A,B) can be derived by means of the I-rules in the same way as the rule c∈Σ(A,B) c=(p(c),q(c))∈Σ(A,B) is derived by way of example on p. 33 of the main text. Conversely, the new elimination and equality rules can be derived from the old ones by making the definition F(c,d) ≡ d((x)Ap(c,x)). So, actually, they are equivalent. It only remains for me to thank Giovanni Sambin for having undertaken, at his own suggestion, the considerable work of writing and typing these notes, thereby making the lectures accessible to a wider audience. Stockholm, January 1984, Per Martin-L¨of Introductory remarks Mathematical logic and the relation between logic and mathematics have been interpreted in at least three different ways: (1) mathematicallogicassymboliclogic,orlogicusingmathematicalsymbol- ism; (2) mathematical logic as foundations (or philosophy) of mathematics; (3) mathematicallogicaslogicstudiedbymathematicalmethods,asabranch of mathematics. We shall here mainly be interested in mathematical logic in the second sense. What we shall do is also mathematical logic in the first sense, but certainly not in the third. TheprincipalproblemthatremainedafterPrincipiaMathematicawascom- pleted was, according to its authors, that of justifying the axiom of reducibility (or, as we would now say, the impredicative comprehension axiom). The rami- fied theory of types was predicative, but it was not sufficient for deriving even elementary parts of analysis. So the axiom of reducibility was added on the pragmaticgroundthatitwasneeded,althoughnosatisfactoryjustification(ex- planation)ofitcouldbeprovided. Thewholepointoftheramificationwasthen lost, so that it might just as well be abolished. What then remained was the simple theory of types. Its official justification (Wittgenstein, Ramsey) rests on the interpretation of propositions as truth values and propositional functions (of one or several variables) as truth functions. The laws of the classical propo- sitional logic are then clearly valid, and so are the quantifier laws, as long as quantificationisrestrictedtofinitedomains. However,itdoesnotseempossible tomakesenseofquantificationoverinfinitedomains,likethedomainofnatural numbers, on this interpretation of the notions of proposition and propositional function. For this reason, among others, what we develop here is an intuition- istic theory of types, which is also predicative (or ramified). It is free from the deficiency of Russell’s ramified theory of types, as regards the possibility of developing elementary parts of mathematics, like the theory of real numbers, because of the presence of the operation which allows us to form the cartesian product of any given family of sets, in particular, the set of all functions from one set to another. Intwoareas,atleast,ourlanguageseemstohaveadvantagesovertraditional foundational languages. First, Zermelo-Fraenkel set theory cannot adequately deal with the foundational problems of category theory, where the category of all sets, the category of all groups, the category of functors from one such cat- egory to another etc. are considered. These problems are coped with by means of the distinction between sets and categories (in the logical or philosophical sense, not in the sense of category theory) which is made in intuitionistic type theory. Second, present logical symbolisms are inadequate as programming languages, which explains why computer scientists have developed their own 1 languages (FORTRAN, ALGOL, LISP, PASCAL, ...) and systems of proof rules (Hoare1, Dijkstra2, ...). We have show elsewhere3 how the additional richness of type theory, as compared with first order predicate logic, makes it usable as a programming language. Propositions and judgements Herethedistinctionbetweenproposition (Ger.Satz)andassertion orjudgement (Ger. Urteil) is essential. What we combine by means of the logical operations (⊥, ⊃, &, ∨, ∀, ∃) and hold to be true are propositions. When we hold a proposition to be true, we make a judgement: proposition A is true judgement Inparticular,thepremissesandconclusionofalogicalinferencearejudgements. The distinction between propositions and judgements was clear from Frege to Principia. These notions have later been replaced by the formalistic notions of formula and theorem (in a formal system), respectively. Contrary to formulas, propositionsarenotdefinedinductively. Sotospeak,theyformanopenconcept. In standard textbook presentations of first order logic, we can distinguish three quite separate steps: (1) inductive definition of terms and formulas, (2) specification of axioms and rules of inference, (3) semantical interpretation. Formulas and deductions are given meaning only through semantics, which is usually done following Tarski and assuming set theory. What we do here is meant to be closer to ordinary mathematical practice. We will avoid keeping form and meaning (content) apart. Instead we will at the same time display certain forms of judgement and inference that are used in mathematical proofs and explain them semantically. Thus we make explicit whatisusuallyimplicitlytakenforgranted. Whenonetreatslogicasanyother branch of mathematics, as in the metamathematical tradition originated by Hilbert, such judgements and inferences are only partially and formally repre- sentedintheso-calledobjectlanguage,whiletheyareimplicitlyused,asinany other branch of mathematics, in the so-called metalanguage. 1C.A.Hoare,Anaxiomaticbasisofcomputerprogramming,CommunicationsoftheACM, Vol.12,1969,pp.576–580and583. 2E.W.Dijkstra,AdisplineofProgramming,PrenticeHall,EnglewoodCliffs,N.J.,1976. 3P. Martin-Lo¨f, Constructive mathematics and computer programming, Logic, Method- ology and Philosophy of Science VI, Edited by L. J. Cohen, J. Los, H. Pfeiffer and K.- P.Podewski,North-Holland,Amsterdam,1982,pp.153–175. 2 Ourmainaimistobuildupasystemofformalrulesrepresentinginthebest possiblewayinformal(mathematical)reasoning. Intheusualnaturaldeduction style, the rules given are not quite formal. For instance, the rule A A∨B takes for granted that A and B are formulas, and only then does it say that we can infer A∨B to be true when A is true. If we are to give a formal rule, we have to make this explicit, writing A prop. B prop. A true A∨B true or A, B prop. (cid:96)A (cid:96)A∨B where we use, like Frege, the symbol (cid:96) to the left of A to signify that A is true. In our system of rules, this will always be explicit. Aruleofinferenceisjustifiedbyexplainingtheconclusionontheassumption thatthepremissesareknown. Hence, beforearuleofinferencecanbejustified, it must be explained what it is that we must know in order to have the right to make a judgement of any one of the various forms that the premisses and conclusion can have. We use four forms of judgement: (1) A is a set (abbr. A set), (2) A and B are equal sets (A=B), (3) a is an element of the set A (a∈A), (4) a and b are equal elements of the set A (a=b∈A). , (If we read ∈ literally as (cid:15)στ´ι, then we might write A ∈ Set, A = B ∈ Set, a∈El(A),a=b∈El(A),respectively.) Ofcourse,anysyntacticvariablescould beused;theuseofsmalllettersforelementsandcapitallettersforsetsisonlyfor convenience. Notethat,inordinarysettheory,a∈banda=barepropositions, whiletheyarejudgementshere. AjudgementoftheformA=Bhasnomeaning unless we already know A and B to be sets. Likewise, a judgement of the form a∈A presupposes that A is a set, and a judgement of the form a=b∈A presupposes, first, that A is a set, and, second, that a and b are elements of A. 3 Each form of judgement admits of several different readings, as in the table: A set a∈A A is a set a is an element of the set A A is nonempty A is a proposition a is a proof (construction) of A is true the proposition A A is an intention a is a method of fulfilling A is fulfillable (expectation) (realizing) the intention (realizable) (expectation) A A is a problem a is a method of solving the A is solvable (task) problem (doing the task) A The second, logical interpretation is discussed together with rules below. The third was suggested by Heyting4 and the fourth by Kolmogorov5. The last is veryclosetoprogramming. “aisamethod...” canbereadas“aisaprogram ...”. Since programming languages have a formal notation for the program a, but not for A, we complete the sentence with “... which meets the specifica- tion A”. In Kolmogorov’s interpretation, the word problem refers to something tobedoneandthewordprogramtohowtodoit. Theanalogybetweenthefirst and the second interpretation is implicit in the Brouwer-Heyting interpretation ofthelogicalconstants. ItwasmademoreexplicitbyCurryandFeys6,butonly for the implicational fragment, and it was extended to intuitionistic first order arithmetic by Howard7. It is the only known way of interpreting intuitionistic logic so that the axiom of choice becomes valid. To distinguish between proofs of judgements (usually in tree-like form) and proofs of propositions (here identified with elements, thus to the left of ∈) we reserve the word construction for the latter and use it when confusion might occur. Explanations of the forms of judgement For each one of the four forms of judgement, we now explain what a judgement of that form means. We can explain what a judgement, say of the first form, means by answering one of the following three questions: What is a set? Whatisitthatwemustknowinordertohavetherighttojudgesomething to be a set? 4A.Heyting,DieintuitionistischeGrundlegungderMathematik,Erkenntnis,Vol.2,1931, pp.106–115. 5A.N.Kolmogorov,ZurDeutungderintuitionistischenLogik,MathematischeZeitschrift, Vol.35,1932,pp.58–65. 6H. B. Curry and R. Feys, Combinatory Logic, Vol. 1, North-Holland, Amsterdam, 1958, pp.312–315. 7W. A. Howard, The formulae-as-types notion of construction, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press, London, 1980, pp.479–490. 4