Hilbert-style formalism for two-dimensional notions of consequence

The present work proposes a two-dimensional Hilbert-style deductive formalism (H-formalism) for B-consequence relations, a class of two-dimensional logics that generalize the usual (Tarskian, one-dimensional) notions of logic. We argue that the two-dimensional environment is appropriate to the study...

ver descrição completa

Na minha lista:
Detalhes bibliográficos
Autor principal: Greati, Vitor Rodrigues
Outros Autores: Almeida, João Marcos de
Formato: Dissertação
Idioma:pt_BR
Publicado em: Universidade Federal do Rio Grande do Norte
Assuntos:
mCi
Endereço do item:https://repositorio.ufrn.br/handle/123456789/46792
Tags: Adicionar Tag
Sem tags, seja o primeiro a adicionar uma tag!
id ri-123456789-46792
record_format dspace
institution Repositório Institucional
collection RI - UFRN
language pt_BR
topic Two-dimensional consequence relations
Hilbert-style proof systems
Non-deterministic semantics
mCi
spellingShingle Two-dimensional consequence relations
Hilbert-style proof systems
Non-deterministic semantics
mCi
Greati, Vitor Rodrigues
Hilbert-style formalism for two-dimensional notions of consequence
description The present work proposes a two-dimensional Hilbert-style deductive formalism (H-formalism) for B-consequence relations, a class of two-dimensional logics that generalize the usual (Tarskian, one-dimensional) notions of logic. We argue that the two-dimensional environment is appropriate to the study of bilateralism in logic, by allowing the primitive judgments of assertion and denial (or, as we prefer, the cognitive attitudes of acceptance and rejection) to act on independent but interacting dimensions in determining what-follows-from-what. In this perspective, our proposed formalism constitutes an inferential apparatus for reasoning over bilateralist judgments. After a thorough description of the inner workings of the proposed proof formalism, which is inspired by the one-dimensional symmetrical Hilbert-style systems, we provide a proof-search algorithm for finite analytic systems that runs in at most exponential time, in general, and in polynomial time when only rules having at most one formula in the succedent are present in the concerned system. We delve then into the area of two-dimensional non-deterministic semantics via matrix structures containing two sets of distinguished truthvalues, one qualifying some truth-values as accepted and the other as rejected, constituting a semantical path for bilateralism in the two-dimensional environment. We present an algorithm for producing analytic two-dimensional Hilbert-style systems for sufficiently expressive two-dimensional matrices, as well as some streamlining procedures that allow to considerably reduce the size and complexity of the resulting calculi. For finite matrices, we should point out that the procedure results in finite systems. In the end, as a case study, we investigate the logic of formal inconsistency called mCi with respect to its axiomatizability in terms of Hilbert-style systems. We prove that there is no finite one-dimensional Hilbert-style axiomatization for this logic, but that it inhabits a two-dimensional consequence relation that is finitely axiomatizable by a finite two-dimensional Hilbert-style system. The existence of such system follows directly from the proposed axiomatization procedure, in view of the sufficiently expressive 5-valued non-deterministic bidimensional semantics available for the mentioned two-dimensional consequence relation.
author2 Almeida, João Marcos de
author_facet Almeida, João Marcos de
Greati, Vitor Rodrigues
format masterThesis
author Greati, Vitor Rodrigues
author_sort Greati, Vitor Rodrigues
title Hilbert-style formalism for two-dimensional notions of consequence
title_short Hilbert-style formalism for two-dimensional notions of consequence
title_full Hilbert-style formalism for two-dimensional notions of consequence
title_fullStr Hilbert-style formalism for two-dimensional notions of consequence
title_full_unstemmed Hilbert-style formalism for two-dimensional notions of consequence
title_sort hilbert-style formalism for two-dimensional notions of consequence
publisher Universidade Federal do Rio Grande do Norte
publishDate 2022
url https://repositorio.ufrn.br/handle/123456789/46792
work_keys_str_mv AT greativitorrodrigues hilbertstyleformalismfortwodimensionalnotionsofconsequence
_version_ 1773958002903089152
spelling ri-123456789-467922022-05-02T16:02:13Z Hilbert-style formalism for two-dimensional notions of consequence Hilbert-style formalism for two-dimensional notions of consequence Greati, Vitor Rodrigues Almeida, João Marcos de http://lattes.cnpq.br/0343448850800210 http://lattes.cnpq.br/3059324458238110 Marcelino, Sérgio Roseiro Teles 00000000000 Rivieccio, Umberto http://lattes.cnpq.br/0597230560325577 Two-dimensional consequence relations Hilbert-style proof systems Non-deterministic semantics mCi The present work proposes a two-dimensional Hilbert-style deductive formalism (H-formalism) for B-consequence relations, a class of two-dimensional logics that generalize the usual (Tarskian, one-dimensional) notions of logic. We argue that the two-dimensional environment is appropriate to the study of bilateralism in logic, by allowing the primitive judgments of assertion and denial (or, as we prefer, the cognitive attitudes of acceptance and rejection) to act on independent but interacting dimensions in determining what-follows-from-what. In this perspective, our proposed formalism constitutes an inferential apparatus for reasoning over bilateralist judgments. After a thorough description of the inner workings of the proposed proof formalism, which is inspired by the one-dimensional symmetrical Hilbert-style systems, we provide a proof-search algorithm for finite analytic systems that runs in at most exponential time, in general, and in polynomial time when only rules having at most one formula in the succedent are present in the concerned system. We delve then into the area of two-dimensional non-deterministic semantics via matrix structures containing two sets of distinguished truthvalues, one qualifying some truth-values as accepted and the other as rejected, constituting a semantical path for bilateralism in the two-dimensional environment. We present an algorithm for producing analytic two-dimensional Hilbert-style systems for sufficiently expressive two-dimensional matrices, as well as some streamlining procedures that allow to considerably reduce the size and complexity of the resulting calculi. For finite matrices, we should point out that the procedure results in finite systems. In the end, as a case study, we investigate the logic of formal inconsistency called mCi with respect to its axiomatizability in terms of Hilbert-style systems. We prove that there is no finite one-dimensional Hilbert-style axiomatization for this logic, but that it inhabits a two-dimensional consequence relation that is finitely axiomatizable by a finite two-dimensional Hilbert-style system. The existence of such system follows directly from the proposed axiomatization procedure, in view of the sufficiently expressive 5-valued non-deterministic bidimensional semantics available for the mentioned two-dimensional consequence relation. Coordenação de Aperfeiçoamento de Pessoal de Nível Superior - CAPES O presente trabalho propõe um formalismo dedutivo bidimensional à 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 sustentamos que o ambiente bidimensional é apropriado para o estudo do bilateralismo em lógica, por permitir que julgamentos primitivos de asserção e rechaç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 formalismo proposto, o qual é inspirado nos sistemas de Hilbert simétricos, 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 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 do sistema resultante. Para matrizes finitas, vale apontar, o procedimento resulta em sistemas finitos. Ao final, como estudo de caso, investigamos a lógica da inconsistência formal chamada mCi quanto à sua axiomatizabilidade por sistemas ao estilo de Hilbert. Demonstramos que não há sistemas de Hilbert finitos unidimensionais que capturem essa lógica, mas que ela habita uma relação de consequência bidimensional finitamente axiomatizável por um sistema de Hilbert bidimensional. A existência desse sistema segue diretamente do algoritmo de axiomatização proposto, em vista da semântica bidimensional 5-valorada não-determinística suficientemente expressiva que determina a relação de consequência bidimensional mencionada. 2022-04-05T00:22:36Z 2022-04-05T00:22:36Z 2022-02-21 masterThesis GREATI, Vitor Rodrigues. Hilbert-style formalism for two-dimensional notions of consequence. 2022. 142f. Dissertação (Mestrado em Sistemas e Computação) - Centro de Ciências Exatas e da Terra, Universidade Federal do Rio Grande do Norte, Natal, 2022. https://repositorio.ufrn.br/handle/123456789/46792 pt_BR Acesso Aberto application/pdf Universidade Federal do Rio Grande do Norte Brasil UFRN PROGRAMA DE PÓS-GRADUAÇÃO EM SISTEMAS E COMPUTAÇÃO