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!
|
| Summary: | 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.
|
|---|---|
| ISSN: | 1112-4393 2588-2031 |