Dependent Connectives in Constructive Type Theory
Fuente:
Zenodo
Enregistré dans:
| Auteur principal: | |
|---|---|
| Format: | Recurso digital |
| Publié: |
Zenodo
2025
|
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866901209419350016 |
|---|---|
| author | SÉRGIO DE ANDRADE, PAULO |
| author_facet | SÉRGIO DE ANDRADE, PAULO |
| contents | Constructive Type Theory (CTT), notably Martin-Löf Type Theory, provides a foundational framework for constructive mathematics, embodying the propositions-as-types and proofs-as-programs paradigm. Central to its expressivity are dependent types, specifically dependent product (Pi-types) and dependent sum (Sigma-types), which allow types to depend on terms, thereby capturing quantification and existential statements constructively. While these dependent types naturally extend the notions of universal and existential quantification, the explicit treatment of traditional logical connectives (conjunction, disjunction, implication) in a genuinely dependent setting often remains implicit or is handled by standard type formers. This paper explores the concept of "dependent connectives," investigating how these fundamental logical operations can be generalized to explicitly account for and leverage term-dependent information. We formally define dependent variants of conjunction, disjunction, and implication within the framework of Martin-Löf Type Theory, examining their formation rules, introduction, and elimination principles, and their computational behavior. We demonstrate how these explicit dependent connectives provide a more granular and expressive mechanism for formalizing complex mathematical arguments and constructing verified programs, especially in scenarios where the structure of a proposition or the nature of its proof components inherently varies based on prior computational results. The study highlights their role in enriching the proofs-as-programs correspondence and expanding the frontiers of formal mathematics and program verification. |
| format | Recurso digital |
| id | zenodo_https___doi_org_10_5281_zenodo_17689774 |
| institution | Zenodo |
| language | |
| publishDate | 2025 |
| publisher | Zenodo |
| record_format | zenodo |
| spellingShingle | Dependent Connectives in Constructive Type Theory SÉRGIO DE ANDRADE, PAULO Constructive Type Theory (CTT), notably Martin-Löf Type Theory, provides a foundational framework for constructive mathematics, embodying the propositions-as-types and proofs-as-programs paradigm. Central to its expressivity are dependent types, specifically dependent product (Pi-types) and dependent sum (Sigma-types), which allow types to depend on terms, thereby capturing quantification and existential statements constructively. While these dependent types naturally extend the notions of universal and existential quantification, the explicit treatment of traditional logical connectives (conjunction, disjunction, implication) in a genuinely dependent setting often remains implicit or is handled by standard type formers. This paper explores the concept of "dependent connectives," investigating how these fundamental logical operations can be generalized to explicitly account for and leverage term-dependent information. We formally define dependent variants of conjunction, disjunction, and implication within the framework of Martin-Löf Type Theory, examining their formation rules, introduction, and elimination principles, and their computational behavior. We demonstrate how these explicit dependent connectives provide a more granular and expressive mechanism for formalizing complex mathematical arguments and constructing verified programs, especially in scenarios where the structure of a proposition or the nature of its proof components inherently varies based on prior computational results. The study highlights their role in enriching the proofs-as-programs correspondence and expanding the frontiers of formal mathematics and program verification. |
| title | Dependent Connectives in Constructive Type Theory |
| url | https://doi.org/10.5281/zenodo.17689774 |