否定の導入
否定の導入
定理
T: 公理系
$ \varphi 閉論理式
このとき$ T \cup \{ \varphi \} が矛盾するならば、$ T \vdash \neg \varphi
証明
前定理より$ T \cup \{ \varphi\} \vdash \neg \varphi
よって$ T \vdash \varphi \to \neg \varphi
https://scrapbox.io/files/68eb896bd9245f7799575f4d.png
https://gyazo.com/366050c5ad050ce4e24a380402565aa9
前回の動画で出たものをつかう
系（狭義の背理法）
$ T \cup \{ \neg \varphi\} が矛盾するならば$ T \vdash \varphi
https://gyazo.com/7530c17ba3a8c835b6c12f43e61a7166
$ \neg\neg \varphi \to \varphiこれを使わないと証明できない
これは、排中律が入っているから証明できる
仮定を入れない場合は、系は成立しない
https://gyazo.com/67dcea5dc02ae208d92c1ba50736641f
狭義の背理法
https://scrapbox.io/files/68eb8a5a3b09a5fd821c1880.png
否定の導入は記号$ \negにとって本質的な性質
否定の導入を使ってこの記号を定義する方法もある
新井数学基礎論