評価について
期末の頃にレポートと試験を課す
試験で殆ど問題解けない人を救済するためにレポートは存在する
試験が何かconferenceか何かと被った時は要連絡
日本語と英語のを用意する
Logic and Software
ロジックをソフトウェアの視点から勉強する
Logicというのは一言で言うと
推論(reasonig)を研究する非常に古い分野
アリストテレス
議論する文章作るときの論理の組み立てを勉強する
この授業で勉強するのは更にその一分野の
Mathematical Logic
あるいは
Symbolic Logic
微妙にニュアンスが違う
論理学の一分野かつ数学の一分野
ただし数学科では勉強しないかも
数学(広い意味、
コンピュータサイエンスを含む)における
推論を数学的に研究する
対象が数学
整数論であれば整数を研究対象
解析だったら
複素関数を研究対象
数理論理学の場合は数学自体の推論を研究対象とする
ソフトウェア、もしくは
コンピュータサイエンスとの関わり
・
Turing Machine
→ Computability 計算可能性
Turing Machine で問題を解くことができる
連立方程式は計算可能
でも例えば整数係数不定方程式はわからない
計算という概念を定義しようとした
Turing Machine は計算機が生まれる以前からあった
・
ブール代数(命題論理)
↓
論理回路
デジタル回路の基礎
・Lambda Calculus
ラムダ計算
関数を基本とする体系
↓
関数型言語 Functional Programming Language
関数を値のように使うことができる
Scheme Haskell
Javaでも将来のヴァージョンでは関数
クロージャが入る
数理論理学とソフトウェアの
共通点としては
・数理論理学
数学の命題や証明を記号化する
論理学の基本となる手法
形式化 Formalize
・ソフトウェア
プログラムというのは
アルゴリズム、計算方法を形式化、記号化したもの
形式化するというのが肝
形式化、記号化が共通している
今日は 自然演繹 Natural Deduction の復習を行う
Natural Deduction とは何か
・Proof theory 証明論の一つ
証明論とは何か
数学において基本となるのは
・命題 Proposition
「〜である」という文章
これは true false(命題の意味)を判断し得る
・正しさ
・証明
正しさを導く過程
命題というのを形式化、記号化したものが論理式
A ::= P(t1,...,tn)
| (?A)
| (A∧B)
| (A∨B)
正しさを formalizeしたものが意味論 Semantics
例
((A->B)->A)->A これは
トートロジー Tautology
TT T T T T T
TF F T T T T
FT T ..
命題論理における semantics
証明を形式化する理論proof theory
・Natural Deduction
・Sequent Calculus シーケント計算
・Hilbert Style
一長一短ある
証明
仮定 assumptions
↓推論規則 inference rule
結論 conclution
仮定から
木構造のように導く
Natural deduction の嫌な所
1.仮定に関する水増し操作weakeningがあって気持ち悪い
[A] 仮定がAで結論がA
[ A ]
[----->I]
[B->A ] AとBを仮定をしてAを結論する
[ [A] ]
[---------]
[ B->A ]
[---------]
[A->(B->A)] 仮定なし 結論
2.
古典論理(
背理法)が難しい!
真偽値法で確かめれば簡単なのに
証明を書くのが難しい
例 ((A->B)->A)->A の証明
理由は対象性のなさ
T と F は
古典論理では対象
∧ ∨
?(A∧B)<->(?A)∨(?B)
?(∀xA)<->∃x(?A)
# Synmetric でない例がいろいろ
2つの嫌な所を改良したものが
Sequent Calculus
証明とは思えないくらい人工的なもの
証明をformalizeしたものが証明図
| |
正しさ semantics
これれらはどちらも正しさを定義している
これらの関連性を示す性質が
完全性completenessと健全性soundness
Aの証明がある
↓soundness ↑completeness
Aが正しい
命題論理は健全性も完全性も成り立つ
述語論理も成り立つが
自然数とか入れると成り立たなくなる
集合論では完全性は成り立たない
ZF
集合論 (普通の数学言語)
+C
選択公理 真でも偽でも良い
∀x∃y P(x,y)
↓
∃f∀x P(x,f(x))
すべてのベクトル空間に基底が存在する
(
Zornの
補題が…)