TypeScriptの型システム上に命題論理を実装
セマンティクス
真偽値
$ \mathbb{B} = \{1,0\}を定める．
普通，$ 1は真，$ 0は偽と呼ぶ．
code:bool.ts
type TT = 1;
type FF = 0;
type BB = TT | FF;
真理関数
1項真理関数$ \lnot: \mathbb{B} \mapsto \mathbb{B}を導入する．
$ b = 0なら，$ \lnot(b) = 1．
$ b = 1なら，$ \lnot(b) = 0．
普通，$ \lnotは「否定，NOT」と呼ばれる．
2項真理関数$ \lor: \mathbb{B}^2 \mapsto \mathbb{B}を導入する．
$ b_1=0,b_2=0なら，$ \lor(b_1,b_2) = 0．
その他の場合，$ \lor(b_1,b_2) = 1．
普通，$ \lorは「または，OR」と呼ばれる．
$ \lnot,\lorを用いて他の真理関数$ \land,\to,\leftrightarrowを糖衣構文として定める．
$ \land(b_1,b_2) = \lnot(\lor(\lnot(b_1),\lnot(b_2)))
「かつ，AND」と呼ばれる．
$ \to(b_1,b_2) = \lor(\lnot(b_1),b_2)
「ならば，IMP」と呼ばれる．
$ \leftrightarrow(b_1,b_2) = \land(\to(b_1,b_2),\to(b_2,b_1))
これの呼称はあまり定まっていないと思う
「IFF」と呼んでいる
code:op.ts
type Not<P extends BB> = P extends TT ? FF : TT
type Or<P extends BB, Q extends BB> = P extends TT ? TT : Q extends TT ? TT : FF
type And<P extends BB, Q extends BB> = Not<Or<Not<P>,Not<Q>>>
type Imp<P extends BB, Q extends BB> = Or<Not<P>,Q>
type Iff<P extends BB, Q extends BB> = And<Imp<P,Q>,Imp<Q,P>>
シンタクス
記号の集合
全ての記号$ \Sigma=\{p,q,r,\dots, \lnot,\land,\lor,\to,\leftrightarrow,,,(, ) \}
有限個の変数: $ p,q,r,\dots
関数記号$ \lnot,\land,\lor,\to,\leftrightarrow
コンマ$ ,とカッコ$ (,)
記号列
$ \Sigmaの要素を有限個並べたものは記号列あるいは式と呼ぶ．
例:
$ p(\lnot\land\to qrqr((((
$ \lnot q ) (p \to
$ \lnot (p)
論理式
記号列のうち，次の形をしているものは論理式と呼ばれる．
1. 変数$ p,q,r,\dotsを一つだけ並べた式
例: $ p
2. $ \varphiが論理式であるとき$ \lnot(\varphi)
例
$ \lnot(p)
$ \varphiとして$ p
$ \lnot(\lnot(p))
$ \varphiとして$ \lnot(p)
$ \lnot(\lor(p,q))
3. $ \varphi,\psiが論理式であるとき
$ \lor(\varphi,\psi)
例: $ \lor(p,q)や，$ \lor(p,\lnot(q))
$ \land(\varphi,\psi)
$ \to(\varphi,\psi)
$ \leftrightarrow(\varphi,\psi)
非常に見づらいので，
適当にカッコは省略する．
二項の関数記号については中置してよいとする
すなわち，$ \lor(p,\lnot(q))は$ p \lor \lnot qと書く．
注意
普通「$ \toは右結合とする」とするのが一般的だが，個人的に割と頻繁に間違えるためこれを採用せず，いちいち$ ()を入れることにする．
すなわち，ここでは全て左結合である．
変数の記号の集合として$ \mathbb{V} = \{p,q,r,\dots\}があるとする．
$ \mathbb{V}