以前に読書会で紹介のあった、背理法による排中律の証明。
(1) ^(E or ^E) : [仮定1]
(2) ^E => (E or ^E) : [公理8]
(3) ^(E or ^E) => (^E => ^(E or ^E)) : [公理1]
(4) ^E => ^(E or ^E) : [mp{(1),(3)}]
(5) (^E => (E or ^E)) => ((^E => ^(E or ^E)) => ^^E) : [公理10]
(6) ^^E : [mp{(2),(4),(5)}]
(7) ^^E => ((^^E => E) E) : [公理3]
(8) E : [mp{(6),(7)}]
(7) E => (E or ^E) : [公理7]
(8) ^(E or ^E) => (E => ^(E or ^E)) : [公理1]
(9) E => ^(E or ^E) : [mp{(1),(8)}]
(10) (E => (E or ^E)) => ((E => ^(E or ^E)) => ^E) : [公理10]
(11) ^E : [mp{(7),(8),(10)}]
(8)と(11)より 「E かつ ^E」となるので矛盾。
原因は仮定1にある。
よって仮定1の否定である、
E or ^E
が公理である。
