しんのすけWiki
情報科学における論理
最終更新:
shinsa
-
view
情報科学における論理
テキストはこちら。
情報数学セミナー 情報科学における論理 小野 寛晰著 (株)日本評論社 ISBN 4-535-60814-8
目次
内容
第1章 命題論理
1. 形式化ということ
対象言語とメタ言語の区別をする必要がある
2. 命題と論理式
命題および論理結合子、論理式、結合子の優先順位の定義
3. 論理式と真偽
真理値表の導入とトートロジーを定義する。また、部分論理式、付値、充足可能性の定義を行う。
- 与えられた論理式Aが恒真かどうかは決定可能である。(述語論理の場合とは異なる)
4. 論理的に同値な論理式
同値記号を導入。基本的なトートロジーの紹介
論理的同値性の定義。論理式の構成に関する帰納法
論理的同値性の定義。論理式の構成に関する帰納法
5. 標準形
論理和標準形 (DNF) 及び論理積標準形 (CNF)
- 標準形の存在定理
- 論理結合子の制限と存在定理 (論理和と「ならば」のみを持つ等価な論理式が存在する)
6. 形式体系における証明
シンタクスとセマンティクス。
形式体系LK (Gentzenによる、古典命題論理に対するsequent計算) の導入
形式体系LK (Gentzenによる、古典命題論理に対するsequent計算) の導入
- 式 (sequent) は Γ→Δ の形をとる (それぞれ論理式の列)。
- 公理 (始式) は A→A
- 推論規則は、各論理結合子に対する導入公理と除去公理、および構造に関するものからなる。
主論理式、副論理式
LKの証明図の定義、終式、証明可能性
LKの証明図の定義、終式、証明可能性
7. トートロジーと証明可能性
トートロジーの概念を式にまで拡張。健全性 (soundness) と完全性 (completeness)
- (soundness) LKで証明可能な式はトートロジーである
- (complete) LKのトートロジーはLKで証明可能である
- (LKの完全性定理) LKにおいて証明可能であることとトートロジーであることは同値である。
ここでは一般のcut除去定理を用いない。式の分解と呼ばれる概念を用いて、完全性においてcutを持たない証明が存在することを示している。
- LKの証明可能性は決定可能である。
8. cut除去定理
ここでは7.の内容から系として得られるものである。通常は証明木の構造を変換することによりこれを示す。
- subformula property
- 規約の概念を用いた、証明可能性の決定方法
双対性と双対定理
ノート: Hilbert流の形式体系
ノート: Hilbert流の形式体系
9. ブール代数
ブール代数、束の定義。双対擬補元
Hasse diagram
ブール値付値
Hasse diagram
ブール値付値
- トートロジーであることと、ブール値付値が最大元であることは同値である。
問題
- ウカシェビッチの三値論理
- クレイグの補完定理
第2章 述語論理
1. 一階の述語論理
命題論理から述語論理へ、変数と定数、量化記号
2. 述語論理の論理式
言語を定義することについて
項、論理式の定義、束縛変数と自由変数、変数の出現 (occurrence)、閉じた式、閉包、項の代入、同時代入、部分論理式
項、論理式の定義、束縛変数と自由変数、変数の出現 (occurrence)、閉じた式、閉包、項の代入、同時代入、部分論理式
3. 構造
述語論理のセマンティクスを定義する。
対象領域、解釈、構造
意味付けの定義。ここで変数の意味づけを行うために取っている方法はちょっと不自然
対象領域、解釈、構造
意味付けの定義。ここで変数の意味づけを行うために取っている方法はちょっと不自然
4. 恒真な論理式
恒真な論理式の定義、トートロジーの例を紹介。充足可能性の定義。
冠頭標準形の定義と存在定理
論理的同値
冠頭標準形の定義と存在定理
論理的同値
5. 古典述語論理の形式体系LK
命題論理のLKに量化記号に対する推論規則を追加したもの。
変数条件、固有変数の定義
変数条件、固有変数の定義
- cut除去定理
- 述語論理では証明可能性は決定不能である (Church)
ノート: Hilbert流の形式体系
6. 完全性定理
- Gödelの完全性定理。述語論理のLKにおいて、恒真であることと証明可能であることとは同値である。
証明は略されている。命題論理と同様に証明できる?
なお、5.にある通り完全性は成り立つが、恒真であるか (=証明可能であるか) は決定可能でないことに注意。
なお、5.にある通り完全性は成り立つが、恒真であるか (=証明可能であるか) は決定可能でないことに注意。
形式理論の定義、矛盾、無矛盾の定義