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.

VCLA Awards 2023, Runner up of the Outstanding Master Thesis Award, Vienna, Austria

*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.