AI 中文总结
本文在一阶逻辑语境下，基于Smullyan的块演算，确立其结构性质与切消，证明其与Gentzen LK的对应关系，为sequent式tableaux提供了系统的结构分析。
AI 中文摘要
我们以无符号sequent式记号对一阶块演算进行了自包含的推导：反驳树的每个节点携带有限块Π=Γ∪¬[Δ]，否定由显式规则支配，分支在互补文字对处闭合。该演算本质上是Smullyan的，定理也如此；本文提供的是它们的不同排列。结构性质按G3式sequent演算熟悉的依赖顺序确立：任意公式的闭合是可容许的，弱化与参数替换在保持高度的情况下可容许，每条规则是保持高度可逆的，且切（cut）是可容许的，后者由前三者导出而非相反。由此得到公平策略下的可靠性、完备性、可数紧致性与可数模型性质，以及保证每个公平构造终止的句法准则。随后双向证明其与Gentzen的LK（含显式弱化的常规形式）的对应关系，这需要基于参数的引理，而基于集合的Gentzen系统无需此类引理。
英文摘要
We give a self-contained development of the first-order block calculus in unsigned sequent-style notation: each node of the refutation tree carries a finite block $Π= Γ\cup \neg[Δ]$, negation is governed by explicit rules, and a branch closes on a complementary pair of literals. The calculus is Smullyan's, and so in substance are the theorems; what is offered here is a different arrangement of them. The structural properties are established in the order of dependence familiar from G3-style sequent calculi: closure on arbitrary formulae is admissible, weakening and the substitution of parameters are admissible with preservation of the height, every rule is height-preserving invertible, and cut is admissible, the last being derived from the first three rather than conversely. Soundness, completeness under a fair strategy, countable compactness and the countable model property follow, together with a syntactic criterion under which every fair construction terminates. The correspondence is then proved, in both directions and with cut included, with Gentzen's LK in its usual presentation with explicit weakening, which requires lemmas on parameters that set-based Gentzen systems do not need.
