[pt] O QUE É O ESQUELETO DE UMA DEMONSTRAÇÃO
[en] WHAT IS SKELETON OF A PROOF
| dc.contributor | NICOLAU CORCAO SALDANHA | |
| dc.creator | EDUARDO NAHUM OCHS | |
| dc.date | 2004-03-12 | |
| dc.date.accessioned | 2022-09-21T21:42:19Z | |
| dc.date.available | 2022-09-21T21:42:19Z | |
| dc.identifier | https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=4645@1 | |
| dc.identifier | https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=4645@2 | |
| dc.identifier | http://doi.org/10.17771/PUCRio.acad.4645 | |
| dc.identifier.uri | https://hdl.handle.net/20.500.12032/42557 | |
| dc.description | [pt] Considere os seguintes dois tipos de transformções em demonstrações: 1) tornar uma prova mais incompleta, apagando um lema ou uma construção que sejam parte da prova e pondo no lugar um aviso dizendo isso é óbvio; 2) pegar um passo que foi provado por um isso é óbvio, aplicar algum algoritmo que encontre uma demonstração para esse passo, e trocar o aviso pela demonstração de verdade. Nós vamos considerar que a primeira operação vai em direção ao esqueleto da demonstração, e que ela é como uma projeção; a segunda operação é um levantamento de um esqueleto para uma demonstração um pouco mais completa com aquele esqueleto. Nós só estamos interessados em esqueletos que possam ser levantados até provas completas usando algum algoritmo conhecido. Nesta tese descrevemos uma linguagem - o sistema DNC - que permite provar vários fatos sobre categorias usando esqueletos. O método para o levantamento é, a grosso modo, o seguinte: a partir do nome de um termo em DNC nós podemos obter o seu tipo; por uma espécie de Isomorfismo de Curry-Howard um tipo desses pode ser visto como uma preposição numa certa lógica; um algoritmo que obtenha uma demonstração para essa proposição retorna uma árvore de demonstração (uma derivação) num certo sistema de Dedução Natural, e essa árvore pode ser lida como um lambda- termo do tipo dado - ela dá uma construção natural para um objeto daquele tipo, e esse objeto muito frequentemente é exatamente o objeto que esperávamos obter. Derivações em DNC podem ser traduzidas para derivações num Pure Type System com Dicionários (PTSD), e derivações em PTSDs podem ser traduzidas para derivações em Pure Type Systems (PTSs); daí, questões sobre a teoria da prova de DNC se tornam questões sobre a teoria da prova de PTSs, que é bastante bem-conhecida. Não só temos um levantamento de nomes de termos em DNC para provas completas, mas também temos um modo formal de levantar diagramas categóricos expressos na linguagem do DNC para termos em DNC e daí para provas completas; e se mudamos o dicionário embutido num PTSD podemos fazer com que o mesmo esqueleto em DNC represente provas em contextos diferentes; por exemplo, algumas provas que aparentemente estão sendo feitas sobre a categoria dos conjuntos podem ser reinterpretados como provas sobre um topos arbitrário. Usamos essa idéia para apresentar de uma forma simples - em que os passos óbvios omitidos são óbvios num sentido muito preciso - a semântica categárica para alguns PTSs, incluindo PTSs com polimorfismo e tipos dependentes, e os PTSs para quais as derivações em DNC são traduzidas. | |
| dc.description | [en] Consider the following two kinds of transformation on proofs; the first is to make a a proof more incomplete, by erasing a lemma or a construction from it and replacing it by a tag saying this is obvious; the second kind of transformation takes a step that is proved by a this is obvious tag, applies some kind of prof-search algorithm to it, and replaces the tag by a real proof for that step. We will consider that the first operation goes toward the skeleton towards a more complete proof that had that skeleton as a projection. We are only interested in skeletons can be lifted back to full proofs using some known algorithm. In this thesis we can describe a language - DNC - that lets us prove several categorical facts using skeletons. The method for lifting these skeletons goes like this: from the name of a DNC term we can obtain its type; by a kind of Curry-Howard isomorphism a such type can be seen as a proposition in a certain logic; proof-search for that proposition will obtain a proof-tree for it in a certain system of Natural Deduction, and that proof-tree can be read as a lambda-term of given type - the proof-tree gives a natural construction for an object of the given type, that very often is exactly the object that we were looking for. Derivations in DNC can be translated into derivations in a Pure Type System with Dictionaries (PTSD), and derivations in PTSDs can be translated into derivations in Pure Type Systems (PTSs); so questions about the proof- theory of DNC become questions about the proof-theory of PTSs, whose properties are quite well-known. Also, not only we can lift names of terms in DNC to full proofs in different settings; for example, some proofs that apparently are happening over the category of sets can be reinterpreted as proofs over an arbitrary topos. We use that idea to give a simple presentation (in which the omitted obvious steps are obvious in a very precise sense) of the categorical semantics for some PTSs - and that includes PTSs into which the DNC derivations are translated. | |
| dc.language | pt | |
| dc.publisher | MAXWELL | |
| dc.subject | [pt] TEORIA DE CATEGORIAS | |
| dc.subject | [pt] SEMANTICA | |
| dc.subject | [pt] LOGICA | |
| dc.subject | [en] CATEGORY THEORY | |
| dc.subject | [en] SEMANTICS | |
| dc.subject | [en] LOGIC | |
| dc.title | [pt] O QUE É O ESQUELETO DE UMA DEMONSTRAÇÃO | |
| dc.title | [en] WHAT IS SKELETON OF A PROOF | |
| dc.type | TEXTO |
Files in this item
| Files | Size | Format | View |
|---|---|---|---|
|
There are no files associated with this item. |
|||