带等式的相继式演算中结构规则的可容许性

基于关于带附加原子规则的相继式演算中结构规则可容许性的一般定理，我们对 ${\bf G3[mic]}$ 相继式演算的若干带有等式规则的扩展进行了证明论分析，其中包括 H.Wang 最初提出的扩展。在经典情形下，我们将我们的结果与带等式的一阶逻辑语义表方法联系起来。特别是我们确定，对于不含函数符号的语言，在 Fitting 的替代语义表方法中，可以同时施加严格性（不允许重复修改后的等式）和等量替换的方向性。在将这一结果扩展到含函数符号的语言方面取得了显著进展，尽管是否可行仍有待确定。我们还简要考虑了在经典情形下与语义表方法相关的系统，其中可以通过随意添加恒等式来扩展分支，并得出在这种情况下也可以施加严格性。此外，我们讨论了 Orevkov 已知的对带有结构规则的相继式演算成立的非增长性质的强化形式在多大程度上也适用于当前语境。