コンテンツへスキップ
Topos Uranos
日本語

形式的演繹体系

要約

この課は、前の単元の言語を証明のための道具に変える。形式的演繹体系とは何か（一つの言語、いくつかの公理図式、いくつかの推論規則）を定義し、本コースが扱う二つの体系のうち最初のもの、すなわちウカシェヴィチの体系を紹介する。それは三つの公理図式と、唯一の規則としてのモーダス・ポネンスからなる。前提集合からの演繹、定理、および関係 Γ⊢φ\Gamma \vdash \varphi を厳密に定義し、⊢(φ→φ)\vdash (\varphi \rightarrow \varphi) を五行で導き、演繹の構造的性質、すなわち反射性、単調性、演繹どうしのモーダス・ポネンス、カット、有限性を証明する。次に、行数に関する累積帰納法によって演繹定理とその逆を証明する。これらにより、演繹についての演繹を用いて推論できるようになる。さらに証明可能な同値を定義する。最後に、真理値に頼ることなく、否定論理和を唯一の結合子とする言語におけるこの体系の限界を確立する。論理式に関する再帰で計算される 00 と 11 の標識は、ウカシェヴィチの公理とモーダス・ポネンスによって保たれ、導かれるべきいくつかの論理式が導かれないこと、さらに (v1↓v2)(v_{1} \downarrow v_{2}) から (¬¬v1↓v2)(\neg\neg v_{1} \downarrow v_{2}) へ移ることさえできないことを証明する。ここから第二の規則、すなわち二重否定の置換の必要が生じ、次の課はそれによって体系を完成させる。

学習目標

  1. 公理図式 A1、A2、A3 の代入例を見分け、論理式の並びが前提集合からの演繹であるかどうかを判定する。
  2. ウカシェヴィチの体系において、公理、前提、モーダス・ポネンスを用いて演繹を構成し、反射性、単調性、カット、演繹定理とその逆を用いて演繹についての演繹を構成する。
  3. 演繹の構造的性質と演繹定理を、行数に関する累積帰納法によって証明する。
  4. 証明可能な同値を確立し、証明可能な同値が反射的、対称的、推移的であることを用いる。
  5. 公理とモーダス・ポネンスが保つ標識によって論理式が導出可能でないことを証明し、それを用いて、ただ一つの結合子をもつ言語におけるウカシェヴィチの体系の限界と、第二の規則が必要な理由を説明する。

形式的演繹体系とは何か

前の単元は一つの言語を構成した。すなわち、白丸と黒丸のどの記号列が論理式であるかを決めたのであり、それ以上のことはしていない。しかし、言語はそれだけでは何も主張せず、何も証明しない。証明するには、さらに出発点と前進の仕方が必要である。したがって、形式的演繹体系は三つの構成要素からなる。論理式を定める形式言語、証明なしに認められる論理式である公理の集合、そして、すでに書かれた他の論理式からどの論理式を書いてよいかを述べる推論規則の集合である。決定的なのは、この三つがいずれも純粋に構文的だということである。ある論理式が公理であること、あるいはある規則が正しく適用されたことを確かめるには、記号列を見るだけでよく、それが何を意味するかを問う必要はない。そうであるならば、形式体系における証明は記号ごとに機械的に検査でき、その価値のすべてはこの可能性にある。

最初に注意しておくべきことは、ここでの公理は、この語の古い用法におけるような「自明な真理」ではなく、出発点として選ばれた論理式だということである。その選択が適切かどうか（公理が意味論の明らかにする意味で真であるかどうか、また導かれるべきものをすべて導くのに十分であるかどうか）は体系についての問いであり、直観ではなく体系についての定理によって答えられる。メタ理論の単元がこれに答え、この課の最後の節は、この問いが無用ではないことを示す。

公理図式と代入例

命題論理の体系は、公理が無限にあるので、それを一つずつ述べるのではなく、図式によって述べる。図式とは、(φ→(ψ→φ))(\varphi \rightarrow (\psi \rightarrow \varphi)) のように、メタ変数で書かれたメタ言語の表現である。図式は論理式ではなく、鋳型である。図式の代入例とは、各メタ変数に論理式を一様に代入して得られる論理式である。すなわち、同じメタ変数のすべての出現には同じ論理式が代入されるが、異なるメタ変数が同じ論理式を受け取っても、異なる論理式を受け取ってもよい。

例図式の代入例

φ:=v1\varphi := v_{1}、ψ:=¬v2\psi := \neg v_{2} とすると、図式 (φ→(ψ→φ))(\varphi \rightarrow (\psi \rightarrow \varphi)) は代入例 (v1→(¬v2→v1))(v_{1} \rightarrow (\neg v_{2} \rightarrow v_{1})) を与える。φ:=(v1↓v2)\varphi := (v_{1} \downarrow v_{2})、ψ:=(v1↓v2)\psi := (v_{1} \downarrow v_{2}) とすると、((v1↓v2)→((v1↓v2)→(v1↓v2)))((v_{1} \downarrow v_{2}) \rightarrow ((v_{1} \downarrow v_{2}) \rightarrow (v_{1} \downarrow v_{2}))) を与える。二つのメタ変数が同じ論理式を受け取ることを妨げるものは何もないからである。これに対して、(v1→(v2→v3))(v_{1} \rightarrow (v_{2} \rightarrow v_{3})) はこの図式の代入例ではない。φ\varphi の最初の出現と最後の出現が異なる論理式を受け取ることになり、代入が一様でなくなるからである。各代入例は、略記を展開すれば白丸と黒丸の記号列である。これに対して図式はメタ言語の中にしか存在しない。