-д хадгалсан:
| Үндсэн зохиолч: | |
|---|---|
| Формат: | Recurso digital |
| Хэл сонгох: | |
| Хэвлэсэн: |
Zenodo
2025
|
| Онлайн хандалт: | https://doi.org/10.5281/zenodo.17689774 |
| Шошгууд: |
Шошго нэмэх
Шошго байхгүй, Энэхүү баримтыг шошголох эхний хүн болох!
|
Агуулга:
- 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.