论文标题
中间逻辑中的统一类型和联合分裂
Unification types and union splittings in intermediate logics
论文作者
论文摘要
遵循其kripke模型的局部表格逻辑的表征[10]，我们确定了某些中间逻辑的统一类型（{\ sf int}的扩展）。恰好有四个最大逻辑，具有无效统一$ {\ Mathsf l}（\ Mathfrak r_ {2}+）$，$ {\ Mathsf L}（\ Mathfrak r_ {2}）\ Cap {\ Mathsf L}（\ Mathsf L}（ g_ {3}）$和$ {\ mathsf l}（\ mathfrak g_ {3}+）$，它们是表格的。遗传性统一只有两个最小逻辑：$ {\ mathsf l} $（$ \ mathbf f_ {un} $），具有遗传性统一的最少逻辑，以及$ {\ mathsf l} $（$ \ \ \ \ \ \ \ \ \ m athbf f_ {pr} $）与她的遗忘者近似locialitive oiltimimitive;它们是局部表格的。单一和非项目的逻辑需要一些纯公式的MGU的其他变量，而具有投影近似的单一逻辑则完全是投影性的。局部表格的中间逻辑都没有无限制的统一。具有统一的逻辑（但不是遗传性统一）很少见，并且在大多数具有无效统一的人中都散布，请参见$ \ Mathsf H_3 \ Mathsf B_2 $及其扩展的示例。
Following a characterization [10] of locally tabular logics with finitary (or unitary) unification by their Kripke models we determine the unification types of some intermediate logics (extensions of {\sf INT}). There are exactly four maximal logics with nullary unification ${\mathsf L}(\mathfrak R_{2}+)$, ${\mathsf L}(\mathfrak R_{2})\cap{\mathsf L}(\mathfrak F_{2})$, ${\mathsf L}(\mathfrak G_{3})$ and ${\mathsf L}(\mathfrak G_{3}+)$ and they are tabular. There are only two minimal logics with hereditary finitary unification: ${\mathsf L}$($\mathbf F_{un}$), the least logic with hereditary unitary unification, and ${\mathsf L}$( $\mathbf F_{pr}$) the least logic with hereditary projective approximation; they are locally tabular. Unitary and non-projective logics need additional variables for mgu's of some unifiable formulas, and unitary logics with projective approximation are exactly projective. None of locally tabular intermediate logics has infinitary unification. Logics with finitary, but not hereditary finitary, unification are rare and scattered among the majority of those with nullary unification, see the example of $\mathsf H_3\mathsf B_2$ and its extensions.
