二重否定除去と背理法は同値

二重否定除去から背理法を導くことができる

https://kakeru.app/87ae6956a6a21f8310d3d781f59c8b57 https://i.kakeru.app/87ae6956a6a21f8310d3d781f59c8b57.svg

逆も導ける

https://kakeru.app/19f6bbbf82f6ff4ca2ce39cfb13c3160 https://i.kakeru.app/19f6bbbf82f6ff4ca2ce39cfb13c3160.svg

全然手応えのない証明だったtakker.icon

ほぼ定義を書いているようなものだった

ていうかこれただの定義じゃん

$ \lnot P:\iff(P\implies\bot)だから$ (\lnot P\implies\bot)\iff\lnot\lnot P