数理論理学
出典: Wikipedio
|
数理論理学(すうりろんりがく)とは、論理を数学によって研究する学問である。記号論理学(きごうろんりがく)とも言う。
目次 |
数理論理学の発祥
言葉を、代数学におけると同様に文字や記号の列で表して、その変換について研究するいわゆる記号論理学、数理論理学の発祥は、19世紀のジョージ・ブールによる「論理代数」、ゴットロープ・フレーゲの書『概念記法』に見ることができる。前者は命題論理、後者は述語論理の原型である。数学自体を数学によって研究する数学基礎論は、数理論理学なしにはあり得ないものである。
たとえば数理論理学の一分科である命題論理では、「風が吹いた」という観念を文字 A で表し「桶屋が儲かる」という観念を 文字 B で表したとき、「風が吹いたならば桶屋が儲かる(風が吹けば桶屋が儲かる)」という観念を A ⇒ B などと表す。ここに、記号 ⇒ は「前の概念が正しければ後ろの概念も正しい」ということを表し、A ⇒ B を「A ならば B」と読む。
数理論理学の諸体系
数理論理学の体系は、論理式を構成する文法及び推論規則によって構成される。
上記文法及び推論規則の違いにより、命題論理・述語論理・様相論理等々の体系が存在する。
命題論理では、論理式は原子論理式および
- 論理式から論理記号によって論理式を作る文法
によって定められる。
具体的には、論理式 A, B, ... から論理記号 ∧, ∨, ¬, ⇒ によって、A ∧ B, A ∨ B, ¬A, A ⇒ B なる論理式が作られる(x は項の一種である変項を表す)。A ∧ B は論理積、A ∨ B を論理和、¬A を A の否定、A ⇒ B を論理包含という。なお、記号は研究者・流派によって、たとえば ⇒ のほかに →, ⊃ や、 ¬ のほかに ∼ など異なるものが用いられることがあるが、いずれも同じものである。⇒ と → を使い分ける流儀もある。
述語論理では、さらに原子項、及び
- 項から関数記号によって項を作る文法
- 項から述語記号によって論理式を作る文法
によって定められる。
具体的には 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 を導くことができる。これは三段論法の一種である。三段論法とは、F → G, G → H から F → H を導く推論規則で、より正確には
- ∀ x {(G(x) → H(x)) ∧ (F(x) → G(x))} ⇒ F(x) → H(x)
すなわち、どんな x を取っても、F ならば G、かつ G ならば H が成り立つとき、F ならば H である、ということである。これは集合を用いれば
- ({x|G(x)} ⊆ {x|H(x)}) ∧ ({x|F(x)} ⊆ {x|G(x)}) ⇒ {x|F(x)} ⊆ {x|H(x)}
と表せる。
数理論理学の諸分科
数理論理学の各分科での研究課題は、大きく証明論・意味論に分けられる。
証明論
Template:Main 証明論とは数学における証明を記号列と見なす立場(つまり syntax の立場)からの研究であり、20世紀初頭にヒルベルトにより数学の基礎付けを目的として創始された。この方面での重要な成果としては、ゲンツェンによる LK の基本定理、すなわち「式 S が LK で provable ならば、S は LK で三段論法なしでも provable である」があげられる。この定理は「対偶や背理法のような間接証明法を用いて証明できる命題は、間接証明法を用いなくても証明できる」というようなことを一般化した、論理について成り立つ非常に美しい法則である。基本定理の応用としては、命題論理・述語論理の無矛盾性、そして命題論理の決定可能性がある。また、この方面の研究としては同じくゲンツェンによる自然数論の無矛盾性の証明があげられる。
意味論
意味論では、論理式で記述される命題の「意味」を、何らかの数学的対象に写像した上で、これらの数学的対象を研究する。述語論理における意味の与え方の一例としては、実在物 (Entity) の全体の集合 E と真偽の集合 {0, 1} との直和を世界と定め、素項の集合から E への写像 f の各々に述語言語から世界への意味写像 f ∗ を対応させる規則を然るべく定め、 意味写像を用いて論理式の真偽の概念を定める等々の方法がある。この方面での重要な成果としてはゲーデルの完全性定理があげられる。これはどのような意味の与え方によっても真となる述語論理の論理式と、述語論理の体系から provable となる論理式は、一致するというものである。
関連項目
Template:数学ar:منطق رياضي
az:Riyazi məntiq
be:Матэматычная логіка
be-x-old:Матэматычная лёгіка
bg:Математическа логика
bs:Matematička logika
ca:Lògica matemàtica
cs:Matematická logika
de:Mathematische Logik
el:Μαθηματική λογική
en:Mathematical logic
eo:Matematika logiko
es:Lógica matemática
et:Matemaatiline loogika
fa:منطق ریاضی
fr:Logique mathématique
gd:Rianas matamataigeach
he:לוגיקה מתמטית
hi:गणितीय तर्कशास्त्र
hr:Matematička logika
hu:Matematikai logika
id:Logika matematika
io:Matematikala logiko
it:Logica matematica
ka:მათემატიკური ლოგიკა
ko:수리논리학
lij:Logica Matematica
mk:Математичка логика
nl:Wiskundige logica
nn:Matematisk logikk
no:Predikatslogikk
pl:Logika matematyczna
ro:Logică matematică
ru:Математическая логика
sh:Matematička logika
sk:Matematická logika
sl:Matematična logika
sq:Logjika matematikore
sr:Математичка логика
sv:Matematisk logik
tg:Мантиқи риёзӣ
th:คณิตตรรกศาสตร์
tl:Matematikal na lohika
tr:Matematiksel mantık
uk:Математична логіка
ur:ریاضیاتی منطق
zh:数理逻辑
zh-yue:數學邏輯