LK の特性
出典: フリー百科事典『ウィキペディア(Wikipedia)』 (2019/11/21 02:32 UTC 版)
この規則体系は一階述語論理において健全かつ完全である。すなわち、 Γ ⊢ A {\displaystyle \Gamma \vdash A} が上記規則群から導出される場合に限って、前提 Γ ( Γ ⊨ A {\displaystyle \Gamma \vDash A} ) から命題 A が意味論的に導かれる。 シークエント計算では、カット除去定理が許される。これをゲンツェンの Hauptsatz(主定理)とも呼ぶ。
※この「LK の特性」の解説は、「シークエント計算」の解説の一部です。
「LK の特性」を含む「シークエント計算」の記事については、「シークエント計算」の概要を参照ください。
- LK の特性のページへのリンク