Constructive Type Theory
Article Sidebar
Main Article Content
Abstract
The aim of our paper is to present the Constructive Type Theory (CTT) and some related concepts for the Swedish logician
Per Martin Löf, who constructed a formal logic system in order
to establish a philosophical foundation of constructive mathematics. He tried to overcome the deficiencies of the various theories
constructed to solve a problematic of set theory which is: Does
the class of all classes is a member to itself or not? among them
Russell’s Type Theory, which is founded on the concept of
type, despite its imperfections and criticisms, opened the way
to others theories like the Alonzo Church’s one which is based
on function not on set, and built what we call Lambda Calculus in
1930. These theories were the origin of Constructive Type theory
and its basic concepts: type, proposition, judgment, proof…etc.
Article Details
References
- Church, A. (1941). The Calculi of Lambda Conversion. Annals of Mathematics studies,(6), London:.Princeton University Press.
Davant, J. B. (1975). Wittgenstein on Russell’s theory of types. Notre Dame J. Formal Log., 16(1), 102-108.
- Howard, W. A. (1986). Per Martin-Löf. Intuitionistic type theory. (Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980). Studies in proof theory. Bibliopolis, Naples1984, ix+ 91 pp. The Journal of Symbolic Logic, 51(4), 1075-1076
Martin-Löf, P. (1996). On the meanings of the logical constants and the justifications of the logical laws. Nordic journal of philosophical logic, 1(1), 11-60.
- Per Martin Löf, (1982). Constructive Mathematics and Computer Programming, in Logic, Methodology and Philosophy of Science. Department of Mathematics. Stockholm: University of Stockholm.
- Rahman, S., McConaughey, Z., Klev, A., & Clerbout, N. (2018). Immanent reasoning or equality in action: A plaidoyer for the play level. Springer (18).
- Russell, B. (1903). Appendix B: The doctrine of types. Principles of mathematics. The Taylor and Francis e-Library
- Vernant, D. (2001). Introduction à la logique standard. Filosoficky Casopis, 50
- Whitehead, A. N., & Russell, B.. (1976), Principia Mathematica .Cambridge at the University.