论文标题
无限公理逻辑的有限二维证明系统
Finite two-dimensional proof systems for non-finitely axiomatizable logics
论文作者
论文摘要
给定逻辑的证明理论表现的特征可能存在于证明形式主义的选择，逻辑规则的形状和由给定证明系统操纵的序列，其后果的基本概念，甚至基于其语言资源的表现力以及其嵌入到嵌入式的逻辑框架上。已知由（非确定性）逻辑矩阵确定的标准（一维逻辑）可以通过分析性和有限证明系统来满足足够表现力的某些约束。在本文中，我们介绍了一种食谱，用于通过两个（可能是部分）非确定性逻辑矩阵的组合来烹饪二维逻辑矩阵（或B-Matrix）。 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.我们将使用众所周知的名为MCI的正式不一致逻辑来说明上述结构。我们首先证明，这种逻辑不是由一维（广义）希尔伯特式系统有限的公理化。然后，利用该逻辑的已知5值非确定性逻辑矩阵，我们将与另一个逻辑矩阵相结合，可方便地选择，以产生B-Matrix，该B-Matrix通过二维Hilbert-Style System AxiOmation，这既是有限和分析又是有限的。
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.
