Constructive Type Theory
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 v...
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | Arabic |
| Published: |
Scientific and Technological Research Center for the Development of the Arabic Language
2022-06-01
|
| Series: | Al-Lisaniyyat |
| Subjects: | |
| Online Access: | https://www.crstdla.dz/ojs/index.php/allj/article/view/58 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1849424601558286336 |
|---|---|
| author | Terkia Mechouet Farid Zidani |
| author_facet | Terkia Mechouet Farid Zidani |
| author_sort | Terkia Mechouet |
| collection | DOAJ |
| description |
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.
|
| format | Article |
| id | doaj-art-5c4bf3a5fa294110b2d0cc2dd4d9e56a |
| institution | Kabale University |
| issn | 1112-4393 2588-2031 |
| language | Arabic |
| publishDate | 2022-06-01 |
| publisher | Scientific and Technological Research Center for the Development of the Arabic Language |
| record_format | Article |
| series | Al-Lisaniyyat |
| spelling | doaj-art-5c4bf3a5fa294110b2d0cc2dd4d9e56a2025-08-20T03:30:05ZaraScientific and Technological Research Center for the Development of the Arabic LanguageAl-Lisaniyyat1112-43932588-20312022-06-0128110.61850/allj.v28i1.58Constructive Type TheoryTerkia Mechouet0Farid Zidani1university of Algiers 2 abu el kacem saadallah university of Algiers 2 abu el kacem saadallah 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. https://www.crstdla.dz/ojs/index.php/allj/article/view/58Element - Type - Judgment - Constructive - Semantic - Canonical. |
| spellingShingle | Terkia Mechouet Farid Zidani Constructive Type Theory Al-Lisaniyyat Element - Type - Judgment - Constructive - Semantic - Canonical. |
| title | Constructive Type Theory |
| title_full | Constructive Type Theory |
| title_fullStr | Constructive Type Theory |
| title_full_unstemmed | Constructive Type Theory |
| title_short | Constructive Type Theory |
| title_sort | constructive type theory |
| topic | Element - Type - Judgment - Constructive - Semantic - Canonical. |
| url | https://www.crstdla.dz/ojs/index.php/allj/article/view/58 |
| work_keys_str_mv | AT terkiamechouet constructivetypetheory AT faridzidani constructivetypetheory |