Uma abordagem sobre a concepção de proposição da teoria institucionalista de tipos
Saved in:
| Main Author: | |
|---|---|
| Publication Date: | 2013 |
| Format: | Master thesis |
| Language: | por |
| Source: | Repositório Institucional da UFG |
| Download full: | http://repositorio.bc.ufg.br/tede/handle/tede/3337 |
Summary: | By means of the Curry-Howard Correspondence Martin-Löf’s intuitionistic type theory claims that to define a proposition by laying down how its canonical proofs are formed is the same as to define a set by laying down how its canonical elements are formed; consequently a proposition can be seen as the set of its proofs. On the other hand, we find in this very same theory a distinction between the notions of set and of type, such that the difference of the latter in relation to the former consists in the fact that to form a type we do not need to present an exhaustive prescription for the formation of its objects; it is sufficient to just have a general notion of what would be an arbitrary object that inhabits such type. Thus we argue that we can extract two distinct notions of propositon from the intuitionistic type theory, one which treats propositions as types and another which treats propositions as sets. Such distinction will have some bearing on discussions concerning hypothetical demonstrations and conjecture’s formation. |