VI. 論理の形式化
論理の形式化においては，論理式の意味には立ち入らず，証明・演繹の
過程を「推論規則」と呼ばれる論理式の変形操作に還元する．また，
推論規則を適用する出発点として，「公理系」と呼ばれるいくつかの
論理式を用意する．この章ではこのような形式化の考え方を紹介する．
目次
- 1. 形式化の考え方
- 2. 形式的証明・演繹の例
- 3. ヒルベルト流の形式化
総目次に戻る
1. 形式化の考え方
以下では論理体系の形式化の考え方を概説する．なお，ここでは
論理体系として古典論理を想定しているが，他の論理体系にも
同様の考え方が当てはまる．
1.1 論理体系に対する二通りの取り扱い
論理式はあくまで記号の並びである．その意味では文字で書かれた
通常の言語に似ている．その言語が未知のものであれば，書かれた
文字の並びが何を意味するかはもちろんわからない．記号・文字
などの「シンボル」の意味解釈とは，要するに，「実体」との
対応付けを与えることである．通常の言語ではその代わりに
辞書が用いられることも多いが，これは既知の言語（実体との
対応関係が既に明確になっている）を仲介にして実体との
対応付けを与えるものであり，本質的な違いはない．前章までは
古典論理の意味論的な取り扱いを考えてきたが，そこでの「実体」
は T,F という真理値やさまざまな集合の要素・函数・述語である．
そしてそのような意味解釈に基づいて恒真式・論理的同値性・充足関係
などの概念が導入されたわけである．
このような意味論（semantics）的取り扱いとは対照的に，
論理体系を形式的体系（formal system）として扱う方法
（論理の形式化）もある．これは論理式の意味自体には立ち入らず，
あくまで記号の並びの「パターン」に注目して議論を進めるものであり，
言語学との類似では構文論（syntax）の立場に立つということ
ができる．
これらはいわば相補的なものであるが，どちらかと言えば，
形式的体系としての取り扱いの方がより根元的な捉え方である．
また「効率」の点でも形式的取り扱いには利点がある．
たとえば論理式の恒真性を判定する問題を考えてみよう．恒真性を
定義通りに確かめようとすれば，あらゆる値割り当てや解釈に対して
真理値を調べることになるが，これは効率の点で問題があり，
少なくとも計算機向きではない（命題記号がn個あれば，
可能な真理値割り当ては2n通りあるから，
n が増えれば確かめるべき可能性は指数函数的に増加する）．
実際にはもっと効率のよい方法がいろいろと工夫されている．
そのような方法を大別すれば，場合分けを確実かつ無駄の少ない
手順で実行するもの（たとえば「タブロー法」と呼ばれるものなど）と，
論理式をある手順に従って変形して行くもの
（必ずしも同値変形とは限らない）の二通りに分けられる．
この「論理式の変形」という考え方が実は形式化につながる鍵なのである．
「論理式の変形」は一種の「計算」であるから，論理を「計算」
として定式化したものが形式的体系である，と言ってもよい．
実際，命題論理や述語論理の形式的体系は「命題計算」や
「述語計算」と呼ばれることもある．
1.2 公理系と推論規則
論理の形式的体系は公理系（axioms）と呼ばれる論理式の集合
（空の場合もある）と推論規則（inference rules）と呼ばれる
論理式の変形規則からなる．形式化された論理体系では論理式に対して
推論規則に従う変形を繰り返すことによって証明を行う．
たとえばヒルベルト（Hilbert）流の形式化と呼ばれるものでは
- (A1) φ→(ψ→φ)
- (A2) (φ→(ψ→χ))→((φ→ψ)→(φ→χ))
- (A3) (¬φ→¬ψ)→(ψ→φ)
という三つの形の論理式（φ，ψ，χは任意の論理式）を命題論理の
公理系に採用する．またゲンツェン（Gentzen）の「自然演繹」と呼ばれる
形式化では古典論理の公理系として排中律（law of excluded middle）
- (LEM) φ∨¬φ
（ここでもφは任意の論理式）を採用する．なお，これらの公理系は
公理の「パターン」を提示したものであり，パターンは有限個であるが
公理自体は（φ，ψ，χなどが任意の論理式として選べるから）無限個
あることになる．
推論規則は一般に
というように表記される．ここでφ1, …,φn, ψは
特定の形をした論理式であり，横線の上側の論理式の組（前提）から
横線の下側の論理式（帰結）を導出することを意味する．
たとえば MP（modus ponens）と呼ばれる推論規則は
となる．公理系と同様，これもまた特定の論理式の間の関係という
よりはそのような関係の「パターン」である．ヒルベルト流の
形式化では推論規則としてMPのみを用いる．他方，ゲンツェン流の
形式化は推論規則を多数用意するのが特徴である．
意味論的に言えば，推論規則は前提が真のとき帰結も真である
（言い換えれば
φ1∧…∧φn |= ψ
が成り立つ）ようなものでなければならない．そのような推論規則を
妥当（valid）な推論規則という．MPは言うまでもなく妥当な
推論規則である．
1.3 形式的な証明・演繹
推論規則を繰り返し適用することによって論理式を変形して行く
ことを証明（proof）あるいは演繹（deduction）
という．
与えられた論理式の集合 Γ
= {φ1, …,φn} から出発して推論規則の
反復適用によって論理式 ψ が導出されること（演繹関係）を
Γ |- ψ
とあらわす．このとき Γ を前提，ψ を帰結という．
ただし，前述のような公理は前提中に明記せず省略するのが普通である．
特に，ψ が公理系だけから出発して導出できることを
|- ψ
とあらわす．このとき，ψ はこの形式的体系の
定理（theorem）である，という．
【注意】
- 「証明」と「演繹」はほとんど同じ意味で用いられる
言葉であるが，「証明」の方が公理から出発して定理を導く，
という意味合いが強いのに対して，「演繹」の方は一般の論理式
（の集合）から別の論理式を導くことを指すことが多いようである．
また「推論（inference）」という言葉を用いることもある．
- 一般には（特に述語論理の場合），前述の論理的公理以外の
論理式を「非論理的公理系」として用意して，
これらも含めた形式的体系を考える（たとえばペアノ算術の
公理系によって自然数論を形式的体系として定式化する）．
非論理的公理系Ｔも含めた公理系から論理式ψが導出されることを
Ｔ |- ψ
とあらわし，ψをこの形式的体系における定理という．
このように論理的公理を明示しないのは，この種の議論では
論理的枠組は共通のもの（たとえば述語論理）に選び，その中で
さまざまな非論理的公理系を比較しながら考えることが多い
からである．
1.4 形式的体系の健全性と完全性
Γ |- ψ という演繹において，推論規則が妥当，かつ前提がすべて恒真式
であれば，帰結 ψ も恒真式である．特に，推論規則が妥当で公理系が
すべて恒真式であれば，そこから導かれる定理もすべて恒真式である．つまり
|- ψ ならば |= ψ
ということがわかる．この性質（いわば「証明できることは正しい」）
をもつ形式的体系は健全（sound）である，という．これは
形式化された論理が最低限満たさなければならない性質と言えよう．
他方，
|= ψ ならば |- ψ
という性質（いわば「正しいことは証明できる」）をもつとき
形式的体系は完全（complete）であるという．これは
公理系と推論規則が十分に強力であることを意味するものである．
これは望ましい性質であるが，形式的体系として必要不可欠と
いうわけではない．実際には，今後紹介して行くような命題論理や
述語論理（正確に言えば１階の述語論理）の形式化は完全性をもつ．
【注意】
- 論理式の意味解釈が異なれば恒真性や完全性の意味も違ってくる．
その例は「直観主義論理」である．そこでは古典論理の２値真理値集合
{T,F} とは異なる真理値集合（ハイティング代数）による意味解釈を行う．
直観主義論理の形式化として後で触れる「NJ」や「LJ」があるが，
これらはハイティング代数による意味解釈のもとで完全性をもつ
ということが知られている．
- 述語論理の場合には，任意の非論理的公理系Ｔに対して，
より強い形での健全性
Ｔ|-ψ ならば Ｔ|= ψ
および完全性
Ｔ|= ψ ならば Ｔ|- ψ
も成立する．
- ゲーデルの「不完全性定理」が扱う（不）完全性は
ここで言う完全性とは異質の概念であり，混同してはならない．
ややこしいことに，ヒルベルト流の形式化が上の意味で完全性を
もつことを初めて証明したのも実はゲーデルであり，その結果を
「ゲーデルの完全性定理」という．このようにゲーデルは
「完全性定理」と「不完全性定理」の両方を証明したわけだが，
それらは内容的に異質のものであり，互いに矛盾するものではない．
1.5 代表的な形式的体系
古典論理（命題論理および述語論理）の形式化として
代表的なものには
- ヒルベルト流の形式化
- 自然演繹（NK）
- シークェント計算（LK）
がある．自然演繹とシークェント計算はゲンツェンが与えたものである．
あとで紹介するように，ヒルベルト流の形式的体系は
あまりわかりやすいものではない．自然演繹は数学で用いられる
推論をそのまま推論規則として取り入れていて，文字どおり「自然」
でわかりやすい．他方，自然演繹では前提と帰結以外に「仮定」というもの
（これは前提の一種だが，本来の前提と違ってあとで消してしまう）
があるため，形式化としては若干問題がある．そのような問題点を
改善したのがシークェント計算であり，自然演繹と比べて形式的体系
としてより望ましい性質を備えている．ちなみに，NK, LK の「K」は
ドイツ語のKalkuel（計算）の頭文字であり，これらが文字どおり論理の
「計算」化を意識したものであることがわかる．
NKとLKを少し修正することによって直観主義論理の形式的体系（NJおよびLJ）
が得られる．ここでは排中律φ∨¬φが一般には成立しない．
ヒルベルト流の形式化は公理系に排中律が内在しているので，
直観主義論理をヒルベルト流に変更することは難しい．
自然演繹は公理系として排中律しか残していないので，
それを除去する（つまり公理を一切置かない）ことによって
ただちに直観主義論理の形式的体系に変更することができる．
シークェント計算では計算対象のシークェント
（これは前提と帰結を組にしたようなものである）
の形に制約を設けることによって直観主義論理を実現している．
今日では古典論理や直観主義論理以外にも様相論理，線形論理など
さまざまな論理体系が考えられているが，その形式化は上に述べた
古典論理の三通りの形式化のいずれかの流儀を踏襲したものが多い．
これらの形式的体系に基づく証明・演繹をそのまま計算機上で
実行することは難しいので，論理式や推論規則を制限した論理体系
も考案されている．「導出原理」（resolution principle）はその
一例である．このように制限された形式的体系はPrologなどの
計算機上の論理プログラムの実行系や定理の自動証明の問題などに
応用されている．
2. 形式的証明・演繹の例
ここでは推論規則による推論・演繹の考え方を簡単な例で
説明する．本格的な例は個々の形式的体系の説明の中で
示すことにする．
2.1 ∧に関する例
連言∧に関して「∧導入」および「∧除去」と呼ばれる次のような
推論規則を考えてみよう（φ，ψは任意の論理式とする）．
φ ψ
φ∧ψ |
（∧導入） |
|
φ∧ψ
φ |
（∧除去） |
|
φ∧ψ
ψ |
（∧除去） |
これらはゲンツェンの自然演繹の推論規則から借りてきた
ものであるが，その妥当性は明らかだろう．∧除去には∧の
左側の論理式を残すものと右側を残すものの二種類があることに
注意されたい．
これを使って
- φ∧ψ |- ψ∧φ
となることを確かめよう．これは次のような形式的演繹で
導出できる：
- 1: φ∧ψ （前提）
- 2: φ （1∧除去）
- 3: ψ （1∧除去）
- 4: ψ∧φ （3,2∧導入）
記法について説明しておこう．左端の番号は行のラベルである．
この演繹では最初の行は前提であり，それ以外の行は推論規則を
適用することによって導かれた式である．右側の括弧内には
そこで用いた論理式と推論規則が示してある．たとえば４行目では
３行目の式と２行目の式から∧導入によってψ∧φを導出している
（ψを左に，φを右に置いて∧導入を適用したことに注意されたい）．
このように行を追って演繹過程を示す代わりに，次のような図で
演繹を表現することもできる．
このような図を証明図と呼ぶ（演繹図あるいは推論図
などとも言う）．このような図が一般に木構造をもつということに
注意されたい．前提は「葉」，推論規則は「分岐」，帰結は「根」に相当する．
2.2 ∧と∨に関する例
ゲンツェンの自然演繹では∨についても「∨導入」と
「∨除去」の推論規則があるが，上の∧の推論規則に
似ているのは
である．∨除去の方は前提以外にすでに触れた自然演繹特有の
「仮定」を含むものなので，混乱を避けるためここでは説明を
省略する（次の章を参照されたい）．
∨導入を前述の∧の推論規則と組み合わせれば，たとえば
- φ∧ψ |- φ∨ψ
が示せる：
- 1: φ∧ψ （前提）
- 2: φ （1∧除去）
- 3: φ∨ψ （2∨導入）
２行目でψを残すこともできる：
- 1: φ∧ψ （前提）
- 2: ψ （1∧除去）
- 3: φ∨ψ （2∨導入）
2.3 →に関する例
→に関する推論規則としてすでに説明したようにMPがある．
これを用いてたとえば
- {φ, φ→ψ, ψ→χ} |- χ
を示すことは簡単にできる：
- 1: φ（前提）
- 2: φ→ψ（前提）
- 3: ψ（1,2 MP）
- 4: ψ→χ（前提）
- 5: χ（3,4 MP）
それでは
- {φ→ψ, ψ→χ} |- φ→χ
はどうだろうか？すぐに気が付くように，これはMPだけでは
示せそうにない．意味論的にはこれら二つの演繹関係は
ほとんど同じ内容をもつのだが，推論規則にもとづく
形式的取り扱いではこのように大きな違いが現れる．
後者を示すには推論規則を増やすか適当な公理を置くしかない．
この演繹関係自体を推論規則にするという考え方もあるが
（実際，これを三段論法と呼ぶこともある），普通はこれを
もう少し基本的な推論規則から導出する．ゲンツェンの自然演繹
ではMPを「→除去」と呼び，それと対をなすものとして「→導入」
という推論規則を用意している．それらを組み合わせると上の
演繹関係が簡単に導出できる（→導入の推論規則も∨導入と
同様に「仮定」を含むものなので，ここでは説明を省く）．
推論規則を増やす代わりに，既に述べたヒルベルト流の公理
（実際にはその最初の二つ）を用いることでも，上の演繹関係を
示すことができる．これについては，ヒルベルト流の形式化に
おける証明の例として，あとで再度議論する．
3. ヒルベルト流の形式化
論理体系の形式化の例として，以下ではヒルベルト流の
古典論理の形式化を紹介する．命題論理の場合を中心に説明し，
述語論理の場合については最後に簡単に触れるにとどめる．
さらに詳しい内容については
- 小松寿「記号論理学入門」（森北出版，1997）
- 田中俊一「位相と論理」（日本評論社，2000）
- 松本和夫「数理論理学」（共立出版, 初版1970，復刊2001）
などを参照されたい．
3.1 命題論理の形式化
- 論理式の構成要素
-
このように，ヒルベルト流の命題論理の形式化では論理結合子として
→と¬のみを用いる．∧，∨，↔は，一種の省略記法で，たとえば
- φ∨ψ = ¬φ→ψ
- φ∧ψ = ¬(φ∨ψ)
- φ↔ψ = (φ→ψ)∧(ψ→φ)
というように派生的に定義される．論理式は命題記号をこれらの
論理結合子で結んで得られるものである．その構文規則は命題論理
の意味論で説明したものと同じである．
- 公理系
- (A1) φ→(ψ→φ)
- (A2) (φ→(ψ→χ))→((φ→ψ)→(φ→χ))
- (A3) (¬φ→¬ψ)→(ψ→φ)
- 推論規則
-
φ φ→ψ
ψ |
Modus Ponens (MP) |
- 演繹
-
論理式の集合Γ={φ1,...,φn}
から論理式ψが演繹される（記号で Γ|-ψ ）
ということの意味はすでに説明したとおりである．特に，
前提なし（Γが空集合）で公理のみから ψが導出できる
とき ψ はこの論理体系の定理である（記号で |-ψ ）
という．
【注意】ヒルベルト流の形式化における公理系の選び方にも
実はいくつかの流儀がある．ここに示した公理系はウカシェビッチ
（Lukasiewicz）によるもので，いわばこれ以上減らせない最小限の
公理からなっている．この三つの公理に還元できるということ
自体は重要であるが，あとで示す演繹の例を見ればわかるように，
この三つだけで演繹を行うことは実は非常に大変である．
そのため，もう少し冗長性をもたせて使いやすくした公理系を
用いることもある．たとえば，ラッセルとホワイトヘッドが
著作（1910--13）で用いた公理系は４個の公理からなる．
また，ヒルベルトとベルナイスの著作（1934, 1939）では
１５個の公理が採用された．
3.2 演繹の例
演繹の簡単な例をいくつか紹介する．
【例１】 |- φ→φ （φは任意の式）
- 1: φ→((φ→φ)→φ) (A1)
- 2: (φ→((φ→φ)→φ))→((φ→(φ→φ))→(φ→φ)) (A2)
- 3: (φ→(φ→φ))→(φ→φ) (1,2 MP)
- 4: φ→(φ→φ) (A1)
- 5: φ→φ (4,3 MP)
右端のコメントが A1,A2 となっているのは該当する公理を
用いたところである．公理はひとつの式ではなくて「式のパターン」
である，ということを改めて思い出されたい．たとえば１行目では
本来の公理A1で ψ= (φ→φ) と選んだものを使っている．
【例２】{φ, ¬φ} |- ψ （φ，ψは任意の式）
- 1: ¬φ（前提）
- 2: ¬φ→(¬ψ→¬φ) (A1)
- 3: ¬ψ→¬φ (1,2 MP)
- 4: (¬ψ→¬φ)→(φ→ψ) (A2)
- 5: φ→ψ (3,4 MP)
- 6: φ (前提)
- 7: ψ (6,5 MP)
この演繹の前提の {φ, ¬φ} は「矛盾」を表わす．
したがってこの演繹は「矛盾からは何でも結論できる」
ということを意味している．
【例３】{φ→ψ, ψ→χ} |- φ→χ
- 1: ψ→χ (前提)
- 2: (ψ→χ)→(φ→(ψ→χ)) (A1)
- 3: φ→(ψ→χ) (1,2 MP)
- 4: (φ→(ψ→χ))→((φ→ψ)→(φ→χ)) (A2)
- 5: (φ→ψ)→(φ→χ) (3,4 MP)
- 6: φ→ψ (前提)
- 7: φ→χ (6,5 MP)
これは保留にしてあった三段論法の証明である．
ここで示した定理や演繹関係はいずれも意味論的には明らかな
ものばかりであるが，ヒルベルト流の形式化（正確に言えば
そのウカシェビッチ版）ではこのように簡単な場合でも導出に
かなりの手間がかかる．また，導出過程自体が，何をやっているのか
いまひとつ明快でない．その根本原因は推論規則として MP しか
用意していないことにある（公理系にもうすこし冗長性をもたせれば，
使いにくさは多少改善されるにしても）．これとは対照的に，
ゲンツェン流の形式化（特に自然演繹）は推論規則を沢山用意する
（その代わり公理は非常に少ない）ことによってはるかに使いやすい
ものになっている．
3.3 形式的体系に関する定理
命題論理をヒルベルト流に形式化するとき，以下のようなことが
成立する：
- 演繹定理
- Γを論理式の集合，φとψを論理式とするとき，
Γ∪{φ}|-ψならば Γ|-φ→ψ である．
- 逆演繹定理
- Γを論理式の集合，φとψを論理式とするとき，
Γ|-φ→ψ ならば Γ∪{φ}|-ψ である．
- 健全性定理
- 任意の論理式φに対して，|-φ ならば |=φである．
- 完全性定理
- 任意の論理式φに対して，|=φ ならば |-φである．
これらは形式的体系に関する定理なので，形式的体系の
「中で」形式的に証明される「定理」と区別する意味で
超定理（metatheorem）とも呼ばれる．この他にも
さまざまな超定理が知られているが，ここでは省略する．
演繹定理・逆演繹定理についてはこの後でもう少し議論する．
健全性定理は公理の恒真性とMPの妥当性からただちに従うが，
完全性定理（すでに触れたように，これはゲーデルによる）
の証明には少し準備が必要なので，ここでは紹介しない．
参考文献を参照されたい．
逆演繹定理はすぐに証明できる．実際，Γ|-φ→ψの
演繹は一般に
- 1: …
- … …
- n: φ→ψ (…)
という形をしているので，引き続いて
- n+1: φ (前提)
- n+2: ψ (n,n+1 MP)
という行を付け加えればΓ∪{φ}|-ψの演繹になる．
演繹定理の証明にはすこし長くなるので節を改めて説明する．
演繹定理は形式的演繹・証明を行う際に役に立つ．一般的に
言って，φ→ψを導出するよりもφを「前提」にしてψを
導出する方が簡単だからである．例を示そう．
【例題】|-¬¬φ→φ（二重否定の除去）を示せ．
演繹定理によって，問題は |-¬¬φ|-φを示すことに帰着する．
後者は次のように導出できる：
- 1: ¬¬φ (前提)
- 2: ¬¬φ→(¬¬¬¬φ→¬¬φ) (A1)
- 3: ¬¬¬¬φ→¬¬φ (1,2 MP)
- 4: (¬¬¬¬φ→¬¬φ)→(¬φ→¬¬¬φ) (A3)
- 5: ¬φ→¬¬¬φ (3,4 MP)
- 6: (¬φ→¬¬¬φ)→(¬¬φ→φ) (A3)
- 7: ¬¬φ→φ (5,6 MP)
- 8: ¬¬φ (前提)
- 9: φ (7,8 MP)
同じ前提を二個所で使っているが，一個所にまとめて
二度引用しても構わない．ただし，証明図に翻訳したとき
そのまま木構造に対応するためには上のように書く方が
よいだろう．
【注意】|-φ→¬¬φ（二重否定の導入）もこれから
ただちに従う：
- 1: ¬¬¬φ→¬φ (二重否定の除去)
- 2: (¬¬¬φ→¬φ)→(φ→¬¬φ) (A3)
- 3: φ→¬¬φ (1,2 MP)
【演習問題】次を示せ．
- 1. |- ¬φ→(φ→ψ)
- 2. |- (φ→ψ)→((ψ→χ)→(φ→χ))
- 3. |- (φ→ψ)→(¬ψ→¬φ)
3.4 演繹定理の証明
証明は Γ∪{φ}|-ψ の演繹
- 1: …
- … …
- n: ψ (…)
の行数 n についての帰納法による．n = 1となるのは
- ψが公理である
- ψがΓに属する前提である
- φ=ψである
のいずれかの場合であるが，第一と第二の場合には
- 1: ψ
- 2: ψ→(φ→ψ) (A1)
- 3: φ→ψ (1,2 MP)
により φ→ψ が導出できる．第三の場合にはすでに
示した |-φ→φ が使える．このようにして n = 1 の場合には
演繹定理が成り立つことがわかる．一般の n について，n < N の
場合に演繹定理が成立すると仮定して n = N の場合にも成立する
ことを示そう．n = N のとき Γ∪{φ}|-ψの演繹は
- … …
- … …
- N: ψ (…)
となって終わっているが，これには
- ψは公理である
- ψはΓに属する前提である
- ψはそれ以前の二つの行
- i:χ (…)
- j:χ→ψ (…)
からMPで導出される
の三通りの場合がある．第一と第二の場合には
Γ∪{φ}|-ψの証明に引き続いて
- N+1: ψ→（φ→ψ) (A1)
- N+2: φ→ψ (N,N+1 MP)
という行を付け加えれば Γ|-φ→ψ の演繹ができる．
第三の場合には，Γ∪{φ}|-ψ の演繹の中から i 行に
いたる部分と j 行にいたる部分を取り出せば，
Γ∪{φ}|-χ および Γ∪{φ}|-χ→ψ の演繹が
得られる．これらは Γ∪{φ}|-ψ の演繹よりも
行数が少ないので，帰納法の仮定が適用できて，
Γ|-φ→χ および Γ|-φ→(χ→ψ) であることが
わかる．この二つの演繹を組み合わせると
- … …
- p: φ→χ (…)
- … …
- q: φ→(χ→ψ) (…)
という演繹ができる（ここでの前提はΓのみ）．
そこで，引き続いて
- q+1: (φ→(χ→ψ))→((φ→χ)→(φ→ψ)) (A2)
- q+2: (φ→χ)→(φ→ψ) (q, q+1 MP)
- q+3: φ→ψ (p, q+2 MP)
という演繹を行えば，最終的にΓから φ→ψ が導出できる．
以上で数学的帰納法による証明が完成する．
3.5 述語論理の形式化
述語論理の形式化も命題論理の場合とほぼ同様の枠組みで行われる．
以下にその要点を示す．
- 論理式
- 論理式は原子論理式を論理記号（論理結合子と量化記号）
で組み合わせたものである．原子論理式は述語論理の意味論で
説明した通りである．論理記号については命題論理の場合と同様で，
→, ¬, ∀を基本的なものとして扱い，∨, ∧, ↔, ∃を
次のように派生的に定義する．
- φ∨ψ = ¬φ→ψ
- φ∧ψ = ¬(φ∨ψ)
- φ↔ψ = (φ→ψ)∧(ψ→φ)
- ∃x φ = ¬∀x(¬φ)
- 公理系
- 公理としては命題論理の場合の(A1), (A2), (A3) に加えて
量化記号に関する次の公理を置く．
- (A4)∀xφ(x)→φ(t)
（t は任意の項，φ(x)は x を自由変数として含む論理式，
φ(t)はφ(x)の自由変数 x を項 t に置き換えたものをあらわす）
- (A5)∀x (φ→ψ(x))→(φ→∀xψ(x))
（φは x を自由変数として含まない論理式，
ψ(x) は x を自由変数として含む論理式）
- 推論規則
- MPに加えて，次の推論規則を置く．
φ(x)
∀xφ(x) |
Generalization (Gen) |
ここでφ(x)は x を自由変数として含む任意の論理式とする．
ただし，この規則(Gen)を適用する際には，自由変数 x は次の
「固有変数条件」をみたさなければならない．
- 固有変数条件
- φ(x)を導出するまでに行った推論の前提（公理を除く）
をすべてを集めた集合をΓとする（Γ|-φ(x)となる）．
このとき x は前提Γの中に自由変数として現れてはならない．
【注意】(Gen)は x を自由変数として導かれた主張φ(x)を
∀xφ(x)に取りまとめる規則であるが，それまでの推論の文脈を
無視しては成り立たない．固有変数条件はそのために
置かれたものである．この条件を無視して(Gen)を適用すれば，
意味論的に正しいと限らない帰結，たとえば |-φ(x)→∀xφ(x)
が得られてしまう（φ(x)→∀xφ(x)は恒真ではない）．実際，
固有変数条件を無視して(Gen)を適用すれば φ(x)|-∀xφ(x) が導かれ，
これと演繹定理を組み合わせれば |-φ(x)→∀xφ(x) が出てくる．
固有変数条件によってこのような誤った推論を防ぐことができる．
【演習問題】次のことを示せ．
- 1. |- ∀x φ(x)→∃x φ(x)
- 2. |- φ(t)→∃x φ(x) （存在汎化）
ここで，φ(x) は x を自由変数として含む論理式，t は任意の項，
φ(t) は φ(x) の自由変数 x を t で置き換えたもの．
キーワード
意味論，構文論，形式的体系，公理系，推論規則，排中律，
前提，帰結，MP（modus ponens），妥当性，証明，演繹，推論，
演繹関係，定理，健全性，完全性，証明図，演繹図，推論図，木構造，
超定理，固有変数条件