Vitor Greati

This talk is a brief introduction to the investigation of computational properties of non-classical propositional logics. We begin by understanding the very basics of non-classical logics, focusing on many-valued and substructural logics. Then, we see what it means for a logic to be decidable or not, and appreciate some of the challenges in studying such property. For some decidable logics, we also see some complexity results, touching in an accessible way topics like structural proof theory and the theory of well-quasi-orderings.

Substructural logics lack structural properties like weakening, contraction, associativity, or exchange (commutativity) that are familiar from classical and intuitionistic logic. The omission of such properties make these logics well-suited for reasoning about resources in various different senses. Substructural logics appear across theoretical computer science, linguistics, and philosophy, and they possess an intricate mathematical and logical structure. For the same reasons, these logics exhibit vast computational diversity including membership in (ordinal-indexed) fast-growing complexity classes. Here we consider substructural logics with weak versions of the usual contraction or weakening rules (collectively referred to as knotted axioms in the literature), and infinitely many of their axiomatic extensions. A host of new decidability and complexity upper bounds are established by exploiting the underlying knotted well-quasi-orders (wqos) and drawing on techniques from proof theory and wqo theory, contributing also with new length theorems in controlled bad sequences for knotted wqos and their power set extensions.

Many thanks to all the VCLA Awards 2023 organizers and all those that read and assessed my Master’s thesis! I’m very honoured for being the runner up in this competition. Finally, congratulations to the winners and their amazing works!

Many thanks to Wesley Fussner for the invitation to this academic visit in Bern, where I could present the work I developed during my Master’s and discuss my current work on substructural logics with the group in Bern (including Gavin St. John, with whom I very nice and fruitful discussions).

The characterizing properties of a proof-theoretical presentation of a given logic may hang on the choice of proof formalism, on the shape of the logical rules and of the sequents manipulated by a given proof system, on the underlying notion of consequence, and even on the expressiveness of its linguistic resources and on the logical framework into which it is embedded. Standard (one-dimensional) logics determined by (non-deterministic) logical matrices are known to be axiomatizable by analytic and possibly finite proof systems as soon as they turn out to satisfy a certain constraint of sufficient expressiveness. In this paper we introduce a recipe for cooking up a two-dimensional logical matrix (or B-matrix) by the combination of two (possibly partial) non-deterministic logical matrices. We will show that such a combination may result in B-matrices satisfying the property of sufficient expressiveness, even when the input matrices are not sufficiently expressive in isolation, and we will use this result to show that one-dimensional logics that are not finitely axiomatizable may inhabit finitely axiomatizable two-dimensional logics, becoming, thus, finitely axiomatizable by the addition of an extra dimension. We will illustrate the said construction using a well-known logic of formal inconsistency called mCi. We will first prove that this logic is not finitely axiomatizable by a one-dimensional (generalized) Hilbert-style system. Then, taking advantage of a known 5-valued non-deterministic logical matrix for this logic, we will combine it with another one, conveniently chosen so as to give rise to a B-matrix that is axiomatized by a two-dimensional Hilbert-style system that is both finite and analytic.

No finite Hilbert-style axiomatization was known so far for Paraconsistent Weak Kleene and Bochvar-Kleene logics. In this presentation, we offer finite and analytic Set-Set (that is, multiple-conclusion) systems for these logics, as well as we show finite traditional Hilbert-style systems for them, answering positively to the open question of whether these two logics are finitely axiomatizable. At the end, we point to future directions of research fundamented on two-dimensional notions of logic, proposing to capture in the same logical structure these two logics plus the associated (non-Tarskian) ts- and st-consequences.

D. Shoesmith and T. Smiley (1978) introduced a generalization of traditional Hilbert-style systems in which rules of inference may have multiple formulas in their conclusions and derivations are trees labelled with sets of formulas. These modifications created the possibility of generating (finite) analytic Hilbert-style systems for a very inclusive class of logics determined by (finite) non-deterministic matrices (C. Caleiro and S. Marcelino, 2019). The analyticity of these systems ensures that, when searching for a proof, we only need to consider formulas in a set that is completely determined by the subformulas of the statement of interest. This contrasts with usual traditional Hilbert-style systems (for classical and intuitionistic logics, for example) lacking analyticity results. In this talk, we will present how the above notions and result may be generalized to the context of two-dimensional logics and two-dimensional non-deterministic matrices (in the sense of C. Blasio, J. Marcos and H. Wansing, 2017). We will also see that logics failing to be finitely axiomatizable may inhabit finitely axiomatizable two-dimensional logics. We will illustrate this fact with the well-known logic of formal inconsistency called mCi, first showing that it fails to be finitely axiomatizable in one dimension and then presenting a finite and analytic two-dimensional Hilbert-style system for it.

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 truth-values, 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.

In this work, we introduce a way of combining two non-deterministic logical matrices into a two-dimensional non-deterministic matrix (or B-matrix), from which the logics determined by the former are easily recoverable. We will see that this combination may result in B-matrices satisfying the property of sufficient expressiveness (useful for generating analytic and possibly finite proof systems for the logic associated to the B-matrix), even if the input matrices are not sufficiently expressive. Consequently, one-dimensional logics that are not finitely axiomatizable may inhabit finitely axiomatizable two-dimensional logics, being, thus, finitely axiomatizable in two dimensions. We will illustrate this fact using the well-known logic of formal inconsistency (LFI) called mCi. We will first prove that this logic is non-finitely axiomatizable by a one-dimensional Hilbert-style system. Then, taking advantage of the 5-valued non-deterministic matrix for this logic, we will conveniently combine such matrix with another one, producing a B-matrix that is axiomatizable by a two-dimensional Hilbert-style system that is both finite and analytic. In the path towards proving the first result, we will show that mCi is the limit of an infinite strictly increasing chain of LFIs.

Learn how to implement bilateralism via a two-dimensional notion of consequence, actualized by a two-dimensional notion of logical matrices and a two-dimensional Hilbert-style proof formalism. Automatically generate two-dimensional analytic calculi for sufficiently expressive two-dimensional matrices and do proof search over the resulting systems. If you have luck, your favorite logic may live inside a two-dimensional consequence induced by an analytic calculus, and you may even discover, just by looking at the rules of inference, that it is polynomial-time decidable!

Advanced talk given to undergraduate and graduate students of UFRN. Covers basic and some advanced topics on Universal Algebra and shows how to enrich De Morgan algebras with a perfection operator.

Classical logic, under a universal-algebraic consequence-theoretic perspective, can be defined as the logic induced by the complete clone over \(\{0, 1\}\). Up to isomorphism, any other 2-valued logic may then be seen as a sublogic or a fragment of Classical Logic. In 1941, Emil Post studied the lattice of all the 2-valued clones ordered under inclusion. Wolfgang Rautenberg explored this lattice in order to show that all fragments of Classical Logic are strongly finitely axiomatizable. Rautenberg used an unusual notation and overloaded it several times, causing confusion; in addition, he presented incomplete proofs and made lots of typographical errors, imprecisions and mistakes. In particular, the main fragments of Classical Logic — expression here that refers to those fragments related to the proofs presented by Rautenberg in the first part of his paper — deserve a more rigorous and accessible presentation, because they promote important discussions and results about the remaining fragments. Also, they give bases to the recursive procedures in the second part of the proof of the axiomatizability of all 2-valued fragments. This work proposes a rephrasing of the proofs for the main fragments, with a more modern notation, with more attention to the details and the writing, and with the inclusion of all axiomatizations of the clones under investigation. In addition, the involved proof systems will be specified in the language of the Lean theorem prover, and the derivations necessary for the completeness proofs will be verified with the aid of this tool. In this way, the presentation of the proof of the result given by Rautenberg will be more accessible, understandable and trustworthy to the community.

From a universal-algebraic consequence-theoretic perspective, classical logic can be defined as the logic induced by the complete clone over \(\{0,1\}\). Up to isomorphism, any other \mbox{2-valued logic} may then be seen as a sublogic / fragment of classical logic. In spite of the theoretical straightforwardness of such a presentation, one may argue that there is still very little common knowledge about the minimal combination of such fragments, which in principle may be obtained by simply merging the corresponding Hilbert calculi. In 1941, Emil Post studied the lattice of all the 2-valued clones, (sets of finitary operations closed under projection and composition) ordered under inclusion. This lattice —countably infinite yet constituted of finitely generated members— has constituted ever since an invaluable source of information and insights about the relationships among the sublogics of classical logic. Wolfgang Rautenberg explored Post’s classification in proving that every 2-valued logic is strongly finitely axiomatizable; it is worth noting that this proof carries along an effective procedure for producing a Hilbert calculus to any fragment of classical logic. Thus, for each finite collection of 2-valued operations given as input, the only challenge concerning the implementation of Rautenberg’s algorithm in a computational system would be to find the exact clone that it describes within Post’s lattice. By an application of Kleene’s Fixed-Point Theorem, any finite set of boolean functions may be closed under projection and finitary multiple composition in finite time, in a bottom-up fashion; as the thereby produced boolean clone must live in the corresponding lattice, by a clever top-down analysis of the latter one may then find its precise location. We have implemented both the latter tasks using the Haskell programming language and distributed the resulting system as a RESTful web service endpoint and as a web application to be freely used by the community. With that, the first step towards the automated extraction of a Hilbert calculus for any fragment of classical logic was made fully operational; the remainder of the work is to be based on Rautenberg’s axiomatization procedure.

Uma lógica \(\mathcal{L}\) é bivalorada quando é caracterizável por uma matriz lógica \(\langle \{0,1\}, \{1\}, \cdot_2 \rangle\), onde \(\cdot_2\) denota interpretações dos conectivos da assinatura de \(\mathcal{L}\). A lógica clássica é qualquer lógica bivalorada cujo clone da álgebra de dois elementos associada possui todas as operações sobre o conjunto subjacente. Dessa forma, qualquer outra lógica bivalorada é uma sublógica – ou fragmento – da lógica clássica. Emil Post, matemático e lógico americano do século XX, apresentou, em 1941, uma descrição completa de todos os clones sobre o conjunto \(\{0,1\}\), na forma de um reticulado formado pelo conjunto dos referidos clones ordenado pela relação de inclusão. O reticulado de Post constitui uma fonte valiosa de informação sobre os fragmentos da lógica clássica, permitindo, por exemplo, extrair conclusões acerca dos efeitos da adição de determinados conectivos booleanos a certos fragmentos. Baseado na estrutura desse reticulado, Wolfgang Rautenberg, matemático alemão também do século XX, em artigo publicado em 1981, apresentou um procedimento para a extração de axiomatizações – ou cálculos de Hilbert – para matrizes bivaloradas, e, portanto, para fragmentos da lógica clássica induzidos por tais matrizes. Tal contribuição é especialmente útil para aplicações interessadas nas lógicas oriundas das combinações de fragmentos da lógica clássica, visto que os cálculos de Hilbert constituem um ambiente simples e propício para a criação de tais combinações e para os estudos dos sistemas complexos derivados a partir delas. Apesar disso, ainda não há uma implementação computacional desse procedimento. O trabalho sendo desenvolvido busca preencher essa lacuna, por intermédio da produção de um sistema computacional que receba como entrada a especificação semântica de um fragmento da lógica clássica, escrito por meio de uma interface amigável, e produza uma axiomatização correspondente segundo o método descrito por Rautenberg. Esta apresentação abordará detalhes e exemplos sobre os fragmentos da lógica clássica no contexto do reticulado de Post, além de explanar o que foi até então estudado quanto ao procedimento exposto por Rautenberg, elucidando a importância deste – e, consequentemente, a do presente trabalho – para a seara da combinação entre lógicas.