形式論理と計算

形式論理は、議論の形式を、その議論が扱う主題から切り離します。構文は許容される式と証明を定義し、意味論は解釈と真理条件を与えます。両者を関連付けることで、証明体系が何を確立でき、計算モデルが何を決定できるかを正確に述べられます。

構文と演繹 #

形式言語は、記号のアルファベットと、整形式を定める形成規則から始まります。命題論理には命題変数と論理結合子が含まれます。第一階述語論理ではさらに、変数、関数記号、述語記号、一般的な定式化における等号、および量化子が加わります。

演繹体系には、次の要素も加わります。

公理: 導出なしに受け入れる式、または式を生成する公理図式
推論規則: 前提から結論を導く機械的なパターン

導出とは有限の列または木であり、その中の各式は、公理、仮定、または推論規則の結果です。記法 \(\Gamma \vdash \varphi\) は、\(\Gamma\) 内の仮定から式 \(\varphi\) を導出できることを意味します。ターンスタイルは構文を表します。証明検査器は、非論理記号の意味を判断せずに導出を検証できます。

モーダスポネンスは推論規則の一つです。

text

P -> Q
P
------
Q

ある式とその否定の両方を導出しない形式体系は、無矛盾です。無矛盾性は完全性とも、意図したモデルにおける選択済み公理の真理性とも異なります。

意味論、モデル、量化 #

命題論理の解釈は、各原子命題に true または false を割り当てます。その後、論理結合子が複合式の真偽を決定します。

式	真となる条件
\(P \land Q\)	両方のオペランドが真
\(P \lor Q\)	少なくとも一方のオペランドが真
\(P \rightarrow Q\)	\(P\) が偽、または \(Q\) が真
\(P \leftrightarrow Q\)	両方のオペランドの真理値が同じ

第一階意味論には、空でない領域と、その領域上での各定数記号、関数記号、述語記号の解釈が必要です。変数割当ては自由変数に値を与えます。量化子は領域全体を範囲とします。

\(\forall x\, P(x)\) は、領域のすべての要素について P が成り立つとき真です。
\(\exists x\, P(x)\) は、領域の少なくとも一つの要素について P が成り立つとき真です。

たとえば、\(\forall x (Human(x) \rightarrow Mortal(x))\) は、人間が存在することを主張していません。\(\exists x\, Human(x)\) と組み合わせると、 \(\exists x\, Mortal(x)\) が導かれます。

式の集合のモデルは、それらすべてを真にします。記法 \(\Gamma \models \varphi\) は、\(\Gamma\) のすべてのモデルが \(\varphi\) のモデルでもあることを意味します。二重ターンスタイルは、導出の存在ではなく意味論的帰結を表します。

妥当性、真理性、健全性、完全性 #

真理性は、ある解釈のもとでの式に属する性質です。妥当性は、複数の解釈にわたる式または議論に属する性質です。

すべての解釈で真となる式は、論理的に妥当です。
すべての前提が真で結論が偽となる解釈が存在しない議論は、妥当です。
健全な議論は妥当であり、かつ意図した解釈で真となる前提を持ちます。

したがって、妥当な議論でも、前提と結論がともに偽の場合があります。妥当性が保証するのは、その議論形式によって真の前提から偽の結論が導かれないことだけです。

証明体系の性質は、導出可能性と意味論的帰結を結び付けます。

text

soundness:    if Gamma |- phi, then Gamma |= phi
completeness: if Gamma |= phi, then Gamma |- phi

健全性は、規則によって妥当でない意味論的帰結が導出されないことを示します。完全性は、その論理で表現可能なすべての意味論的帰結に導出が存在することを示します。古典命題論理と第一階述語論理には、健全かつ完全な証明体系があります。第一階述語論理に関するゲーデルの完全性定理を、彼の不完全性定理と混同してはなりません。十分な表現力を持ち、無矛盾で、実効的に公理化された算術理論は、意図した算術的解釈で真となるすべての命題を証明できません。

有限個の変数を持つ式には有限個の付値しかないため、真理値表によって命題論理の妥当性を決定できます。一方、モデルが任意の大きさの領域を持ち得るため、対応する有限の表では第一階述語論理の妥当性を決定できません。

計算モデルとしてのチューリング機械 #

決定性単一テープ・チューリング機械は、次の要素で規定できます。

開始状態と停止状態を含む、有限の状態集合
空白記号を含む、有限のテープ・アルファベット
数学的モデルにおいて無限に延長可能なテープ
一つのセルを読み書きするヘッド
現在の状態と読み取った記号を、新しい状態、記号、およびヘッドの移動に写像する遷移関数

構成は、制御状態、テープ内容、およびヘッド位置を記録します。遷移関数を一度適用すると、ある構成から次の構成へ移ります。機械は、ある言語に属する文字列だけを受理するとき、その言語を認識します。さらに、すべての入力について停止して答えを返すとき、その言語を決定します。

計算可能性と決定不能性 #

関数の定義域内のすべての入力について、チューリング機械が結果を生成して停止するなら、その関数はチューリング計算可能です。ラムダ計算やレジスター機械を含む他の厳密なモデルも、同じ関数のクラスを計算します。チャーチ＝チューリングのテーゼは、そのクラスを実効的に計算可能な関数と同一視します。このテーゼは数学的モデルと非形式的な概念を結び付けるため、モデル内部の定理ではありません。

可算個の機械によってアルゴリズムを記述できますが、有限アルファベット上の言語でさえ非可算集合を形成します。したがって、どの機械にも決定できない言語が存在します。停止問題は構成的な例です。符号化された任意の機械と入力について、その計算が停止するかどうかを判定できるチューリング機械は存在しません。標準的な対角線論法では、そのような判定器が存在すると仮定し、自身の符号化に対する判定器の結果と矛盾する機械を構成して、仮定を棄却します。

決定不能であることは、すべての個別事例に答えられないことを意味しません。静的解析、定理証明器、および型システムは、言語を制限する、保守的な回答を許容する、注釈を要求する、またはすべての意味論的性質を決定せずに終了するため、依然として有用です。