Vitor Greati

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.