命題論理の記号をなるべく少なくする

これをすると色々帰納法の時や定理証明支援系で証明する必要があることを少なくできるはず

戸次大介; "数理論理学"にちらっと書いてあった気がする

$ \to,\botだけを用いることは定義3.104に記述あり

$ \to,\botの組

古典命題論理においては$ \botと$ \toだけがあればいいはず

0項演算子$ \bot

2項演算子$ \to

後の論理演算子はシュガーシンタクスとして導入する

$ \top := \bot \to \bot

$ \lnot A := A \to \bot

$ A \lor B := \lnot A \to B

$ A \land B := \lnot (\lnot A \lor \lnot B)

もう少しいい方法があるはず…

$ A \leftrightarrow B := (A \to B) \land (B \to A)

付値に対する再帰的定義/意味論

$ v(\bot) = 0

$ v(A \to B) = 1$ \iff$ v(A) = 0または$ v(B) = 1

シュガーシンタクスに対しての確認

$ v(\lnot A) = 1

$ \iff$ v(A \to \bot) = 1

$ \iff$ v(A)=0または$ v(\bot)=1

$ \iff$ v(A) = 0

当然後者は常に成り立たない

後省略