Intuitionistic type theory. Notes by Giovanni Sambin of a Series of Lectures given in Padua, June 1980.

*(English)*Zbl 0571.03030
Studies in Proof Theory, Lecture Notes, 1. Napoli: Bibliopolis. 91 p. (1984).

This booklet fills a gap left by the literature in the 20’s that put the finishing touches on set-theoretic foundations of the parts of mathematics called ”basic” in the 19th century; in particular, axioms for natural numbers, the definite article, principles of transfinite induction and the like. In the 20’s it was still thought (for example, by Hilbert worrying about boxers using their fists) that no corresponding intuitionistic foundation was possible. By the mid 30’s various metamathematical translations or interpretations had assured that possibility ”in principle”. Now this booklet, for good or ill, realizes it in practice; in fact, in a style of remarkably familiar flavour. This is of course a proper end in itself on the assumption that the notions used in set-theoretic foundations are invalid or in some other way defective. Without that assumption the booklet shows that there is not only no logical, but even no expository need for specifically classical principles in a foundation for the mainstream of 19th century mathematics. - Reviewer’s note. The author seems unmoved by the almost universal consensus - among (classical) mathematicians and philosophers - that (set-theoretic) foundational aspects of mathematical notions are of limited interest or even leur côté le moins intéressant; for reasons that apply with knobs on to the intuitionistic variety; cf. the contemporary use of ”basic” as in ”basic structure” (structure mère). The assumption above draws attention away, both in theory and practice, from the question: For which-variants-of those basic structures are intuitionistic aspects rewarding? Viewed this way the booklet is retrograde compared, for example, to topos theory, which attempts to respect the question above. More specifically, dubious doubts about elementary properties of sets draw attention away from genuine problems, for example, of iterating the power set operation, and from the broad philosophical literature under the heading: priority of what we know over how we know.

Reviewer: G.Kreisel

##### MSC:

03F50 | Metamathematics of constructive systems |

03F55 | Intuitionistic mathematics |

03-02 | Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations |