relações de consequência bidimensionais, sistemas de demonstração ao estilo de Hilbert, semânticas não-determinísticas, busca de demonstrações
O presente trabalho propõe um formalismo dedutivo bidimensional à la Hilbert (H-formalismo) para relações de B-consequência, uma classe de lógicas bidimensionais que generalizam as noções usuais (Tarskianas, unidimensionais) de lógica. Nós argumentamos que o ambiente bidimensional é apropriado para o estudo do bilateralismo em lógica, por permitir que julgamentos primitivos de asserção e denegação (ou, como preferimos, as atitudes cognitivas de aceitação e rejeição) ajam em dimensões independentes e capazes de interagir entre si ao determinar as inferências válidas de uma lógica. Nessa perspectiva, o formalismo proposto constitui um aparato inferencial para raciocinar sobre julgamentos bilateralistas. Após uma descrição detalhada do funcionamento do H-formalismo proposto, o qual é inspirado nos sistemas de Hilbert simétricos unidimensionais, nós provemos um algoritmo de busca de demonstrações que executa em tempo exponencial, em geral, e em tempo polinomial quando apenas regras contendo no máximo uma fórmula no sucedente estão presentes no sistema em questão. Então, nós passamos a investigar semânticas não-determinísticas bidimensionais por meio de estruturas de matrizes contendo dois conjuntos de valores distinguidos, um qualificando alguns valores de verdade como aceitos, e o outro, alguns valores como rejeitados, constituindo um caminho semântico para o bilateralismo no ambiente bidimensional. Nós apresentamos também um algoritmo para a produção de sistemas de Hilbert bidimensionais analíticos para matrizes não-determinísticas bidimensionais suficientemente expressivas, bem como alguns procedimentos de simplificação que permitem reduzir consideravelmente o tamanho e a complexidade dos sistemas resultantes. Para matrizes finitas, vale apontar, o procedimento resulta em sistemas finitos. Neste documento, nós registramos os resultados obtidos até o momento e indicamos um plano de trabalho para o restante das investigações cujos resultados serão documentados na versão final desta dissertação.