Finite two-dimensional proof systems for non-finitely axiomatizable logics
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.