Resumo: O propósito desta tese é desenvolver uma Teoria de Modelos paraconsistente a partir das bases lançadas por Walter Carnielli, Marcelo Esteban Coniglio, Rodrigo Podiack e Tarcísio Rodrigues no artigo "On the Way to a Wider Model Theory: Completeness Theorems for First-Order Logics of Formal Inconsistency" de 2014. A busca por uma compreensão mais profunda do fenômeno da paraconsistência de um ponto de vista epistemológico leva a um sistema de raciocínio baseado nas "Lógicas de Inconsistência Formal'' (LFI's). Os modelos são tratados como estados de conhecimento e o conceito de isomorfismo é reformulado de modo a gerar outro que preserva uma por\c{c}\~{a}o da totalidade do conhecimento de cada estado. Com base nisso, \'{e} criada uma no\c{c}\~{a}o de refinamento que pode acontecer de dentro ou de fora do estado. Na sequência, mostra-se que dois importantes resultados clássicos, a saber o Teorema da Omissão de Tipos e o Teorema da Interpolação de Craig, valem no novo sistema e se mostra ainda que, caso se queira que os resultados clássicos em geral valham em um sistema paraconsistente, é necessário que tal sistema seja essencialmente como o que foi desenvolvido aqui. Finalmente, é feito um ensaio sobre como deveria ser um PROLOG paraconsistente à luz das ideias que foram desenvolvidas até então Ver menos

Abstract: The purpose of this thesis is to develop a paraconsistent Model Theory from the basis launched by Walter Carnielli, Marcelo Esteban Coniglio, Rodrigo Podiack and Tarc\'{i}sio Rodrigues in the article 'On the Way to a Wider Model Theory: Completeness Theorems for First-Order Logics of Formal Inconsistency' of 2014. The pursuit of a deeper understanding of the phenomenon of paraconsistency from an epistemological point of view leads to a reasoning system based on the Logics of Formal Inconsistency. Models are regarded as states of knowledge and the concept of isomorphism is reformulated so as to give raise to a new concept that preserves a portion of the whole knowledge of each state. Based on this, a notion of refinement is created which may occur from inside or from outside the state. In the sequel, two important classical results, namely the Omitting Types Theorem and Craig's Interpolation Theorem are shown to hold in the new system and it is also shown that, if classical results in general are to hold in a paraconsistent system, then such a system should be in essence how it was developed here. Finally, an essay of what a paraconsistent PROLOG should be is made in the light of the ideas developed so far Ver menos