Skinerrian's blog

論理学・哲学・科学史・社会学などに興味があるので、その方面のことを書きます。更新は不定期。

三値論理

ウカシェーヴィチの三値論理L3では演繹定理は成り立たない。例えば

  • A∧¬A ├ B

はなりたつが

  • ├ (A∧¬A)→B

は成り立たない。Aに真理値#を割り当て、Bに真理値Fを割り当てると反例になる*1

A→(B→A)と[A→(B→C)]→[(A→B)→(A→C)]があれば、演繹定理を導くのに十分なので、どちらかがL3では成り立たないはずである。実際、2つ目はL3ではトートロジーではない。AとBに#を割り当てて、CにFを割り当てると反例。

三値論理L3には、これ以外にも古典論理には見られない性質が沢山ある。排中律矛盾律が成り立たないことはよく知られているが、

縮約(contraction)
[A→(A→B)]→(A→B)

が成り立たないというのも面白い。縮約が成り立たないというと線型論理が有名だけど、縮約規則を持たない論理学は三値論理が歴史上初めてだという。

排中律トートロジーとしない点で、三値論理は直観主義論理と共通するが、直観主義では¬¬(A∧¬A)が成り立つ。しかし、三値論理では排中律の否定である¬(A∧¬A)も充足可能である。直観主義論理を多値論理の一種と見なすことはできない。

Postscript (2014/2/23)

「縮約が成り立たないというと線型論理が有名」とか書いたけど、他の例も挙げられるかな。古典論理のシークエント計算LKから縮約規則を取り除いたものをグリシン論理という。また、直観主義論理のシークエント計算LJから縮約規則を取り除いたものをBCK論理という*2。これらの論理はよく研究されてるっぽい。

ところで、上の記事ではそもそもなんで縮約規則が成り立たないことに注目するのかをまったく説明してないが、一つの眼目は、ラッセルのパラドクスの診断にある。A≡¬Aから矛盾を導出するには縮約規則が必要だから。んで、縮約規則を取り除いた論理の研究者は、縮約を除くことでパラドクスが生じるのを避けつつ、それでも証明能力ができるだけ弱くならないようにすることで、数学の基礎のオルタナティブを提案しようとしてるのだと思う。

*1:妥当な推論が保存すべき指示値(designated value)は、真のみとする。

*2:B, C, Kはコンビネータ項に対応する。

広告を非表示にする