数理論理学
出典: フリー百科事典『ウィキペディア（Wikipedia）』
数理論理学（すうりろんりがく）とは、論理を数学によって研究する学問である。記号論理学（きごうろんりがく）とも言う。
目次 |
[編集] 数理論理学の発祥
言葉を、代数学におけると同様に文字や記号の列で表して、その変換について研究するいわゆる記号論理学、数理論理学の発祥は、19世紀のジョージ・ブールによる「論理代数」、ゴットロープ・フレーゲによる「概念記法」に見ることができる。前者は命題論理、後者は述語論理の原型である。 数学自体を数学によって研究する数学基礎論は、数理論理学なしにはあり得ないものである。
たとえば数理論理学の一分科である命題論理では、「風が吹いた」という観念を文字 A で表し「桶屋が儲かる」という観念を 文字 B で表したとき、「風が吹いたならば桶屋が儲かる（風が吹けば桶屋が儲かる）」という観念を A ⇒ B で表したりする。従ってこの場合、記号 ⇒ は「ならば」という観念を表している。
[編集] 数理論理学の諸体系
数理論理学の体系は、論理式を構成する文法及び推論規則によって構成される。
上記文法及び推論規則の違いにより、命題論理・述語論理・様相論理等々の体系が存在する。
命題論理では、論理式は原子論理式および
- 論理式から論理記号によって論理式を作る文法
によって定められる。
具体的には、論理式 A, B, ... から論理記号 ∧, ∨, ¬, ⇒, によって、A ∧ B, A ∨ B, ¬A, A ⇒ Bなる論理式が作られる（x は項の一種である変項を表す）。 A ∧ B を論理積といい、A ∨ B を論理和といい、¬A を A の否定という。
述語論理では、さらに原子項、及び
- 項から関数記号によって項を作る文法
- 項から述語記号によって論理式を作る文法
によって定められる。
具体的にはn 個の項 x1, x2, ..., xn と n 変数関数記号 f によって項 f(x1, x2, ..., xn) が、 そして、n 変数述語記号 p によって論理式 p(x1, x2, ..., xn) が作られる (n = 0, 1, 2, ...) 。
さらに論理式A, B, ... から論理記号∀x, ∃x によって∀x A, ∃x Aなる論理式が作られる。
様相論理学では、さらに様相記号を用いる。
論理式から論理式を導き出す推論規則には、たとえば論理式 A と A ⇒ B とから B を導き出す推論規則がある。これはいわゆる三段論法である。
[編集] 数理論理学の諸分科
数理論理学の各分科での研究課題は、大きく証明論・意味論に分けられる
[編集] 証明論
証明論とは数学における証明を記号列と見なす立場（つまりシンタックスの立場）からの研究であり，20世紀初頭にヒルベルトにより数学の基礎付けを目的として創始された． この方面での重要な成果としては，ゲンツェンによる LK の基本定理，すなわち「式ＳがＬＫで証明可能ならば、Ｓは三段論法なしでも証明可能である」があげられる．この定理は「対偶や背理法のような間接証明法を用いて証明できる命題は、間接証明法を用いなくても証明できる」というようなことを一般化した，論理について成り立つ非常に美しい法則である．基本定理の応用としては，命題論理・述語論理の無矛盾性，そして命題論理の決定可能性がある。 また，この方面の研究としては同じくゲンツェンによる自然数論の無矛盾性の証明があげられる．
[編集] 意味論
意味論では、論理式で記述される命題の「意味」を、何らかの数学的対象に写像した上で、これらの数学的対象を研究する。 述語論理における意味の与え方の一例としては、実在物 (Entity) の全体の集合 E と真偽の集合 {0, 1} との直和を世界と定め、素項の集合から E への写像 f の各々に述語言語から世界への意味写像 f ∗ を対応させる規則を然るべく定め、 意味写像を用いて論理式の真偽の概念を定める等々の方法がある。 この方面での重要な成果としてはゲーデルの完全性定理があげられる。これはどのような意味の与え方によっても真となる述語論理の論理式と、述語論理の体系から証明可能となる論理式は、一致するというものである。
