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

数理論理学

6.4 その他のシークェント計算

カット規則

\frac{\Gamma \Rightarrow \Delta,A \ A,\Gamma' \Rightarrow \Delta'}{\Gamma \Gamma' \Rightarrow \Delta \Delta'}

等号に関する公理シークェント

G^{\approx}=G^{CUT} + \approx

  • \Rightarrow s \approx s
  • s_1\approx t_1 ,...,s_n \approx t_n \Rightarrow f(s_1,...,s_n) \approx f(t_1,...,tn)
  • s_1\approx t_1 ,...,s_n \approx t_n , P(s_1,...,s_n) \Rightarrow P(t_1,...,tn)

等式論理という分野がある。

その他の規則
  • 弱化規則
  • 縮約規則

シークェント計算の健全性

（書けなかった）

シークェント計算の完全性

=Γ⇒Δならば├Γ⇒Δ

対偶を証明する。
（全部やる…のは大変だ）