UM SISTEMA DE GENTZEN PARA CÁLCULOS COM IDENTIDADE PARCIAL E UNIVERSOS ABERTOS

Os Sistemas Q1 e Q2 desenvolvidos por Andréa Loparic, perfazem três pincipais modificações na semântica clássica: primeiramente, o universo do discurso pode não estar limitado aos objetos que pertencem ao domínio de uma data estrutura; em segundo lugar, a relação de identidade é determinada como a diagonal desse domínio (assim, tal relação pode não ser aplicável a todas as coisas sobre as quais a linguagem possa falar); em terceiro lugar, o quantificador existencial, em Q1, bem como o universal, em Q2, podem alcançar valores que estejam fora do domínio da estrutura. Como consequência, embora definida classicamente, a negação apresenta alguns comportamentos não clássicos - a negação de um predicado numa fórmula atômica, por exemplo, pode caracterizar algo maior que, e não tão bem definido quanto, o complemento da extensão desse predicado relativamente ao domínio..Posteriormente, o sistema Q1 foi estendido por Fernando Paulo Christe Adorno para incluir nomes e símbolos funcionais em sua linguagem. Adorno apresentou também: uma nova extensão desse sistema estendido, chamada Q1p, que inclui parâmetros entre seus símbolos individuais e é uma extensão conservativa de Q1p. Dois outros resultados foram demonstrados: 1) para toa fórmula a da linguagem de Q1, a é válida em Q1 se e somente se a é um teorema de S; e 2) para toda formula a em Q2 há uma fórmula a* em Q1 tal que a é Q2 válida se a* é Q1 válida..Em nosso trabalho, apresentamos um estudo detalhado dos sistemas Q1 e Q2, na primeira parte; na segunda parte, um novo sistema de Gentzen, chamado QG1, que trabalha como sequentes, e resulta de algumas modificações no sistema LK, de Gentzen. Por fim, na terceira parte, provamos que o sistema QG1 é equivalente ao sistema S.