-
Notifications
You must be signed in to change notification settings - Fork 6
Abstracts.2021.Meaning
by Peter Dybjer
At the LMPS conference in Hannover in 1979 Martin-Löf presented his seminal paper “Constructive Mathematics and Computer Programming”[1]. In this paper there is not only a new version of intuitionistic type theory but also so-called “meaning explanations” for this theory. These represent an important contribution to the foundations of intuitionistic logic and constructive mathematics. They clarify the Brouwer–Heyting–Kolmogorov interpretation and also generalize it and not only explain the meaning of the logical constants but also provide a conception of what a constructive mathematical object is in general. The meaning explanations can be viewed both metamathematically, as a certain kind of model construction in the tradition of Kleene realizability, and philosophically, as a “premathematical” discussion of the direct, intuitive semantics of type theory. In this talk I will discuss both aspects, and also present some Agda code towards the formalization of the meaning explanations.
- Abraham Wolk. Constructive Mathematics and Computer Programming. 2019.
- ^ Per Martin-Löf. Constructive Mathematics and Computer Programming. Logic, Methodology and Philosophy of Science VI (Hannover, 1979), pp. 153–175. Studies in Logic and the Foundations of Mathematics 104, 1982.
- Per Martin-Löf. Intuitionistic Type Theory. Studies in Proof Theory 1, 1984.
- Peter Dybjer. Program Testing and the Meaning Explanations of Intuitionistic Type Theory. Epistemology versus Ontology: Essays on the Philosophy and Foundations of Mathematics in Honour of Per Martin-Löf, pp. 215-241. Logic, Epistemology, and the Unity of Science 27, 2012.
- Peter Dybjer and Erik Palmgren. Intuitionistic Type Theory. The Stanford Encyclopedia of Philosophy 2020 (Summer Edition), 2020.