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.