Constructive type theory (CTT)‎

Abstract EN

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.

Abstract FRE

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- non-canonique…etc.