>>160
分かりやすい解説ありがとうございます。

>（１）導入した仮定Pから矛盾⊥が導かれた場合、¬Pを結論して良いか？
>これは普通の背理法。許される
>ただし、これと独立にPも証明されることもあるかもしれない
>>104でいうところの1に相当すると考えていいということでしょうか
　ZFCにおける連続体仮説とか

>（２）(P→⊥) ∧ (¬P→⊥) から何が言えるか？
>（１）の推論規則から、これは(¬P) ∧ (¬(¬P))
>ここから矛盾⊥が導かれる
　これが正にお伺いしたかったことです。
　ということは>>104の4の解釈はやはり単に"考えている体系において矛盾である"、という解釈で問題ないんでしょうか。

>（３）（１）や（２）で行った推論は排中律か？
>違う。排中律とは、「P∨¬Pの形の仮定をいつでも追加してよい」という推論規則のこと
　(1)や(2)の推論が排中律の証明ではないことは理解しているつもりですが、
　(1)の推論を行う上でp∨¬pを無条件に成り立つことを前提としていて、それゆえ背理法が使える、
　という認識で合っていますでしょうか?

回答者の方の丁寧な解説に当方の頭がついていってない感じもしますが…w
本当にどうもありがとうございます。