Submitted by Erika Demachki (erikademachki@gmail.com) on 2014-10-13T19:12:35Z
No. of bitstreams: 2
Dissertação - Bruno Rigonato Mundim - 2013.pdf: 1303876 bytes, checksum: 4f1bada6e1186d920d0d0bfcd28d47f1 (MD5)
license_rdf: 23148 bytes, checksum: 9da0b6dfac957114c6a7714714b86306 (MD5) / Approved for entry into archive by Jaqueline Silva (jtas29@gmail.com) on 2014-10-13T20:49:48Z (GMT) No. of bitstreams: 2
Dissertação - Bruno Rigonato Mundim - 2013.pdf: 1303876 bytes, checksum: 4f1bada6e1186d920d0d0bfcd28d47f1 (MD5)
license_rdf: 23148 bytes, checksum: 9da0b6dfac957114c6a7714714b86306 (MD5) / Made available in DSpace on 2014-10-13T20:49:48Z (GMT). No. of bitstreams: 2
Dissertação - Bruno Rigonato Mundim - 2013.pdf: 1303876 bytes, checksum: 4f1bada6e1186d920d0d0bfcd28d47f1 (MD5)
license_rdf: 23148 bytes, checksum: 9da0b6dfac957114c6a7714714b86306 (MD5)
Previous issue date: 2013-09-02 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior - CAPES / 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. / A teoria intuicionista de tipos, de Martin-Löf, alega, à luz da correspondência Curry-
Howard, que definir uma proposição por meio do estabelecimento de como as suas provas
canônicas são formadas é o mesmo que definir um conjunto por meio do estabelecimento de
como os seus elementos canônicos são formados, fazendo com que uma proposição possa ser
vista como o conjunto de suas provas. Por outro lado, encontramos nessa mesma teoria uma
distinção entre as noções de conjunto e tipo, sendo que a diferença deste em relação àquele consiste
no fato de que para se formar um tipo não é preciso apresentar uma prescrição exaustiva da
formação de seus objetos, basta se ter uma noção geral do que seria um objeto arbitrário que o
habita. Tendo isso em conta, argumentamos que podemos extrair da teoria intuicionista de tipos
duas concepções de proposição distintas, uma que considera proposições como tipos e outra
que considera proposições como conjuntos. Tal distinção implicará em algumas considerações
envolvendo questões sobre demonstrações hipotéticas e a formação de conjecturas.
| Identifer | oai:union.ndltd.org:IBICT/oai:repositorio.bc.ufg.br:tede/3337 |
| Date | 02 September 2013 |
| Creators | Mundim, Bruno Rigonato |
| Contributors | Porto, André da Silva, Porto, André da Silva, Velloso, Araceli Rosich Soares, Pereira, Luiz Carlos Pinheiro Dias |
| Publisher | Universidade Federal de Goiás, Programa de Pós-graduação em Filosofia (FAFIL), UFG, Brasil, Faculdade de Filosofia - FAFIL (RG) |
| Source Sets | IBICT Brazilian ETDs |
| Language | Portuguese |
| Detected Language | Portuguese |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis |
| Format | application/pdf |
| Source | reponame:Biblioteca Digital de Teses e Dissertações da UFG, instname:Universidade Federal de Goiás, instacron:UFG |
| Rights | http://creativecommons.org/licenses/by-nc-nd/4.0/, info:eu-repo/semantics/openAccess |
| Relation | -7401176116358064379, 600, 600, 600, 600, 5585255767972561168, 7975219356843496474, 2075167498588264571 |
Page generated in 0.0027 seconds