scientific article; zbMATH DE number 1302065
Beginning in 1970, Per Martin-Löf has developed an intuitionistic type theory (henceforth type theory for short) as a constructive alternative to the usual foundation of mathematics based on classical set theory. We assume the reader is aware at least of the main peculiarities of type theory, as formulated by \textit{P. Martin-Löf} [Intuitionistic type theory (Bibliopolis, Napoli) (1984; Zbl 0571.03030)] and \textit{B. Nordström}, \textit{K. Petersson} and \textit{J. M. Smith} [Programming in Martin-Löf's type theory. An introduction (Oxford Univ. Press, Oxford) (1990; Zbl 0744.03029)]; here we recall some of them to be able to introduce our point of view. The form of type theory is that of a logical calculus, where inference rules to derive judgements are at the same time set-theoretic constructions, because of the ``propositions-as-sets interpretation. The spirit of type theory -- expressing our interpretation in a single sentence -- is to adopt those notions and rules which keep total control of the amount of information contained in the different forms of judgement. However, our experience in developing pieces of actual mathematics within type theory has led us to believe that ``orthodox type theory is not suitable because its control of information is too strict for this purpose. In fact, the fully analytic character of type theory becomes a burden when dealing with the synthetic methods of mathematics, which ``forget or take for granted most of the details. This, in our opinion, could be the reason why type theory has generated, up to now, more interest among logicians and computer scientists as a formal system than among mathematicians as a foundational theory. We claim that there is no intrinsic reason why it should remain so, and that actually it is only a matter of developing a stock of ``utilities: that is, of building up a toolbox which covers the territory between the basic formalism and mathematical practice; after all, this happened for classical set theory ZF long ago. In other words, the situation seems analogous to that of a programmer who, maybe because of a particular skill with the machine language, has not yet developed those higher level constructs and languages which allow him or her to save time and mental energy, and thus in the end are necessary to free the mind for a common human (i.e. abstract) comprehension. So our general aim is to build up those tools, that is definitions and rules, which ``forget some information, and thus allow a higher level of abstraction, which can make type theory more handy and suitable to work out (intuitionistic) mathematics based on mathematical intuition, as it has been and should be. For the entire collection see [Zbl 0899.00026].
- A minimalist two-level foundation for constructive mathematics
- Constructive domain theory as a branch of intuitionistic pointfree topology
- Inductively generated formal topologies.
- Constructive metrisability in point-free topology.
- Some points in formal topology.
- The problem of the formalization of constructive topology
- A cartesian closed category in Martin-Löf's intuitionistic type theory
- Pretopologies and a uniform presentation of sup-lattices, quantales and frames
- Programming interfaces and basic topology
- Formal Zariski topology: Positivity and points
- A minimalist foundation at work
- On choice rules in dependent type theory
- Finiteness in a Minimalist Foundation
- In the Search of a Naive Type Theory
- scientific article; zbMATH DE number 3910392 (Why is no real title available?)
- Quotient completion for the foundation of constructive mathematics
- scientific article; zbMATH DE number 517090 (Why is no real title available?)
- Subsets, quotients and partial functions in Martin-Löf's type theory
- Are subsets necessary in Martin-Löf type theory?
- A SYNTACTIC CHARACTERIZATION OF MORITA EQUIVALENCE
- Can You Add Power‐Sets to Martin‐Lof's Intuitionistic Set Theory?
- scientific article; zbMATH DE number 3999882 (Why is no real title available?)
- Real and ideal in constructive mathematics
- Realist consequence, epistemic inference, computational correctness
- A Comparison of Type Theory with Set Theory
- Equiconsistency of the minimalist foundation with its classical version
- Objects: a study in Kantian formal epistemology
- On different ways of being equal
- Finitary formal topologies and Stone's representation theorem
- The Zariski spectrum as a formal geometry
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4247310)
