2005-06-20から1日間の記事一覧

第6章 シークェント計算(4)

Gの完全性の証明(続き) 復習 公平な導出木 ΦとΨ(各辺の無限経路のある位置以上の位置に存在し続ける論理式の和集合) 任意のシークェントに対して公平な導出木が存在する。 →展開レベルの小さいものから展開する。 補題6.7.6 ※このとき、有限な公理で終了…