Intuitionistic Type Theory. Per Martin-Löf - PDF

Description
Intuitionistic Type Theory Per Martin-Löf Notes by Giovanni Sambin of a series of lectures given in Padua, June Contents Introductory remarks Propositions and judgements

Please download to get full document.

View again

of 20
All materials on our website are shared by users. If you have any questions about copyright issues, please report us to resolve them. We are always happy to assist you.
Information
Category:

Humor

Publish on:

Views: 47 | Pages: 20

Extension: PDF | Download: 0

Share
Transcript
Intuitionistic Type Theory Per Martin-Löf Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980 Contents Introductory remarks Propositions 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 Applications of the disjoint union The axiom of choice The notion of such that Disjoint union of two sets Propositional equality Finite sets Consistency Natural numbers Lists Wellorderings Universes Preface These lectures were given in Padova at the Laboratorio per Ricerche di Dinamica dei Sistemi e di Elettronica Biomedica of the Consiglio Nazionale delle Ricerche during the month of June 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 categories. 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 by Prof. Dr. Helmut Schwichtenberg, to whom I am indebted for the invitation, during the week 29 September 3 October The main improvement of the Munich lectures, as compared with those given in Padova, was the adoption of a systematic higher level (Ger. Stufe) notation which allows me to write simply instead of Π(A, B), Σ(A, B), W(A, B), λ(b), E(c, d), D(c, d, e), R(c, d, e), T(c, d) (Π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 possible to formulate the elimination and equality rules for the cartesian product in such a way that they follow the same pattern as the elimination and equality rules for all the other type forming operations. In their new formulation, these rules read Π-elimination and (y(x) B(x) ) c Π(A, B) d(y) C(λ(y)) F(c, d) C(c) Π-equality (y(x) B(x) ) 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) is an assumption, itself hypothetical, which has been put within parentheses to indicate that it is being discharged. A program of the new form F(c, d) has value e provided c has value λ(b) and d(b) has value e. This rule for evaluating F(c, d) reduces to the lazy evaluation rule for Ap(c, a) when the above definition is being made. Choosing C(z) to be B(a), thus independent 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öf Introductory remarks Mathematical logic and the relation between logic and mathematics have been interpreted in at least three different ways: (1) mathematical logic as symbolic logic, or logic using mathematical symbolism; (2) mathematical logic as foundations (or philosophy) of mathematics; (3) mathematical logic as logic studied by mathematical methods, as a branch 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. The principal problem that remained after Principia Mathematica was completed was, according to its authors, that of justifying the axiom of reducibility (or, as we would now say, the impredicative comprehension axiom). The ramified 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 pragmatic ground that it was needed, although no satisfactory justification (explanation) of it could be provided. The whole point of the ramification was then 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 propositional logic are then clearly valid, and so are the quantifier laws, as long as quantification is restricted to finite domains. However, it does not seem possible to make sense of quantification over infinite domains, like the domain of natural numbers, on this interpretation of the notions of proposition and propositional function. For this reason, among others, what we develop here is an intuitionistic 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. In two areas, at least, our language seems to have advantages over traditional 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 category 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 (Hoare 1, Dijkstra 2,... ). We have show elsewhere 3 how the additional richness of type theory, as compared with first order predicate logic, makes it usable as a programming language. Propositions and judgements Here the distinction between proposition (Ger. Satz) and assertion or judgement (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 In particular, the premisses and conclusion of a logical inference are judgements. 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, propositions are not defined inductively. So to speak, they form an open concept. 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 what is usually implicitly taken for granted. When one treats logic as any other branch of mathematics, as in the metamathematical tradition originated by Hilbert, such judgements and inferences are only partially and formally represented in the so-called object language, while they are implicitly used, as in any other branch of mathematics, in the so-called metalanguage. 1 C. A. Hoare, An axiomatic basis of computer programming, Communications of the ACM, Vol. 12, 1969, pp and E. W. Dijkstra, A displine of Programming, Prentice Hall, Englewood Cliffs, N.J., P. Martin-Löf, Constructive mathematics and computer programming, Logic, Methodology and Philosophy of Science VI, Edited by L. J. Cohen, J. Los, H. Pfeiffer and K.- P. Podewski, North-Holland, Amsterdam, 1982, pp Our main aim is to build up a system of formal rules representing in the best possible way informal (mathematical) reasoning. In the usual natural deduction 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 or A prop. B prop. A true A B true A, B prop. A A B where we use, like Frege, the symbol to the left of A to signify that A is true. In our system of rules, this will always be explicit. A rule of inference is justified by explaining the conclusion on the assumption that the premisses are known. Hence, before a rule of inference can be justified, 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 ɛστί,, then we might write A Set, A = B Set, a El(A), a = b El(A), respectively.) Of course, any syntactic variables could be used; the use of small letters for elements and capital letters for sets is only for convenience. Note that, in ordinary set theory, a b and a = b are propositions, while they are judgements here. A judgement of the form A = B has no meaning 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 Heyting 4 and the fourth by Kolmogorov 5. The last is very close to programming. a is a method... can be read as a is a program.... Since programming languages have a formal notation for the program a, but not for A, we complete the sentence with... which meets the specification A. In Kolmogorov s interpretation, the word problem refers to something to be done and the word program to how to do it. The analogy between the first and the second interpretation is implicit in the Brouwer-Heyting interpretation of the logical constants. It was made more explicit by Curry and Feys 6, but only for the implicational fragment, and it was extended to intuitionistic first order arithmetic by Howard 7. 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? What is it that we must know in order to have the right to judge something to be a set? 4 A. Heyting, Die intuitionistische Grundlegung der Mathematik, Erkenntnis, Vol. 2, 1931, pp A. N. Kolmogorov, Zur Deutung der intuitionistischen Logik, Mathematische Zeitschrift, Vol. 35, 1932, pp H. B. Curry and R. Feys, Combinatory Logic, Vol. 1, North-Holland, Amsterdam, 1958, pp W. 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 What does a judgement of the form A is a set mean? The first is the ontological (ancient Greek), the second the epistemological (Descartes, Kant,... ), and the third the semantical (modern) way of posing essentially the same question. At first sight, we could assume that a set is defined by prescribing how its elements are formed. This we do when we say that the set of natural numbers N is defined by giving the rules: 0 N a N a N by which its elements are constructed. However, the weakness of this definition is clear: 10 10, for instance, though not obtainable with the given rules, is clearly an element of N, since we know that we can bring it to the form a for some a N. We thus have to distinguish the elements which have a form by which we can directly see that they are the result of one of the rules, and call them canonical, from all other elements, which we will call noncanonical. But then, to be able to define when two noncanonical elements are equal, we must also prescribe how two equal canonical elements are formed. So: (1) a set A is defined by prescribing how a canonical element of A is formed as well as how two equal canonical elements of A are formed. This is the explanation of the meaning of a judgement of the form A is a set. For example, to the rules for N above, we must add 0 = 0 N and a = b N a = b N To take another example, A B is defined by the rule a A b B (a, b) A B which prescribes how canonical elements are formed, and the rule a = c A b = d B (a, b) = (c, d) A B by means of which equal canonical elements are formed. There is no limitation on the prescription defining a set, except that equality between canonical elements must always be defined in such a way as to be reflexive, symmetric and transitive. Now suppose we know A and B to be sets, that is, we know how canonical elements and equal canonical elements of A and B are formed. Then we stipulate: (2) two sets A and B are equal if and a A a B (that is, a A a B and a B a A ) 5 for arbitrary canonical elements a, b. a = b A a = b B This is the meaning of a judgement of the form A = B. When we explain what an element of a set A is, we must assume we know that A is a set, that is, in particular, how its canonical elements are formed. Then: (3) an element a of a set A is a method (or program) which, when executed, yields a canonical element of A as result. This is the meaning of a judgement of the form a A. Note that here we assume the notion of method as primitive. The rules of computation (execution) of the present language will be such that the computation of an element a of a set A terminates with a value b as soon as the outermost form of b tells that it is a canonical element of A (normal order or lazy evaluation). For instance, the computation of N gives the value (2 + 1), which is a canonical element of N since N. Finally: (4) two arbitrary elements a, b of a set A are equal if, when executed, a and b yield equal canonical elements of A as results. This is the meaning of a judgement of the form a = b A. This definition makes good sense since it is part of the definition of a set what it means for two canonical elements of the set to equal. Example. If e, f A B, then e and f are methods which yield canonical elements (a, b), (c, d) A B, respectively, as results, and e = f A B if (a, b) = (c, d) A B, which in turn holds if a = c A and b = d B. Propositions Classically, a proposition is nothing but a truth value, that is, an element of the set of truth values, whose two elements are the true and the false. Because of the difficulties of justifying the rules for forming propositions by means of quantification over infinite domains, when a proposition is understood as a truth value, this explanation is rejected by the intuitionists and replaced by saying that and that a proposition is defined by laying down what counts as a proof of the proposition, a proposition is true if it has a proof, that is, if a proof of it can be given 8. 8 D. Prawitz, Intuitionistic logic: a philosophical challenge, Logic and Philoshophy, Edited by G. H. von Wright, Martinus Nijhoff, The Hague, pp Thus, intuitionistically, truth is identified with provability, though of course not (because of Gödel s incompleteness theorem) with derivability within any particular formal system. The explanations of the meanings of the logical operations, which fit together with the intuitionistic conception of what a proposition is, are given by the standard table: a proof of the proposition consists of A & B a proof of A and a proof of B A B a proof of A or a proof of B A B a method which takes any proof of A into a proof of B ( x) B(x) a method which takes an arbitrary individual a into a proof of B(a) ( x) B(x) an individual a and a proof of B(a) the first line of which should be interpreted as saying that there is nothing that counts as a proof of. The above table can be made more explicit by saying: a proof of the proposition has the form A & B (a, b), where a is a proof of A and b is a proof of B A B i(a), where a is a proof of A, or j(b), where b is a proof of B A B (λx) b(x), where b(a) is a proof of B provided a is a proof of A ( x) B(x) (λx) b(x), where b(a) is a proof of B(a) provided a is an individual ( x) B(x) (a, b), where a is an individual and b is a proof of B(a) As it stands, this table is not strictly correct, since it shows proofs of canonical form only. An arbitrary proof, in analogy with an arbitrary element of a set, is a method of producing a proof of canonical form. If we take seriously the idea that a proposition is defined by laying down how its canonical proofs are formed (as in the second table above) and accept that a set is defined by prescribing how its canonical elements are formed, then it is clear that it would only lead to unnecessary duplication to keep the notions of proposition and set (and the associated notions of proof of a proposition and element of a set) apart. Instead, we simply identify them, that is, treat them as one and the same notion. This is the formulae-as-types (propositions-as-sets) interpretation on which intuitionistic type theory is based. 7 Rules of equality We now begin to build up a system of rules. First, we give the following rules of equality, which are easily explained using the fact that they hold, by definition, for canonical elements: Reflexivity Symmetry Transitivity a A a = a A a = b A b = a A A set A = A A = B B = A a = b A b = c A a = c A A = B B = C A = C For instance, a detailed explanation of transitivity is: a = b A means that a and b yield canonical elements d and e, resp
Related Search
We Need Your Support
Thank you for visiting our website and your interest in our free products and services. We are nonprofit website to share and download documents. To the running of this website, we need your help to support us.

Thanks to everyone for your continued support.

No, Thanks