AL-Lisaniyyat
Volume 28, Numéro 1, Pages 409-414
2022-06-16
Constructive Type Theory
Authors : Mechouet Terkia . Zidani Farid .
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. Hetried to overcome the deficiencies of the various theories constructed to solve a problematic of set theory which is: Does the class of all classes member to itself or not? among them Russell’s Type Theory, which is founded on the concept of type, despite its imperfections and criticisms, directed at it, 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.
Keywords
Element-Type- Judgment-Constructive-Semantic-Canonical.
Les articles similaires
الفيحاني مريم
.
ص 554-580.
صافي زُهرة
.
رزايقية محمود
.
ص 764-782.
Benadda Abdelouahid
.
pages 249-257.
Akindele Akinade Frederick
.
Lawal-solarin Opeola Esther
.
pages 1-14.
