>>160
聞きかじった知識なので、又聞きのようになってしまうけど、解説のようなもの：

（１）導入した仮定Pから矛盾⊥が導かれた場合、¬Pを結論して良いか？
これは普通の背理法。許される
ただし、これと独立にPも証明されることもあるかもしれない

（２）(P→⊥) ∧ (¬P→⊥) から何が言えるか？
（１）の推論規則から、これは(¬P) ∧ (¬(¬P))
ここから矛盾⊥が導かれる

（３）（１）や（２）で行った推論は排中律か？
違う。排中律とは、「P∨¬Pの形の仮定をいつでも追加してよい」という推論規則のこと