19/01/17 10:54:45.59 lTvr+WmF.net
>>615
>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
を公理にすると排中律が出ると思うよ