Uma abordagem sobre a concepção de proposição da teoria institucionalista de tipos
Carregando...
Data
2013-09-02
Autores
Título da Revista
ISSN da Revista
Título de Volume
Editor
Universidade Federal de Goiás
Resumo
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.
Descrição
Citação
MUNDIM, Bruno Rigonato. Uma abordagem sobre a concepção de proposição da teoria institucionalista de tipos. 2013. 118 f. Dissertação (Mestrado em Filosofia) - Universidade Federal de Goiás, Goiânia, 2013.