|
数理論理 |
|
mathematical logic |
数理論理は, 記号化した論理を数学的手法を用いて研究する学問であり, 記号論理とも呼ばれる．形式的な記号列としての論理式や証明の構文を定義し, その性質を研究する分野を構文論という．一方, 記号列に, 集合や関数, ブール代数などの数学的構造への対応を与える研究を意味論という．構文論は, 計算機での記号処理の対象となり自動証明などに応用される．一方, 意味論は, 単なる記号列として定義された論理体系への理解を深める道具となる． 数理論理は単一の体系ではなく, 目的, 用途に応じて多様な体系が考案されている．最も基礎となるのは命題論理である．命題は真か偽のいずれかを表す記号列であり, 基礎となる命題(原始命題)を, 「かつ」「または」「ならば」「〜でない」という論理記号で結んだ表現である．命題論理では「任意の個体について〜である」や「ある個体について〜である」という表現はできないため, これらを追加した体系を1階述語論理という．さらに, 「任意の論理式について〜である」などの表現が許される体系を2階述語論理という．同様にさらに高階の述語論理を考えることができ, 総称して高階論理という．1階述語論理の範囲内で多くの事象の記述ができるため, 1階述語論理が種々の応用の基礎となっている．一方, 非単調推論や多相型プログラミング言語に対応した論理など高階論理が必要な場面も知られている． 日常的推論や数学での推論で用いられる通常の論理を古典論理と呼び, 古典論理以外の論理を非古典論理と総称する．非古典論理には, 多値論理, 直観主義論理, 様相論理, 内包論理, 線形論理などがある．多値論理は, 命題が真・偽以外の値をとりうる論理であり, プログラムの実行が止まらない未定義状態などを表すのに用いられる．直観主義論理は, 排中律(A または A でない)が必ずしも成立しないよう古典論理を弱めた論理である．直観主義論理は構成的論理とも呼ばれ, その証明と一種の関数型プログラミング言語のプログラムは密接に対応している．型理論はプログラミング言語の型の理論の一般化であるが, 同時に直観主義論理の体系ともみなすことができる．様相論理は, 「〜であるはずだ」(必然)や「〜かもしれない」(可能)など, 様相を表す記号を導入した論理である．様相論理には極めて多くの種類があり, 種々の計算機科学分野に応用をもっている．内包論理は, 命題の真・偽がその命題の文脈に依存するような論理の総称であり, 様相論理もその一種とみなすことができる．近年では, 線形論理が理論・応用の両面から注目を集めている．線形論理では, 仮定した論理式はちょうど1回だけ使われなければいけないため, 「 A ならば A かつ A 」は成立しない．線形論理は論理式を有限の資源を表すと解釈できるため, 資源の論理とも呼ばれる． 数理論理と計算機科学のかかわりには, 数理論理に基づいた計算機プログラムの検証体系, 数理論理で記述された定理の自動証明などがある．前者の代表例がホーア論理であり, 後者の代表例は導出原理である．導出原理を一種の計算とみなす立場から論理型プログラミング言語 Prolog が発生した． (古川・佐藤) |