- 382 名前：369 mailto:sage [2007/08/05(日) 12:58:02 ]
- 直観主義論理で、Sequent Ａ⊃Ｂ⇒¬Ｂ⊃¬Ａの証明のＢに¬¬Ａを採用
すれば、三重否定からの二重否定の除去 ⇒¬¬¬Ａ⊃¬Ａが得られると
聞いて素直にSequentで証明したことがある。
Ａ⇒Ａ
−−−−−−−−−
¬Ａ，Ａ⇒ Ａ，Ａ⊃¬¬Ａ⇒¬¬Ａ
−−−−−−−−− −−−−−−−−−−−−−−−−−−−
Ａ⇒¬¬Ａ ¬¬¬Ａ，Ａ⊃¬¬Ａ⇒¬Ａ
−−−−−−−−− −−−−−−−−−−−−−−−−−−−
⇒Ａ⊃¬¬Ａ Ａ⊃¬¬Ａ⇒¬¬¬Ａ⊃¬Ａ
−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−
⇒¬¬¬Ａ⊃¬Ａ
でもそれをCut除去定理の証明の方法でCutを除去していったらすごく簡単
になってびっくりしたんだよね。
Ａ⇒Ａ
−−−−−−−−−−−−−
¬Ａ，Ａ⇒
−−−−−−−−−−−−−
Ａ⇒¬¬Ａ
−−−−−−−−−−−−−
¬¬¬Ａ，Ａ⇒
−−−−−−−−−−−−−
¬¬¬Ａ⇒¬Ａ
−−−−−−−−−−−−−
⇒¬¬¬Ａ⊃¬Ａ
私が言いたかったのは具体的に言うとこういうこと。
|
 |
