(¬p → p) → pは恒真だが非自明に思える(Löbの定理みたいな)
そういえばこの形式の論理式には驚嘆すべき帰結(Consequentia mirabilis)という名前が付いていたことを思い出す
https://en.wikipedia.org/wiki/Consequentia_mirabilis [参照]
様々な目的に使える、日本の汎用マストドンサーバーです。安定した利用環境と、多数の独自機能を提供しています。