原子初期シーケントの完全性

シーケント計算において、原子初期シーケントの完全性とは、初期シーケントA ⊢ A ( Aは任意の式) は、原子初期シーケントp ⊢ p ( pは原子式)からのみ導出できるという定理である。この定理は、ラムダ計算におけるイータ展開に類似した役割を果たし、カット消去とベータ縮約の双対となる。通常、カット消去よりもはるかに容易に、Aの構造に関する帰納法によって証明できる。

• 竹内嘉司。『証明論』 。 『論理学と数学の基礎に関する研究』第81巻。ノースホランド社、アムステルダム、1975年。
• アンネ・シェルプ・トロエルストラ、ヘルムート・シュヴィヒテンベルク著。 『基礎証明論』。第2版、図解入り、改訂版。ケンブリッジ大学出版局、2000年刊行。