principle of duality

\lnot,\land,\lor以外の論理演算子を含まない論理式A,Bを任意に選び、Aの双対をA^\astで表し、Bの双対をB^\astで表す。このとき、AとBが論理的に同値ならば、A^\astとB^\astもまた論理的に同値である。

ある定理Aが得られたとき、Aの双対A*が成り立つことも自動的に得られること

ex. 「圏の終対象が存在すれば同型を除いて一意的である」がわかったとき、

自動的に「圏の始対称が存在すれば同型を除いて一意的である」が得られる

わざわざ双対側で定理の再確認が不要

一口で二度おいしい