Computability of logical problems associated to partial non-deterministic matrices

Pedro Gonçalo Godinho Filipe

Key information

Authors:

Pedro Gonçalo Godinho Filipe (Pedro Gonçalo Godinho Filipe)

Supervisors:

Carlos Manuel Costa Lourenço Caleiro (Carlos Manuel Costa Lourenço Caleiro); Sérgio Roseiro Teles Marcelino (Sérgio Roseiro Teles Marcelino)

Published in

November 11, 2022

Abstract

Recentemente, temos observado um aumento no interesse sobre semânticas algébricas para lógicas, com interpretações não funcionais dos conectivos proposicionais, nomeadamente matrizes não-deterministicas parciais (PNmatrizes), que generalizam a noção tradicional de matriz lógica, permitindo não-determinismo e parcialidade. Apesar deste interesse reforçado, ainda não se sabe muito sobre as propriedades algébricas destas estruturas, nomeadamente no contexto da Lógica Algébrica Abstrata, ou sobre a decidibilidade das mesmas. Nesta tese, procuramos estudar a computabilidade e complexidade de vários problemas de decisão relacionados com lógicas induzidas por PNmatrizes, e pelas suas subclasses principais, para os quais já existe resposta no contexto de matrizes lógicas tradicionais. Com isto, procuramos dar um primeiro passo no sentido do desenvolvimento de uma teoria geral de algebrização de lógicas baseada em PNmatrizes. Com este objetivo, exploramos várias construções algébricas que tomam partido da extra expressividade proporcionada pelo não-determinismo e pela parcialidade, de forma a manipular várias caracteristicas das lógicas induzidas. Estas construções são diversas. Criamos uma ponte entre matrizes não-deterministicas (Nmatrizes) e máquinas de registos (ao estilo de Minsky), ao mostrar como construir Nmatrizes que codificam, no seu conjunto de teoremas, precisamente as computações finitas de uma dada máquina de registos. Estendemos resultados conhecidos de lógicas de inclusão e semânticas de infeção — sobre as quais também temos observado um interesse renovado nos últmios anos — onde utilizamos a parcialidade e o não-determinismo para caracterizar uma classe rnais geral de lógicas de inclusão. Filtramos a lógica induzida por uma dada PNmatriz, mantendo apenas as consequências cuja conclusão é também premissa, ou teorema da lógica inicial, utilizando o não-determinismo para duplicar valores de verdade. Apresentamos uma construção que relaciona o problema de decidir se uma dada Nmatriz tem teoremas com o problema de decidir se uma dada Nmatriz é monádica. Finalmente, apresentamos um pumping lemma para PNmatrizes que constitui um primeiro passo no estudo de condições necessárias e/ou suficientes para uma lógica admitir uma semântica finita baseada em PNmatrizes. Na última secção aplicamos estas construções ao estudo de problemas de decidibilidade concretos. Os problemas abordados podem ser divididos em três categorias: problemas relacionados com teoremas, problemas relacionados com lógicas, e um último problema relacionado com monadicidade. Os resultados obtidos neste contexto são também bastante diversos: alguns problema mantêm a sua complexidade, para outros a sua complexidade aumenta e, para outros ainda, a decidibilidade é perdida. In recent years, we have seen an increased interest in non-truth functional algebraic semantics for logic, namely partial non-deterministic matrices (PNmatrices), which generalize the traditional, truth-functional, notion of logical matrix by allowing for non-determinism and partiality. Despite this increased interest, not much is yet known about the algebraic properties of these structures, particularly in what concerns Abstract Algebraic Logic, or about the decidability of such properties. In this thesis, we aim at providing an answer to the computability/complexity status of various logical problems regarding PNmatrices, and their most relevant subclasses, for which an answer is already known when restricted to traditional matrices. By doing so, we hope to take a first step towards a general theory of Algebraization for PNmatrices. To this end, we explore various algebraic constructions, that take advantage of the extra expressivity provided by non-determinism and partiality, in order to manipulate various aspects of the induced logics. The explored constructions are diverse. We create a bridge between nondeterministic matrices (Nmatrices) and finite deterministic counter-machines by showing how to construct Nmatrices that encode, in their set of theorems, precisely the finite computations of a given counter-machine. We extend known results of inclusion logics and infectious semantics - that have also seen a renewed interest in recent years - using non-determinism in order to characterize a wider class of inclusion logics. We filter the logic induced by a given PNmatrix, keeping only the consequences for which the conclusion is already a theorem, using a technique of duplication of elements allowed by non-determinism, and present a construction that relates the problem of the existence of theorems with the problem of deciding if a PNmatrix is monadic. Finally, we also present a Pumping Lemma for PNmatrices that provides a first step towards the characterization of finite-valuedness for these structures. In the last section, we apply these constructions to study of concrete decidability problems. The studied problems can be divided into three categories: problems regarding theorems, problems regarding logics and one last problem regarding monadicity. The results obtained in this context are also quite rich: some problems retain their complexity, others see an increase in their asymptotic complexity, and other lose their decidability altogether.