树与共树的双中间逻辑局部可判性

双 Heyting 代数当且仅当其素滤器的序 poset 为树的序偶时，才验证 Gödel-Dummett 公理 $(p\to q)\vee (q\to p)$。此类双 Heyting 代数称为双 Gödel 代数，构成一种由 Gödel-Dummett 公理所公理化的扩展 $\operatorname{\mathsf{bi-GD}}$ 的双直觉逻辑。本文确立了判断有限可公理化 $\operatorname{\mathsf{bi-GD}}$ 延伸是否局部表格的判定问题的可判性。值得注意的是，若 $L$ 是 $\operatorname{\mathsf{bi-GD}}$ 的延伸，则 $L$ 为局部表格当且仅当 $L$ 不包含于 $Log(FC)$，后者是一族特定有限共树（即树的序偶）的逻辑，称为有限comb。我们证明 $Log(FC)$ 是有限可公理化的。由于该逻辑同样具有有限模型属性，因此是可判定的。因此，上述局部表格性的表述确保了上述问题的可判性。