La Théorie Constructive des Types (TCT)
##plugins.themes.bootstrap3.article.sidebar##
##plugins.themes.bootstrap3.article.main##
Résumé
Le but de notre article est de présenter la Théorie Constructive des Types
(TCT) de Per Martin Löf et les concepts qui y sont en relation avec. Fondée dans
le but de construire un système logique formelle et une assise philosophique des
mathématiques constructive. Löf a essayé de surpasser toutes les imperfections
des théories logiques qui ont déjà essayé de résoudre le paradoxe de la théorie
des ensembles: l’ensemble de tous les ensembles appartient-il à lui-même ou
pas? Problème traité par plusieurs mathématiciens et logiciens, parmi eux
Bertrand Russell dans sa théorie des Types, qui, et malgré ses lacunes et les
divers critiques à son encontre, a ouvert le champ pour l’élaboration d’autres
théorie telle que le Lambda Calcul en 1930 de Alonzo Church, fondée elle aussi
sur le concept de type, mais se distinguant par l’utilisation du concept de fonction
à la place de l’ensemble. Ces deux théories ont été à l’origine de la TCT et ses
concepts basiques comme: type, proposition, jugement, preuve-canonique-noncanonique…etc.
##plugins.themes.bootstrap3.article.details##
Références
- 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.