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

命題論理の意味論

要約

これまで論理式は白丸と黒丸の記号列であり、演繹は記号列の操作であった。その真偽については何も述べられていない。この課はそれらに意味を与える。付値は各変数に二つの真理値、11（真）と 00（偽）のいずれかを割り当て、複雑さに関する再帰によって、ただ一つの条項だけを用いて、すべての論理式へ一意的に拡張される。その条項とは、(φ↓ψ)(\varphi \downarrow \psi) が値 11 をとるのは、φ\varphi と ψ\psi が値 00 をとるときであり、かつそのときに限る、というものである。この条項と公式の略記から、それ以上何も約定することなく、否定、選言、連言、含意、双条件、排他的選言の値が計算される。一致補題は、複雑さに関する帰納法で証明され、論理式の値がその変数の値だけに依存することを保証する。そこから、真理値表（行数は 2n2^n、変数は nn 個）は、無限に多くの付値がその論理式について言いうることのすべてを含むことが従う。これによって充足、恒真性、充足可能性、矛盾、偶然性が定義され、論理式 ⊤\top と ⊥\bot が固定され、恒真性を判定する問題が提起される。真理値表はこの問題を、変数の個数とともに指数関数的に増大するコストで解く。

学習目標

  1. 付値のもとでの論理式の真理値を、その再帰的な拡張によって計算し、公式の略記から各派生結合子の値を求める。
  2. 一致補題を複雑さに関する帰納法で証明し、それを用いて、2n2^n 行の真理値表が nn 個の変数をもつ論理式を調べるのになぜ十分なのかを説明する。
  3. 真理値表を列ごとに構成し、論理式を恒真、偶然式、矛盾式に、論理式の集合を充足可能または充足不能に分類する。その際、⊭φ\not\models \varphi を矛盾式と混同しない。
  4. 論理式を反駁する付値を探すことによってその恒真性を判定し、真理値表の方法のコストを変数の個数の関数として見積もる。

論理式の意味

言語の単元は、命題論理の言語の課で、二つの記号からなる記号列の集合を構成し、演繹の単元は、公理と規則によってある記号列から別の記号列を得る方法を教えた。どちらも真理については語らなかった。演繹体系は記号をその形に従って変形するのであり、自分の書いているものを理解しない機械のようなものである。しかし、この言語は言明を表すために構成されたのであり、自然言語の形式化の課はそれらに非形式的な読みを与えた。(φ↓ψ)(\varphi \downarrow \psi) が真であるのは φ\varphi と ψ\psi がともに偽であるときであり、他の結合子の読みはこれから得られた。意味論はこれらの読みを数学的な定義に変える。

二つの決定がその基礎にある。第一は二値原理である。真理値はちょうど二つあり、11（真）と 00（偽）と書かれ、各論理式は各状況においてそのいずれか一方をもつ。第二は真理関数性である。複合論理式の値はその成分の値だけに依存し、その内容には依存しない。したがって、変数の真偽がすべての論理式の真偽を決める。形式化の課は、この第二の決定の代償を示した（因果性、様相、時間は外に置かれる）。その見返りは、言語全体の意味論がただ一つの条項、すなわち原始結合子の条項から得られることである。

さらに注意すべきことに、この単元は全面的にメタ言語の中で作業する。「φ\varphi はしかじかの付値のもとで真である」や「φ\varphi はトートロジーである」といった主張は論理式ではなく、論理式についての数学的な言明であり、通常の推論によって、しばしば複雑さに関する帰納法によって証明される。それらは本コースの体系における演繹ではない。二つの世界の関係、すなわち導出可能なものはすべて真であり、この単元の厳密な意味で真なるものはすべて導出可能であるということは、メタ理論の単元の主題である。