>p∨¬pをそれより弱い主張の(p→q)∧(p→¬q)→¬pに替えて使う
後者は最小論理で示せるぐらいだからあんまり意味ないんじゃ？
p, (p→q)∧(p→¬q) |- p, p→q
p, p→q |- q
p, (p→q)∧(p→¬q) |- p, p→¬q
p, p→¬q |- ¬q
p, (p→q)∧(p→¬q) |- q, ¬q
(p→q)∧(p→¬q) |- ¬p
この主張は
pを仮定して矛盾が出たら¬pを結論するっていう最小論理の公理と同値で
q, p→¬q |- ¬p
のタイプの背理法とも同値
直観主義論理で排除される背理法は
q, ¬p→¬q |- p
あと
(¬p→q)∧(¬p→¬q)→p
を公理にすると排中律が出ると思うよ
