存在論的コミットメント免除の限度
これまでに次のことを見てきた：

１、単称名辞が指示する対象／存在者を措定する必要はない。
２、述語のような一般名辞についても、それが抽象的存在者の名前であると認めることなしに使うことができる
３、意味という存在者を認めずとも言明は有意／同義でありうる。

このように、存在論的コミットメントを次々に免除していった。では、この免除はどこまでも可能なのか。クワインはこの問に対して、否定的である。そして、上記で触れた量化子の変項を再度持ち出す。つまり、束縛変項を使用する際にはその背後にこれを充足する要素の集合（⊆議論領域）が措定されており、この前提を排除することはできないため、束縛変項に対しては、存在論的コミットメントを免除することはできないという。だが、この使用が存在論的コミットメントの唯一の仕方であるとも言う。

存在者とされるということは、掛け値なしに言って、変項の値と見なされることである。（『論理的観点から』和訳p19）

存在論的前提（意味論的次元からの回答）
量化の変項は、我々の存在論がなんであれ、その全域にわたる。そして、存在論的前提を我々が持っているとするのに必要十分な条件は次のものである。ある言明を真とするためにはその言明が持つ変項の及ぶ範囲に、この前提されていると言われたものが入っていなければならないという条件である。

　　　　∃xFxは真である　⇔　∃x x∈F

例えば「白い犬がある（いる）」という文は、犬性や白さ性という存在論にコミットしているわけではない。この文は、「ある何かが犬というクラスに含まれており、かつ、その何かが白いというクラスに含まれている」ということである。そして、この文が真であるためには、量化子の変項に白い犬がなければならないが、犬性も白さ性もこの集合Dに含まれている必要はないのである。

F＝xは犬である
G＝xは白い

∃x（Fx＆Gx）は真である　⇔　∃x x∈F、そして、∃x x∈G
※ここで、「犬性,白さ性∈D」である必要はない。

---

数学と存在論的コミットメント
古典数学は、抽象的存在者の存在論に徹頭徹尾コミットしている。例えば、∃x（xは百万以上である＆xは素数である）などの文は真とみなされる。こうして、普遍者をめぐる中世の大論争が、現代の数学の哲学において再燃した。クワインによると、我々は中世の頃よりもこの問題を明確にする基準を有しており、これによりある説/言明がどのような存在論にコミットしているかを決定できる。その基準とは：

ある理論がコミットしている存在者とは、その理論の中で肯定される言明が真であるためには、その理論の束縛変項によって指示されえなければならない存在者のことである。

つまり、その説/言明の背景にある議論領域を明確にすることでそれらのコミットする存在論を決定できる。このような基準から、現代の数学の哲学は論理主義、直観主義、形式主義の三つの立場に分けられる。これらはそれぞれ中世における実在論、概念論、唯名論の立場に対応している。

実在論（論理主義）

　　　・普遍的対象を認める
　　　・古典数学を擁護する

この立場は、フレーゲ、ラッセル、ホワイトヘッド、チャーチ、カルナップを代表者とする。数学におけるプラトニズムであり、普遍者／抽象的対象は、心が作り出すものではなく、心と独立に存在するとする。また、この立場は、束縛変項が表示する対象を知られているかどうかにかからず許す。

概念論（直観主義）

　　　・普遍的対象を一部認める
　　　・古典数学を部分的に否定する

この立場は、ポアンカレ、ブラウアー、ワイルを代表者とする。直観主義は、抽象的対象の束縛変項による指示を（議論領域に抽象的存在者を加えるのことを）許容するが、それはそのような存在者が前もって創りだされえる場合においてである。そして、この立場は、無限集合などの概念を許容しないため、実数に関するいくつかの古典的法則を捨てる。

唯名論（形式主義）

　　　・普遍的対象を一切認めない
　　　・古典数学を擁護する

この立場は、ヒルベルトを代表者とする。これは、直観主義と同じように論理主義者が行うむやみな普遍者の措定を批判するが、しかし、これは直観主義に対しても正反対の２つの理由から批判を行なう。１，形式主義は、論理主義者と同様、古典数学を損なうことに反対する。２，形式主義は、かつての唯名論者と同様、心によってつくられた存在者も含め一切の抽象的存在者を認めない。どちらの場合でも、形式主義者は、無意味な記号の戯れとして古典数学を捉える、ということが帰結する。しかし、数学が戯れであったとしても有用ではありえる。

---

競合する存在論を裁定するには
上記のような存在論の競合（特に数学における）を裁定するにはどのような手段が考えられるだろうか。先に見た意味論的定式化「あるということは変項の値であるということである」は、これの答えにならないとクワインは考える。なぜならば。この定式は：

“ある説や言明が、何があると言っているかを知るため”であり、
“何があるかを知るため”ではない。

ここで問題となっているのは、後者の「なにがあるのか」、つまり、議論領域の要素はなにかという問題である。

意味論的次元へ遡る
だが、なにがあるのか、について議論する際でも、意味論的次元（真偽を充足で捉える次元）に遡りそれを行なう。それは次の理由による。

・理由１（プラトンの髭を回避するため）
私はペガサスを否定するために、ペガサスを指示する必要があるという窮地に陥る。また、これを受け付けないならば、私は自分の存在論に存在しない（しかし、マックスの存在論には含まれる）対象について語ることになり、これは無意味である。
　上記で見たように、意味論的次元に後退することで、この問題を回避できる。なぜなら、ペガサスは文脈で定義することができ、それゆえこの対象が私の存在論に含まれていなくても語ることが出来るからだ、

・理由２（議論の共通の土俵を得るため）
存在論の相違は、概念図式における根本的相違を含意している。しかし、このような根本的な相違にかからず、マックスと我々は話題（例えば天候、政治、そして、言語の話題）を共有することができる。この事実が存在論的相違に関する議論を先送りにして、高い次元（表面上）の言語についての議論になってしまう傾向がある。しかし、既に見たように「なにがあるか」は語に依存するのだと結論してはならない。語の存在論的コミットメントは消去可能だからである。存在論的コミットメントは、束縛変項という意味論的次元において見出され、そのため、クワインによると、存在論の議論はこの次元でおこなわれねばならない。

---

科学理論の体系と我々の存在論
我々はまず合理性に従い、原初的なカオス的所与（なまの経験の無秩序な断片）を整合的に配置する最も単純な概念図式を採用する。これがもっとも広い意味での「全体論的概念図式」（over-all conceptual scheme）なる。そして、それによって、我々の存在論（議論領域）も決定される。
　そして、この概念図式の任意の部分（例えば、生物学的、物理学的部分）の合理的構成を決定する考慮は、全体の合理的構成を決定する考慮と種類において異ならない。つまり、全体図式から任意の科学理論の体系を決定することも言語の問題であり、存在論の決定と同じである。

　　　存在論の決定≒科学理論の体系の決定

二つの概念図式（現象的／物理主義的）
概念図式の構成は単純化という曖昧な原理によってなされる。また、単純化は常にひとつの標準を提供するとは限らない。次は、単純化の規則にって提供された二つの概念図式（※２）で、一方は物理的に基本であり、一方は認識論的に基本である。また、クワインによると二つのどちらも長所を持っているためどちらも発展させるべきである。

・物理主義（ノイラートの立場）
物理主義的概念図式は、量化の変項が及ぶ範囲を、外界について語る物理言語に限定し単純化する。

　　　直接経験→単純化→物理言語

・現象主義（カルナップの立場）
現象主義的概念図式は、量化の変項が及ぶ範囲を感覚所与（センスデータ）に限定する。しかし、現象主義は、カルナップが直面したように、無数に多様なセンスデータを原子命題と考えることはできないという問題をもつ。これに対してクワインは、「バラバラの感覚的出来事を一緒にし、それらを同一の対象のさまざまな知覚とみなす」という単純化を行なう。つまり、ヒュレーを志向的に統一することでノエマを構成する。このノエマが現象主義の存在論（変項の及ぶ範囲）である。

　　　直接経験→単純化→ノエマ

---

物事を単純化する便利な神話

・物理的対象という神話
物理的概念図式は我々の経験を単一の（物理的）”対象”へと単純化する。しかし、物理言語は現象主義的言語に還元／翻訳することはできない。物理的対象とは、我々の無数の経験を単純化するために仮定された存在者である。それは、無理数の導入が算術を単純化するのと同じである。しかし、物理的対象も無理数も便利ではあるがある種の「神話」である。

この神話（無理数を含んだ算術）は、字義通りの真理（有理数の算術）よりも単純であるが、字義通りの真理をその中にばらばらな部分として含んでいる。同様に、現象主義の観点からは、物理的対象の概念図式は便利な神話である。また、字義通りの真理（直接経験）よりも単純であるが、字義通りの真理をそのなかにばらばらな部分として含んでいる。

・クラスと属性という神話
物理的対象の属性（述語）やクラス（述語が指示する集合）はどうか。物理主義的概念図式の観点からは、この種のプラトン的存在論は神学の定話である。だが、数学はこの一段高い神話を本質とするため（数学は高階の論理で基礎づけられるため？）、この神話は数学にとって、そして、すべての自然科学にとって有益である。

・数学と物理学という神話の危機
数学と物理学は共に便利な神話を前提としているが、しかし、これらの領域は20世紀に発見されたパラドックスや定理によって危機に陥っている。例えば、数学はラッセルのパラドックスやゲーデルの不完全性定理によって、そして、物理学は徹底した矛盾ではないにしろ光の波動説と粒子説やハイゼンベルクの不確定性原理によってである。

---

ドメインの領域はどのような対象であるべきか
クワインがこれまでに示したこと：

・ある種の存在論を認める議論のいくつかが誤りであること（マックスとワイマン批判）
・言明/説の存在論的コミットメントが何であるかを決定する明示的な基準（存在するとは変項の値になるということで）

だが、存在領域に、どの存在を採用すべきかという問は未だに答えられていない。ここではまず次のような様々な方向から考察を試み（具体的な考察はこの論文には書かれていない）：

・物理主義的概念図式のどれだけ現象主義的概念図式に還元できるか。
・物理的概念図式が現象主義的概念図式に還元できないとしても探求を続けてみよう。
・自然科学がプラトン主義的数学から、どのように、あるいは、どのよう手間で独立と成りうるか。
・数学の探求も続けて、そのプラトン主義的基礎に探りを入れる。

現象主義の優位性とクワインの相対主義
こうした探求から、現象主義の概念図式は、認識論上の優先性をもっているという。現象主義的概念図式からは、物理的対象と数学的対象の存在論は確かに神話であるが、しかし、神話の性質は相対的である。この場合、それは、認識論的観点と相対的である。この認識論的観点は、我々の様々な関心や目的に対応する様々な観点の内の一つなのである。（概念図式相対主義、翻訳の不確定性などの議論へ）

---

※２
この区別は恐らく論理実証主義におけるプロトコル命題論争に基づいている。

マックスの主張
クワインは、まずペガサスなどの実際には存在しない対象である「非存在」を否定する際に生じる問題（否定存在言明のパズル）を「プラトンの髭」と呼び取り上げる。その際、彼はマックス（McX）とワイマン（Wyman）いう架空の哲学者を論駁する形で論を進める。

マックスはある存在（ペガサス）を主張しており、クワインはこれの存在を否定している。しかし、クワインがマックスが主張する存在を否定する時、ある困難に陥る。それは、「マックスは認めるが私は認めないようなもの（ペガサス）がある、と私には認めることはできない」というものだ。なぜなら、私がある存在を否定するためには、その対象を一旦認めてその上で否定しなければならないからだ（￢AはAがなければ作れない）。また、もしこの存在を最初から認めずに何にもないものを否定したとしても、その言明は無意味である（「￢」だけでは文にならない）。

１，“ペガサス”という対象を認める→文「ペガサスはない」は有意味である
２，“ペガサス”という対象を認めない→文「ペガサスはない」は無意味である

従って、マックスはペガサスが存在すると主張する。

マックスの混乱
だが、彼は血肉をもったペガサスが”実際に”存在するとは考えていない。彼によると、ペガサスの“観念”が人の心の中に存在する。しかし、ここにはマックスの混乱がある。なぜらな、最初にクワインが拒否した存在は、この「ペガサスの観念」ではなかった。彼が否定したのは、「血肉をもったペガサス」である。クワインとマックスの主張は噛み合っていないのだ。

---

ワイマンの主張（ペガサスは可能的に存在する）
クワインは、次に別のペガサスの擁護者としてワイマンを登場させて議論する（※１）。ワイマンによれば、「ペガサスは、現実化されていない可能的存在者としてある」。つまり、我々が、「ペガサスはない」と言うとき、彼によればこれは、ペガサスは、「xは可能的に存在する」という属性を持つが、「xは現実化されいる」という属性を持たない（つまり、血肉を持ったペガサスは可能的に存在する）のだ。

＜ワイマンのペガサス＞
A＝xは現実化されている
K＝xは可能的に存在する
ペガサス＝p

ペガサスはない　＝df（p?A　＆ p∈K）

・ワイマン批判１（「存在する」の常識的用法との乖離）
ワイマンは、「存在する」を「可能的に存在する」と「現実的に存在する」に区別する。そして、彼の「存在する」という語それ自体には時空的なニュアンスを含んでいない。このような「存在する」という語の使用は、日常的なこの語の使用と乖離する（これは「存立する」（subsist）とも言われる）。また、クワインはこのワイマンの「存在する」の用法を認めて、彼に”進呈”したとしても、まだ我々には「ある」という語が残されているため、問題にはならないという。

・ワイマン批判２
ワイマンの宇宙は、人口過剰で美しくない。

・ワイマン批判３（可能的存在の同一性の曖昧性）
可能性の住み着くワイマンのスラムでは、同一律が成り立たず秩序破壊的である。例えば、その戸口に立っている可能的な太った男と、同じ戸口に立っている同様に可能的なハゲの男を考えることで次のような疑問を持つ：

ここには同一の可能的な男がいるのか。
異なる二人の可能的な男がいるのだろうか。
どうやってそれを決めるのか。
その戸口には何人の可能的な男がいるのだろうか。
可能的な太った男よりも可能的な痩せている男のほうが多くいるのだろうか。
そのうちどれだけがお互いに似ているのだろうか。
それとも、互いに似ているということは、同一だということになるのだろうか。
可能的なものはどれひとつとして互いに似ていることはないのだろうか。

クワインによると、同一性の概念は、可能的存在者に対しては恐らく適用できない。そして、同一律が成り立たない存在に対して語ることは無意味であるように思われるという。

・ワイマン批判４（不可能なもの）
ペガサスの否定がパズルに陥らずに有意味なものとするために、ワイマンは「可能的に」という様相概念を導入した（ペガサスはない＝ペガサスは現実化されていないが、可能的に存在する）。クワインはこのような様相概念の導入は、「不可能的存在」を認めざるをえなくなると主張する。まず、冒頭の問題を振り返る：

「ペガサスがある」を前提しなければ、「ペガサスがない」が無意味となる

次に、例えば、ペガサスの代わりに「丸い四角」という矛盾した不可能な対象で同様に見てみる：

「丸い四角がある」を前提しなければ、「丸い四角はない」が無意味となる

ペガサスとは異なり丸い四角は、現実化されていない可能者としても認めることができない。つまり、ワイマンのように様相概念の導入すると、不可能者の領域をも認めざる得なくなる。こうした不可能者の領域には多くの困難があるように思われる。

だが、ワイマンは、ディレンマのもう一方の角（下記の４）を選んで、「「丸い四角はない」と言うことは無意味である」とすることができ、「丸い四角」は無意味であると彼は言う：

３，“丸い四角”という対象を認める→「丸い四角はない」という文は有意味である
４，“丸い四角”という対象を認めない→「丸い四角はない」という文は無意味である

このように矛盾した文は無意味であるとする立場は昔からある。しかし、これは矛盾から結論を導く背理法を疑問視するといった極端な道に至るし、また、矛盾が意味を有しないということは、矛盾を手がかりに行われる文の真偽チェックができなくなるということだ。

---

クワインの解決策
以降は、彼は自身の解決策に移る。まず、彼はラッセルの記述理論を使って固有名を述語に還元する。

・ラッセルの記述理論
ラッセルは「表示について」で著名な記述理論を提唱した（詳細は別記）。例えば、「『ウェーヴァリー』の著者（the author of Waverley）は詩人である」は次のように分析される：

W＝xは『ウェーヴァリー』の著者である
P＝xは詩人である

(i)　ある『ウェーヴァリー』の著者が存在する。∃xWx
(ii)　多くとも『ウェーヴァリー』の著者は一人である。∀x（Wx→∀y（Wy→x=y））
(iii)　全ての『ウェーヴァリー』の著者は詩人である。∀x（Wx→Px）

この理論は、記述句を述語（命題関数）に分析することを可能にし、これらのまとまりが十分に意味を持ちうることを示したのである。

・記述理論による指示対象の排除
マックスとワイマンは確定記述（句）が指示の機能を持ち、従って、指示対象がなければならないと考えた。その結果、ある種の形而上学的対象を措定したのだった。しかし、ラッセルの理論は、記述を述語に還元することで指示概念の消去可能性を示している。対象を”指示”するという機能は、量化子の束縛変項による”表示”によって行われるのだ。

記述の場合は、あるということを肯定したり否定することにはもはやなんの困難もない。「『ウェーヴァリー』の著者がある」は記述理論で、

(i)　だれか（なにか）は『ウェーヴァリー』の著者である。∃xWx
(ii)　多くとも『ウェーヴァリー』の著者は一人である。∀x（Wx→∀y（Wy→x=y））

というこの二つの連言（i＆ii））で説明される。これに対して、「『ウェーヴァリー』の著者は次の選言（～i∨～ii）で説明される：

(i')　どのものも『ウェーヴァリー』を書かなかった　（～∃xWx）、または、
(ii')　二つ以上のものが『ウェーヴァリー』を描いた。（∃x（Wx＆∃y（Wy＆x≠y）））

この選言は偽だが有意味である。また、それは、『ウェーヴァリー』の著者を名指す表現を含んでいない。「丸い四角はない」という矛盾した記述を含む文も同様の仕方で分析される。そして、マックスやワイマンが行ったような存在を想定しなくてもすむのである。この分析によって非存在を含む確定記述の文の問題は解決する。

・文脈定義を固有名に適用
確定記述の文の場合は、プラトンの髭を剃り落とすことに成功したが、「ペガサス」などの固有名の場合はどうか。クワインは、固有名を述語に変換することで文脈定義を適用できるようにする。例えば、「ペガサス」だったら「ベレロフォンが捕まえた翼を持った馬」などの確定記述に書き換えてもいいし、確定記述が見つからなかったら、「xはペガサスる（pegasize）」や「xはペガサスである（x is-Pegasus）」などのように述語で表現するのである。これによって、上記と全く同様にラッセルの理論を適用し、直接指示の対象を措定せずにすむのである。つまり、丸い四角やペガサスが“ない”と言う時、我々はそれらの存在論にコミットしなくてもよいのである。

---

述語がもつ普遍者の存在論
上記の議論によって、固有名における存在論的コミットメントは排除された。次にクワインは、属性、関係、クラス、数、関数といった論理カテゴリーに存在者を措定する必要があるのか考察する。マックスはそうした（イデア的・普遍的）存在者があると考える。属性（赤さ）について、彼は次のように言う：

赤い家、赤いバラ、赤い夕陽がある。ここまでは哲学以前の常識である。そうすると、こうした家、バラ、夕日は、なにか共通のものを持っている。そして、この共通のものが、赤の属性ということで私が意味するものにほかならない。

マックスは、「赤い家、バラ、夕日がある」以上に「属性がある」ことは明白でトリビアルなことなのである。なぜならば、ある人がある言明の解釈を行なう際に、この判斷はその人がもつ「概念図式」（conceptual sheme）に基づいている。そして、概念図式は彼のもつ存在論（変項の及ぶ範囲＝集合）に基づいている。従って、その人にとって存在論的な言明は当然で公理とも言えるようなトリビアルなことだからだ。マックスの「属性がある」という存在論的言明も彼の持つ公理から発せられたものであり、そのため、明白でトリビアルなことなのだ。｛赤｝⊆マックスのD。マックスとは別の人の概念図式からすれば、マックスが当然とする存在論的言明が偽と判斷される場合もあろう。従って、マックスの存在論と概念図式からしたら「赤さ」の存在論がいかに明白だとしても、それは相対的なものであり実際の説得力をもっているわけではないのだ。

加えて、普遍者の存在論を主張するためにそれを名前（「赤」という名前）と見なすという方法があるだろうが、上記において名前は既に述語に還元されており、この手段は使えない。

---

意味の存在論
マックスは次に意味の存在論を主張する。彼によると、意味と指示の区別があり、かつ、述語が属性の名前でないとしても、それでも語は「意味を持つ」ということは明らかである。こうした意味は、それが指示されようがされまいが普遍的なものである。そして、この中に先に見た属性と呼ばれるものがあるのかもしれない。

これに対するクワインの応答は、「意味なるもの」を排除してしまうというものだ。マックスは意味を「持たれるもの」（抽象的な対象）として考えるのに対して、クワインはそのように物化して考えない。そのため、マックスが言うような「持たられるような意味なるもの」を排除したからといって、語や言明が有意味であることを否定するわけではないのだ。そのため、マックスの意味なるものの排除はなんの痛みももたらさないという。

有意味性は有意と同義に還元できる
ではクワインの意味はどのように説明するか。彼はそれを「有意」（significant）（意味の物化を避けるために有意味とは区別した語を使う）と「同義性」から説明する。ある言明に意味を与えるということは同義な表現を与えるということである。有意と同義という語に対する厳密な説明は他の論文で行われる。

---

※１
ワイマンのモデルは一般的にA.マイノングだとされる。しかし、プリースト（『存在しないものに向かって』）によると、彼はマイノングよりもマイノングに影響を受けていた頃のラッセル（1903）に近いという。

タルスキの真理理論
前回の６－３の評価点と反省点を踏まえてデイヴィドソンが注目するのがタルスキの真理理論である。この真理理論の特徴は、この理論が対象言語のすべての文Sに関して、T文を含意する＜規約T＞を要求することである。

＜規約T＞
Sは真である⇔P
※ 'S'をSの正準記述で'P'をSの翻訳で置き換えることによって得られる。

この理論における重要な意味論的概念は「充足」の概念である。もし理論の言語（メタ言語）が十分な集合論を内包しているならば、真理は充足の概念によって明示的に定義されうる。つまり、「充足」という概念を使えば、「私の言語」に言及することなく意味論的構造を与えられる可能性があるのだ。

デイヴィドソンの解釈理論（真理理論を応用）
　タルスキは自然言語の複雑な要因を排除した形式言語を扱った。以下は、自然言語に適用するように修正された真理理論は、解釈理論として用い得る、という主張である。この解釈理論は次の３つの問いに応えることで明確にする：

１，タルスキの真理理論を自然言語に適用することは可能か
２，解釈者は解釈する言語に関して無知だとした場合、彼にとっても利用可能な証拠によって解釈理論を検証することは可能か。
３，もしその理論が真であると分かったならば、その言語の話し手の発話を解釈することが可能か。

---

１，自然言語に関して真理理論を与えることは可能か
　タルスキの真理理論におけるT文の際立った特徴は、次の二つ：

T文の特徴１：一つのT文は一つの文の真理条件を述べる
T文の特徴２：その際、当の文自体という資源より豊富な資源は用いられない（資源は同じなため）

異国語については、タルスキの＜規約T＞のように、「翻訳」という概念が要請される。

自然言語の形式化の試み
　自然言語がもつ様々な複雑な特徴を形式化することは難しい。例えば、態度的帰属文や様相などの問題は未だに残されている。一方、前進したと思われる事柄もある。例えば、固有名（T・バージ）、ought（G・ハーマン）、量名辞と比較級（J・ウォーレス）、態度帰属と行為遂行的発話、副詞、出来事、因果的単称言明、引用（デイヴィドソン）、などである。

自然言語の真理理論
　自然言語に詳細に真理理論を適用するという仕事は、二つの段階に分かれるだろう：

段階１：T文の集合を集めて真理定義する段階
段階２：一つか一つ以上の残りの文のそれぞれを適応させる段階。

我々は理論の最初の段階が扱う文を、全ての文の論理形式と深い構造を与えるものとして考えることができるだろう。

---

２，真理理論は、解釈が始まる前から利用可能であった証拠によって確証されうるか。

　真理理論は対象言語の各文に関してT文を生成する、と＜規約T＞は言う。そのため、真理理論が正しいことを示すために、T文が真であるということを検証すればよい。実行可能な理論は、次のことを公理とする（直接的な検証の範囲を超えたものと見なす）：

公理１，文をこれよりも短い語（表現）の連結として扱わねばならない。
公理２，充足や指示のような意味論的概念を導入しなければならない。
公理３，系列や系列によって整列させられる対象の存在論に訴えなければならない。

この真理理論はT文の形でテスト可能な結果を含むだけで機能することになり、従って、それらの結果はそのメカニズムに言及を行わないのである。従って真理理論は、先に見た解釈理論に必要な２つの理論を調停する：

解釈理論に必要な理論１（統語論的構造の解明の要求）
理論によって文法構造が分節化されねばならないという要求

解釈理論に必要な理論２（意味論的構造の解明の要求）
理論が文に関し述べることだけに基づいて（つまり、私の言語への言及なしで）当の理論がテストされねばならないという要求

根源的解釈においては＜規約T＞のように翻訳の概念を前提できない。そこで、翻訳と真理の関係を反転させる。つまり、タルスキは「翻訳」を前提として「真理」を定義するが、ここでは「真理」を前提として「翻訳」（そして解釈）の説明を行なう。真理（～は真である）は発話に付与されたりされなかったりする唯一の性質であり、かつ、これは単純な態度を結びつく傾向があるため、根源的解釈においても利用できる。真理と翻訳を反転させた規約Tが次のものである：

＜規約T＞（反転Ver）
Sは真である⇔P
※ただし、'P'は真である任意の文によって置き換えられる。

　この定式化が与えられると、真理理論はT文が真であるという証拠によってテストされる。ここには、解釈理論の生成に必要な「形式的制約」と「経験的制約」が課されている。

信念と意図は証拠にはできない
　では、解釈の場合、どのような証拠が利用可能か。そうした証拠は、話の手の信念や意図の詳細な記述ではない（反省点５より）。信念と意味の相互依存性は、次の点で明らかである。

（X）発話者はある文を真と見なす態度は、
（Y）その文が意味すること（意味）、かつ、（Z）彼が信じていること（信念）に依存する
XはY＆Zに依存する

我々は、XとYを知っているならば彼の信念（Z）を推論できる（XとYからZを推論）。彼の信念について十分な情報（つまりZとX）が与えられると、我々はおそらくその意味を推論できる（XとZからYを推論）。だが、根源的解釈は、意味（Y）/信念（Z）についての知識を前提としない証拠を用いなければならない。

証拠＝観察可能な信念＝真とみなす態度＝（X）
　意味（Y）/信念（Z）が使えないとするならば、証拠として可能性があるのはある文を真とみなすこと（X）である。（X）もひとつの信念であるが、単純な態度に結びつきやすく（頷きなど）、それは、すべての文に適用可能な唯一の態度で、かつ、複雑な信念ではないため解釈を始める前に解釈者にも理解可能であると前提してよい唯一の態度である。この証拠（X)は、理論を支持するためにどのように用いることができるのだろうか。次のようなT文がある（PはT文の右側で世界状態を意味する）。

（T）　∀x∀t（時間tにxによって話された時、Es regnetはドイツ語で真である
　　　　　　　　　　　　　　　　　　　　　　　　　　　⇔tにxの近くで雨が降っている（P））

　他方では、次のような形の証拠（X)がある。

（E）　クルトはドイツ語共同体に属しており、
　　　クルトは土曜日にEs regnetを真とみなす態度をとり（Z）、かつ、
　　　土曜日にクルトの近くで雨が降っている（P）

（E）を（T)の真であることの証拠となりうる。しかし、この（E)という個別事例を一般命題である（T)の証拠とした場合、全ての解釈は不可謬になるという問題が生じる。そこで、（T)は全称量化条件文であるから、第一のステップは次のような主張を指示する証拠をもっと集めて帰納的に一般化することでGEという証拠にする。

（GE)　∀x∀t（xはドイツ語共同体に属している→（xはEx regnetをtにおいて真とみなす
　　　　　　　　　　　　　　　　　　　　　　　　⇔tにおいてxの近くで雨が降っている（P）））※１

これが公的な基準となり不可謬性を回避できる。そのためこの（GE)が解釈理論の最初のステップである。

最良の適合としての解釈理論
　当然、誰であれ、自分の近くで雨が降っているかについて誤りうるため（つまり、Zの内容とPが一致しない可能性があるため）、（E)は（GE)や（T)に決定的な証拠となりえない。しかし、我々が求めているのは、「最良の適合」（the best fit）としての解釈理論である。これは形式論的制約と経験的制約を満たすが、ここにおける経験的制約はクルトが真とみなす文を可能な限り最大化すること（文の可能性無限に拡大するのではなくその中でもっとも有りそうな文の可能性を最大化して100％にすること）によって満たされる。

真理条件意味論という前提
以上で、T文の証明の説明は終わる。T文の証明で得られたものは文の意味ではなく、「真理条件」である。真理条件＝意味というデイヴィドソンの真理条件意味論は別の論文で述べられており、ここでもこの意味論が前提とされている。従って、T文の証明によって真理条件を得たこの時点で、発話文の意味の理解を成し得たことになるのである。

真とみなす態度からT文を証明する
↓
T文の証明によって真理条件が導かれる
↓
真理条件によって発話の意味が判明する
↓
解釈（文の意味と信念の理解）の半分が達成された

意味論的構造の解明（『真理と述定』和訳P81参照）
　未知の言語のための真理理論を考案する過程は次のように進むだろう。

最初のステップ（論理的真理）
第一に、我々は＜規約T＞を満足する理論を得るために、我々の論理（一階量化理論）を新しい言語に適合させる最良の方法を探らねばならない。
この場合の証拠は、すべての時と人によっても真もしくは偽とされてるような文の集合（論理的真理）と推論のパターンである。
一階量化理論を適応することで、述語、単称名辞、量化子、結合子および同一性が同定される。また、理論的にはこのステップは論理形式の問題を解決する。

論理的真理＆推論パターンという証拠
　　↓最良の方法
一階述語論理を未開言語に適用
　　↓
述語、単称名辞、量化子、結合子、同一性が同定される。
これによって規約Tを満足することができる。

第二のステップ（指標性の同定）
第二のステップでは、時には真とされ、時には偽とされる指標詞をもつ文に焦点が合わせられる。このステップは第一のステップと共に、個々の述語を解釈する可能性を制限する。

第三のステップ（残りの文）
最後のステップは、残りの文を扱う。それらの文は、一様な合意がないような文であったり、その真理値が環境の変化に系統だって依存しないような文である。

寛容の原理（信念の固定）
　真とみなす態度によるT文の証明という方法は、発話に真理条件を与える。これは「意味の問題の解決に関わる一方で、可能なかぎり信念を一定に保つことによって、信念と意味の相互依存性の問題を解決する、ということが意図されている」。つまり、文の意味とは、それ真理条件であるとする（真理条件意味論）。そうすると、解釈が成立する条件、つまり「意味」と「信念」の理解、の中で残されたのは「信念」のみということになる。

そして、デイヴィドソンは、信念を広範囲な同意（寛容の原理）によって固定する。この手順は、寛容の原理を前提とすることでのみ真とみなす態度（不同意や同意）が理解可能になる、という事実が正当化する。

また、寛容の原理における広範囲な同意とは、解釈する人を合理的であるとすることである。これは前提とすることが許されるだろうし、この前提によって解釈が可能になる。

---

※１
「ドイツ語」と「時間」という表現を無視して（E)、（GE)、（T)を記号化すると次のようになる：
Zxy＝xはｙを真と見なす
Px＝xの近くで雨が降っている
Txy＝xによって話されたｙは真である
e=Es regnetという発話

　　（E)　　∃x（Zxe＆Px）
　　　（GE)　∀x（Zxe⇔Px）
　　　（T)　　∀x（Txe⇔Px）

発話を解釈する
ある人間が発した音を言語と認識できたならば、私は彼の言葉を解釈を試みることができるだろう。解釈とは、その言葉の「意味」と、その言葉の意味に対する彼の「信念」を解明することである。

解釈＝ある人xによる文yの発話を理解すること
ある人xによる文yの発話＝yの意味＆xの意図
xの意図＝xのyの意味に対する信念
まとめると、解釈＝yの意味＆xのyの意味に対する信念の理解

解釈に対する問いは次の二つのものがある：

（問１）解釈を可能にするものとして、我々は何を知りうるのか（Whatの問）。（あとで見る答え：規約T）
（問２）解釈を可能にするものをどのように我々は知ることが出来るか（Howの問）。（あとで見る答え：真とみなす態度を証拠としたテスト）

解釈の問題は、異言語を解釈する場合はもちろん、発話者が解釈者と同じ言語を話す場合においても同様の問題が生じている。それは発話者が本当に同じ言語を使用していると言う確証を得ることができないからだ。しかし、解釈の問題を扱う場合は、異言語の解釈、特に根源的解釈のケースを扱うことが様々な前提を見過ごさないために役立つ。

---

解釈理論案１（意味の把握説）
　問１に対する簡潔な答えは、それは有意味な表現の「意味」に関する知識であ。二つの異なる言語の発話に共通する意味を想定するのである。そして、クルトがEs regnetといった場合、Es regnetの「意味」を自国語で把握した場合に解釈は成立する。例えば：

１，クルトはドイツ語でEs regnetと話していた。
２，ドイツ語でEs regnetは雨が降っているということを意味している。
３，従って、クルトは「雨が降っている」を意味する言葉を発していた。

これは解釈には、語や表現からなる一つのメカニズムを導入しなければならない、という重要な示唆がある。しかし、この答えは、問２に答えていないし、また、文の客観的「意味」という役に立たない考えを前提にしている。

（評価点１）解釈には語や表現からなるある種のメカニズムを導入しなけれならない。
（反省点１）「意味」にのみ解釈の源泉を求めるのは、解釈の証拠基盤を提供する「意図」（そして、これの根底にある「信念」）を無視している。

解釈理論案２（発話＝空気の攪拌説）
　解釈の説明に要請される概念が当の解釈自体よりも不可解であることが分かると、結局、口頭のコミュニケーションは、人間という主体に属する非言語的行動の間に因果的繋がりを形成している手の込んだ空気の攪拌以外の何ものでもない（つまり、同一である）と考えたくなる。しかし、発話＝（非言語的）意図を伴った行為/身体運動という見解は、問１に答えをもたらさない。

（評価点２）解釈に意図という観点を導入している。
（反省点２）発話と意図を伴った行為とを同一視する態度は、その「証拠」（意図をともなった行為）と、それが「証明していること」（発話）との関係に関してなにも情報をもたらさない（A=Bという同一律では情報がない）。

案１と案２の反省（証拠と証明していることのギャップ）
反省点１と２により明らかになるのは、解釈における「証拠」（意図/信念を伴った行為）と「証明していること」（発話）との間にはギャップがあり、これを埋めなければならないということだ。そして、これ橋渡しするための試みは次のものである。

---

解釈理論案３（行動主義的証拠による個々の文の解釈）
オグデン等の因果説は、行動主義的データを証拠として文の意味を一つづつ別々に分析する。しかし、この試みは複雑で抽象的な文の解釈へ進むことはできない（解釈の範囲が限定され無限にある文に意味を与えることはできない）。

（評価点３）経験的証拠を解釈のベースに据えようとしている。
（反省点３）解釈可能な文の範囲が限定されている。（解釈理論は無限にある文のどれをとっても解釈が成立するようなものでなければならない。）

解釈理論案４（語の解釈から文の解釈へ向かう）
文はたとえ無限であっても有限な語が結合されることで成り立っているので、語を解釈することで発話（証明しようとしていること）の解釈に到達できる、と考える。しかし、この立場は、「語」の解釈から開始するため、すなわち、語に対する「証拠」が要請される。しかし、語の意味論的特徴（文脈定義）は非言語的現象では説明できないため、この場合の証拠の到達に失敗する。文の前に語に意味論を与えることはできない。

（評価点４）有限なものから解釈を開始している
（反省点４）語から解釈を開始することはできないので、あくまで文から解釈しなければならない。

解釈理論案５（意図と信念の説明する）
　根源的解釈の際に、発話者の文が典型的に伴う意図の「説明」を解釈の証拠にする。しかし、この説明は証拠にはなりえない。なぜなら、「発話者の意図」、「発話者の信念」、そして、「言葉の解釈」は一つの計画の諸部分であり、それらは相互依存の関係にあるため、「発話とは独立的に区別された意図」は理解できないからだ。

（評価点５）発話の解釈を信念や意図（つまり、発話の理解をまったく前提としないもの）をベースにして行なう。
（反省点５）信念と意図は相互依存で個別的に説明できない。

解釈理論に課せられている制約を具体化
上記のさまざまな解釈理論の反省点を踏まえて冒頭の２つ問の答えに対する制約を具体化する：

・問１：解釈を可能にするものとして我々はなにを知りうるか
制約１－１，解釈理論は一般的（ある言語のどの発話も理解可能）でなければならない（反省点３より）
制約１－２，解釈者が知りうるものは有限な形で表現しなければならない（評価点４より）
制約１－３，解釈理論は「客観的意味」 といったものに明白に言及してはならない（反省点１より）

制約１－２の補足、有限な表現という要請から全ての言語に通じるような普遍的方法（universal）として解釈理論は諦めなければならない。そして、解釈理論は個別の言語の発話者の発話を解釈者がいかに解釈できるのかを説明することになる。

・問２：解釈を可能にするものをどのように我々は知りうるか
制約２－１，利用可能な証拠によって解釈理論は検証されなければならない（評価点３より）。また、解釈理論は一般的なもの（制約１－１）なので個別の解釈事例が一般的解釈事例を検証することになる。
制約２－２，根源的解釈の証拠は、解釈者が解釈する発話を全く知らない場合でも利用できるものでなくてはならない（評価点５より）

---

解釈理論案６（翻訳理論説）
「翻訳理論」こそ解釈理論であるという立場。翻訳理論は、異国語の任意の文から既知の言語へと進むための実効的手続きである。したがって、これは解釈理論は有限の仕方で記述できる方法である（制約１－２を充たす）。しかし、問題もある。

言語間の関係を扱う理論
　翻訳理論は、解釈の対象となる言語（対象言語）と解釈を行なう言語（メタ言語）の他に対象言語が翻訳される言語（翻訳主体言語）が必要になる。つまり、この場合の解釈理論は二つの言語間の”関係”を扱うことになる。

　　　　　　　　　　　L2：メタ言語
　　　　　　　　　　（理論の言語）
　　　　　　　　　?　　　　　　　　　?
　　　　L1：対象言語　　　　　　　L3：翻訳主体言語
　　　（翻訳する言語）　　　　　　（翻訳される言語）

解釈理論案６－１（L1≠L2≠L3）
この理論によると、解釈者がL1とL3の意味を知らない場合でも翻訳が成立することになる。しかし、意味が理解できていないので解釈が成立したことにはらない。

（反省点６－１）解釈理論は発話の意味を理解するための理論であり、これはそれを満たさない。

解釈理論案６－２（L１≠L２＝L3）
メタ言語と翻訳主体言語が同一である場合、その解釈理論を理解する者は、異国語の発話を解釈するのに翻訳マニュアルを使うことができる。だがここには次の二つの仮定がある。

（仮定１）L3が解釈者自身の言語であるという事実。
（仮定２）自身の言語における発話をいかに解釈するかに関する解釈者の知識。

翻訳理論に従い解釈のケースを次のように置き換えると仮定１には問題があるのが分かる：

クルトの言語におけるEs regnetは、私の言語において「雨が降っている」と翻訳される。

いかなる解釈者にも有効な一般的な解釈理論においては、この指標的な自己言及（私）は不適当である。また仮定１が解決できたとして仮定２が残っている。

（評価点６－２）翻訳マニュアルという翻訳する言語から翻訳者の文を作る理論が使える。
（反省点６－２）解釈理論は、意味論的構造を明らかにする必要がある。

解釈理論案６－３（L1＝L２＝L3）
　自身の言語のため翻訳理論を解釈理論に加えたと仮定した場合、このとき我々は求めていた解釈理論に至るだろう。これは次の二つの理論を両方とも持っているからだ：

解釈理論に必要な理論１：構文理論的構造を明らかにする理論（翻訳マニュアル）
翻訳する言語のそれぞれの文に対し、翻訳者の言語の文を作る理論。

解釈理論に必要な理論２：意味論的構造を明らかにする理論
解釈の理論が、これらなじみ深い文の解釈を与える。

既知の言語への言及を余分なものである。そして、この言及が抜け落ちた時、残されたものは、解釈を構造的に明らかにする対象言語のための解釈理論である。

（評価点６－３）翻訳マニュアルと意味論的構造のための理論が融合することで十全な解釈理論になることが判明した。
（反省点６－３）解釈の対象となる言語が「私の言語」でなくても意味論的構造を与えるような理論でなければならない。

---

タルスキの真理理論
　上記の６－３の評価点と反省点を踏まえてデイヴィドソンが注目するのがタルスキの真理理論である。

デイヴィドソンの解釈理論へ

ここでは、自然言語の記号化とはあまり関係ないが、項の代入を見る。

---

【述語論理の言語】

1)　論理結合子：＆、∨、⊃、～
2)　量化記号：∀、∃
3)　対象変数（個体変項）：x、y、z,...
4)　対象定数（個体定項）：a、b、c,...
5)　関数記号：f、g
6)　述語論理：F、G、H...
7)　補助記号：（（カッコ）、,（コンマ）

自然数論では次のような記号が加わる
4)'　対象定数：0.1.2,...
5)'　関数記号：Sx（＝x＋1）、＋、×、...
6)'　述語論理：＝、＜、...

例えば、∃x（x×y＜z）という論理式を今まで見てきた表記で表現すると、「∃xSf(x,y)z」という形になり、「Sφψ：φはψより小さい」、「f(x,y)：xをy倍した数字」と定義される。「Iφψ：φはψと同一である」という同一性述語を「＝」という同一性記号で表現するのはこれまで見てきたとおり。

---

【項と論理式】

・項の定義
対象変数と対象定数は項である。
t1,...,tmが項であるなるならば、f（t1,...,tm）は項である。

・論理式の定義
t1,...,tmが項であるなるならば、F（t1,...,tm）は論理式（原子式）である。
A,Bがともに論理式ならば、（A＆B）、（A∨B）、（A⊃B）、（～A）は論理式である。
Aが論理式で、xが対象変数ならば、（∀xA）、（∃xA）は論理式である。

---

【項の代入】
∃x（x×y=z）は∃x（x×y=w）などと変数を置き換えることができる。論理式Aに現れる全ての自由変数xに項tを代入して得られる論理式をA[t/x]と表現する。A[t/x]：論理式Aの自由変数xへ定数tを代入。

1)　sを項とする時、sに現れるすべてのxの出現をtで置き換えることで得られる項をs[t/x]と表す。例えば、f(x)という項の自由変数にtを代入することでf(t)が得られる。

2)　Aが原子論理式F(s1,...sn)のとき、A[t/x]はF(s1[t/x],...,sn[t/x])を表す。

3-1)　Aが（B＊C）（＊は＆、∨、⊃のいずれか）であるとき、A[t/x]は（B[t/x]＊C[t/x]）を表す。
3-2)　Aが～Bであるとき、A[t/x]は～(B[t/x])を表す。

4-1)　Aが∀yBまたは∃yBであるとしA[t/x]は、Aに自由変数xがないとき、Aを表す。
4-2)　Aが∀yBまたは∃yBであるとしA[t/x]は、項tに束縛変数yが出現しない場合、∀y(B[t/x])、∃y(B[t/x])を表す。
※Aを∃y（x×y=z）としてA[1/x]は∃y（1×y=z）になる。
4-3)　Aが∀yBまたは∃yBであるとしA[t/x]は、項tに束縛変数yが出現する場合には、∀u((B[u/y])[t/x])、∃u((B[u/y])[t/x])を表す。ただし、uはA、tに現れない新しい対象変数とする。
※自由変数xに代入する項tに束縛変数yが出現する場合とは、例えば、Aを∃y（x×y=z）としてA[y/x]とする。この[y/x]にはtにyに現れる。そして、この代入は∃y（y×y=z）になる。
　しかし、これは、yの二乗を意味しており、xをy倍するという意味とは異なってしまう。つまり、代入するtと束縛変数のyが被ること（tにyが出現すること）を制限しなければならない。そのため、tを代入する前に、束縛変数yを新しい束縛変数uに置き換える（B[u/y])。そして、その後に、自由変数xにyを含む項tを代入すれば被ることを防げる。
　代入する項tに束縛変数が出現する場合にそのまま代入すると問題がある：
A=∃y（x×y=z）
A[y/x]=∃x（x×x=z）
　これを防ぐために束縛変数だけ新しい変数uに置き換える：
A=∃y（x×y=z）
A[u/y]＝∃u（x×u=z）＝A'
A'[y/x]＝∃u（y×u=z

---

【同時代入】
（A[t/x]）[s/y]を

　　　A[t/x][s/y]

と表す。例えば、AがPxy、tがf(y)、sがg(z)、であるとし、この場合A[t/x][s/y]は、次のような手順で代入される：

　　　１，Pxy　[f(y)/x][g(z)/y]
　　　２，Pf(y)y　[g(z)/y]
　　　３，Pf(g(z))g(z)　

また、自由変数xとyを同時にそれぞれtとsに置き換えることを

　　　A[t/x、s/y]

と表す。そして、上記のように代入を行なうと次のようになる：

　　　１，Pxy　　　[f(y)/x、g(z)/y]
　　　２，Pf(y)g(z)

つまり、A[t/x][s/y]とA[t/x、s/y]は異なるものであり、A[t/x、s/y]による代入はワンステップでつまり同時に行われる。また、項もしくは論理式であるEのそれぞれの異なる自由変数x1...,xnをそれぞれ同時に項s1,...,snで置き換えることを

　　　E[s1/x1,...,sn/xn]

と表す。

---

また、次のような場合、多重の代入を省略できる：

　　　A[y/x][s/y]⇔A[s/x]

つまり、xをyに置き換えて、yをsに置き換えるため、xをsに置き換えるのと同値である。

自然演繹NDを前回まで概観したが、今度はゲンツェンが自然演繹を定式化する以前に、体系化した統語論の体系である論理計算（Logischer Kalkül（LK））をみる。LKは公理を（α→α）だけに限定して、これを元に推論規則でもってあらゆるトートロジーを導く。これは式の構造や論理結合子の推論規則を分離する体系である（もう一つの統語論の体系であるヒルベルトの公理体系は、公理を増やして推論規則を限定する）。

LKは連式（sequent）計算とも呼ばる。なぜならば、これまで見てきた自然演繹などで表現は、「A1,・・・Am ├ B」と結論が一つ（B）に限られるが、これの基本的な表現は、「A1,・・・Am→B1,・・・Bn」という連式である。つまり、導入可能性を意味する「→」（※１）の右辺が複数つの式「B1,・・・Bn」でありうる。これは、基本的に「→」の左辺は「A1＆A2＆・・・Am」を意味し、右辺は「B1∨B2∨・・・Bn」を意味する。

---

構造に関する推論規則

【weakning左】　　　　　　【weakning右】

Γ→Δ　　　　　　　　　　　Γ→Δ
――――　　　　　　　　―――――
A,Γ→Δ　　　　　　　　　Γ→Δ,A

【contraction左】　　　　　【contraction右】

A,A,Γ→Δ　　　　　　　　Γ→Δ,A,A
―――――　　　　　　　――――――
A,Γ→Δ　　　　　　　　　Γ→Δ,A

【exchange左】　　　　　　【exchange右】

Γ,A,B,Π→Δ　　　　　　　Δ→Γ,A,B,Π
――――――　　　　　　―――――――
Γ,B,A,Π→Δ　　　　　　　Δ→Γ,B,A,Π

【Cut】

Γ→Δ,A　　　　　　A,Π→Σ
―――――――――――――
　　　　　Γ,Π→Δ,Σ

論理結合子に関する推論規則

【～左】　　　　　　　　　【～右】

Γ→Δ,A　　　　　　　　A,Γ→Δ
―――――　　　　　――――――
～A,Γ→Δ　　　　　　Γ→Δ,～A

【＆左】　　　　　　　　　【＆右】

A,Γ→Δ　　　　　　　　　　Γ→Δ,A　　　　　　Γ→Δ,B
――――――　　　　　――――――――――――――
A＆B,Γ→Δ　　　　　　　　　　　　Γ→Δ,A＆B

【∨左】　　　　　　　　　　　　　　　　【∨右】

A,Γ→Δ　　　　B,Γ→Δ　　　　　　Γ→Δ,A　　
―――――――――――　　　　――――――
　　　　　A∨B,Γ→Δ　　　　　　　　Γ→Δ,A∨B　

【⊃左】　　　　　　　　　　　　　　　　【⊃右】

Γ→Δ,A　　　　B,Π→Σ　　　　　　A,Γ→Δ,B
―――――――――――　　　　―――――――
　　　A⊃B,Γ,Π→Δ,Σ　　　　　　　Γ→Δ,A⊃B

定理と矛盾
自然演繹では、矛盾式/恒偽式は┴、恒真式/定理は┬で表現されたが、LKにおいては、次のように表現される。

（定理）　　　→Γ
（矛盾）　　Γ→　

つまり、定理は前提が空白で、矛盾は結論が空白で表現される。

---

証明図
公理/始式（α→α）から開始して、これに上記の推論規則を適用した式を証明図（proof figure）という。そして、証明図の最後に出現する式Sを終式（end sequent）という。そして、SはLKで証明可能（provable）であるという。例として、非矛盾律～（P＆～P）という定理の証明図をつくってみよう。

（定理：非矛盾律）　～（P＆～P）

　　P→P
―――――――（～左）
　　P,～P→
―――――――（＆左）
　P＆～P→
―――――――（～右）
→～（P＆～P）

次にパースの法則の証明図を求めてみる。

（定理：パースの法則）　（（P⊃Q）⊃P）⊃P


(1)　　P→P[始式]
―――――――（Weakning右）
(2)　　P→P,Q
―――――――（⊃右）
(3)　　→P,P⊃Q　　　　　　　　P→P[始式]
―――――――――――――――――（⊃左）
(4)　　　　（P⊃Q）⊃P→P
――――――――――――（⊃右）
(5)　→　（（P⊃Q）⊃P）⊃P

証明図を作る際は、(1)始式から初めて(5)終式を導くのではなく、逆に終式から始式へと遡っていく。遡っていく手順は、多くの場合、終式から論理定項を一つづつ減らしていき、そして、最終的にweakningで余分な式を削って始式を導くというものになる（※２）。終式に一つづつ推論規則を適用していけば自ずと始式を導けるため、LKの証明図は自然演繹よりもタブローに似ている。

---

述語論理のLKは命題論理のLKに次の量化子の規則を加える。

量化子に関する推論規則

【∀左】　　　　　　　　　　　　　【∀右】

A[t/x], Γ→Δ　　　　　　　　Γ→Δ, A[z/x]
――――――　　　　　　　―――――――
∀xA, Γ→Δ　　　　　　　　　Γ→Δ, ∀xA

【∃左】　　　　　　　　　　　　　【∃右】

A[z/x], Γ→Δ　　　　　　　　Γ→Δ, A[t/x]
――――――　　　　　　　―――――――
∃xA, Γ→Δ　　　　　　　　　Γ→Δ, ∃xA

tは項、zは個体変項である。また、∀右と∃左におけるzは下式に現れない変項（eigencariable）でなけれなならない。例えば、次は「∀右」の正しい使用例である：


　A→A　　　　　　B→B
――――　　　――――（Weakning）
　A→B,A　　　　B,A→B
―――――――――――（⊃右）
　A⊃B, A → B
―――――――――――（∀左）
∀x（A⊃B）,A → B
―――――――――――（∀右）
∀x（A⊃B）,A → ∀xB
―――――――――――（⊃右）
∀x（A⊃B） → A⊃∀xB

次は誤用例である：

　A→A　　　　　　B→B
――――　　　――――（Weakning）
　A→B,A　　　　B,A→B
―――――――――――（⊃右）
　A⊃B, A → B
―――――――――――（∀右）
　A⊃B, A → ∀xB

この例において、∀右を適用した下式「A⊃B, A → ∀xB」と上式「A⊃B, A → ∀xB」を見比べると、下式は、Bに∀右を適用しているが「A⊃B」のBは量化子で束縛されておらず自由な出現を持つ可能性がある。そのため、これは「∀右」が成り立たない。

論証図の具体例を見てみる（exchangeは適当に省略している）：

(1)　　　　　　　　　　　　　　　　　　　　　　　　　　　　Gx→Gx　　　　　　　Hx→Hx
　　　　　　　　　　　　　　　　　　　　　　　　　　　　　―――――　　　　　――――
(2)Fx→Fx　　　　　　　　　Hx→Hx　　　　　　　　　Gx、Fx→Hx、Gx　　Hx、Fx→Hx、Gx
　　―――　　　　　――――――――　　　―――――――――――――――（∨左）
(3)Gx、Fx→Hx、Fx　　Hx、Fx→Hx、Fx　　　　　　Gx∨Hx、Fx→Hx、Gx
　　―――――――――――――（∨左）　　――――――――――（～左）
(4)　　　　Gx∨Hx、Fx→Hx、Fx　　　　　　　　　　　　～Gx、Gx∨Hx、Fx→Hx
　　　―――――――――――――――――――――――――――（⊃左）
(5)　　　　　　　　　　　　　Fx⊃～Gx、Gx∨Hx、Fx→Hx
　　　　―――――――――――――――――――――――（∀左×2）
(6)　　　　　　　∀x（Fx⊃～Gx）、∀x（Gx∨Hx）、Fx→Hx
　　　　―――――――――――――――――――――――（⊃右）
(7)　　　　　　　∀x（Fx⊃～Gx）、∀x（Gx∨Hx）→Fx⊃Hx
　　　　―――――――――――――――――――――――（∀右）
(8)　　　　　　∀x（Fx⊃～Gx）、∀x（Gx∨Hx）→∀（Fx⊃Hx）
　　　　―――――――――――――――――――――――（＆左）
(9)　　　　(∀x（Fx⊃～Gx）＆∀x（Gx∨Hx）→∀（Fx⊃Hx）


手順としては命題論理のときの論証図とさほど変わらない。つまり、結論の終式から開始して、論理定項を減らして、最終的にWeakningで余分な式を削ってα→αという始式を導く。ただし、述語論理の場合は、「∀右」と「∃左」の使用に注意する。そして、これらは、「∀左」と「∃右」よりも優先的に使用する。規則適用の優先順位（構造の推論規則を除いた）は、

　　論理結合子の規則　＞　∀左もしくは∃右　＞　∀右もしくは∃左

となる。上記でも、(9)にまず「＆左」を使って論理定項を減らし、減らす論理定項がなくなった(8)に「∀右」を使うという手順を踏んでいる。量化子がなくなればあとは、命題論理の証明図と同じである。

---

※１
LKでは導入可能性を「→」で表現し条件法は「⊃」を使う（自然演繹では、導入可能性を「├」、条件法を「⊃」もしくは「→」のいずれかで表現した）。

※２
この方法だとcutを使うことなく全ての証明図を作れる。つまり、cutは除去可能である。これは「cut除去定理」と呼ばれゲンツェンが証明した。

述語の自然演繹は、量化子と同一性記号の規則が加わるだけで、それ以外は命題論理と同じなのでそれほど難解になるわけではない。いくつか確認しておく。

---

（論証）　∀x(～Gx∨～Hx)、∀x((Jx→Fx)→Hx)　├　～∃x(Fx＆Gx)

1　　　(1)　　∀x(～Gx∨～Hx)　　　　　A
2　　　(2)　　∀x((Jx→Fx)→Hx)　　　　A
3　　　(3)　　∃x(Fx＆Gx)　　　　　　　　H(for RAA)
4　　　(4)　　Fa＆Ga　　　　　　　　　　　H(for ∃E)
4　　　(5)　　Fa　　　　　　　　　　　　　　4＆E
4　　　(6)　　Ga　　　　　　　　　　　　　　4＆E
1　　　(7)　　～Ga∨～Ha　　　　　　　　1∀E
1,4　　(8)　　～Ha　　　　　　　　　　　　6,7∨E
4　　　(9)　　Ja→Fa　　　　　　　　　　　5TC
2　　　(10)　　(Ja→Fa)→Ha　　　　　　2∀E
2,4　　(11)　　Ha　　　　　　　　　　　　　9,10→E
1,2,4　(12)　　～∃x(Fx＆Gx)　　　　　　8,11 RAA(3)
1,2,3　(13)　　～∃x(Fx＆Gx)　　　　　　3,12 ∃E(4)
1,2　　(14)　　～∃x(Fx＆Gx)　　　　　　3,13 RAA(3)

RAAを2回使うのは∃Eでキャンセルした前提3が再使用され復活するので、再度キャンセルするため。

---

・同意性記号を含んだ論証の自然演繹

（論証）　∃x∀y（Fy→x=y）、∃x（Fx＆Gx）　├　∀x（Fx→Gx）

1　　　(1)　　∃x∀y（Fy→x=y）　　A
2　　　(2)　　∃x（Fx＆Gx）　　　　　A
3　　　(3)　　Fa　　　　　　　　　　　　H（for →I）
4　　　(4)　　∀y（Fy→b=y）　　　　H（for 1∃E）
5　　　(5)　　Fc＆Gc　　　　　　　　H（for 2∃E）
5　　　(6)　　Fc　　　　　　　　　　　5＆E
5　　　(7)　　Gc　　　　　　　　　　　5＆E
4　　　(8)　　Fa→b=a　　　　　　　　4∀E
4　　　(9)　　Fc→b=c　　　　　　　　4∀E
3,4　　(10)　b=a　　　　　　　　　　　3,8→E
3,4　　(11)　b=c　　　　　　　　　　　5,9→E
3,4　　(12)　a=c　　　　　　　　　　　10,11=E
3,4,5　(13)　Ga　　　　　　　　　　　　7,12=E
4,5　　(14)　Fa→Ga　　　　　　　　　13→I(3)
4,5　　(15)　∀x（Fx→Gx）　　　　　14∀I
2,4　　(16)　∀x（Fx→Gx）　　　　　2,15∃E(5)
1,2　　(17)　∀x（Fx→Gx）　　　　　1,16∃E(4)

∃Eを使用するため仮定する前提の定項に注意。

---

・定理の証明

（定理）　├　∀xy（Pxy⇔x=y）→∀xRxx

1　　　(1)　　∀xy（Pxy⇔x=y）　　　H
1　　　(2)　　Paa⇔a=a　　　　　　　1∀E×2
　　　　(3)　　a=a　　　　　　　　　　　=I
1　　　(4)　　Paa　　　　　　　　　　　2,3BP
1　　　(5)　　∀xRxx　　　　　　　　　4∀I
　　　　(6)　　∀xy（Pxy⇔x=y）→∀xRxx　　　5→I(1)

---

最後にまとめでタブローによる真理値チェックも加える。

（論証）　∀x（Fx→～（Gax⇔∃y（Fy＆（Gyx＆Gxy）））　├　～Fa

【タブロー】

・ステップ１
(1)　　∀x（Fx→～（Gax⇔∃y（Fy＆（Gyx＆Gxy）））
(2)　　Fa

・ステップ２
(1)　　∀x（～Fx∨～Gax⇔∃y（Fy＆（Gyx＆Gxy））
(2)　　Fa

・ステップ３
(2)　　　　　　　　　　Fa
　　　　　　┌───┴─────┐
(1-1)　～Fa　　　　〆～Gaa⇔∃y（Fy＆（Gya＆Gay））
　　　　　×　　　　┌──────┴──────┐
(1-2)　　　　　　～Gaa　　　　　　　　　　　　　　Gaa
　　　　　　　〆∃y（Fy＆（Gya＆Gay））　　〆～∃y（Fy＆（Gya＆Gay））
　　　　　　　　　　　│　　　　　　　　　　　　　〆∀y（～Fy∨～Gya∨～Gay）
(1-3)　　　　　　　Fb　　　　　　　　　┌────┬─┴┐
　　　　　　　　　　Gba　　　　　　　　～Fa　　　～Gaa　～Gaa
　　　　　　　　　　Gab　　　　　　　　　×　　　　　×　　　　×
　　　　　　　　　┌┴────────┐
(1-1：2回目)　～Fb　　　　〆～Gab⇔∃y（Fy＆（Gyb＆Gab））
　　　　　　　　　　×　　　　　　　　　　　　　│
　　　　　　　　　　　┌────────┴─┐
(1-2：2回目)　　～Gab　　　　　　　　　　　　　　Gab
　　　　　　　　∃y（Fy＆（Gyb＆Gby））　　〆～∃y（Fy＆（Gyb＆Gby））
　　　　　　　　　　　×　　　　　　　　　　　　〆∀y（～Fy∨～Gyb∨～Gby）
(1-3：2回目)　　　　　　　　　　　　　┌────┬─┴┐
　　　　　　　　　　　　　　　　　　　　～Fb　　　～Gab　～Gba
　　　　　　　　　　　　　　　　　　　　　×　　　　　×　　　　×
・タブローの結果
全ての経路が閉じたので妥当な論証

【自然演繹】

1　　　(1)　　∀x（Fx→～（Gax⇔∃y（Fy＆（Gyx＆Gxy））））　　A
2　　　(2)　　Fa　　　　　　　　　　　　　　　　　　　　　　　　　　H（for RAA）
1　　　(3)　　Fa→～（Gaa⇔∃y（Fy＆（Gya＆Gay）））　　　1∀E
1,2　　(4)　　～（Gaa⇔∃y（Fy＆（Gya＆Gay）））　　　　　　2,3→E
5　　　(5)　　～∃y（Fy＆（Gya＆Gay））　　　　　　　　　　　　H（for RAA）
5　　　(6)　　～∃y（Fy＆（Gya＆Gay））∨Gaa　　　　　　　　5∨I
5　　　(7)　　∃y（Fy＆（Gya＆Gay））→Gaa　　　　　　　　　6∨→
5　　　(8)　　∀y（～Fy∨～Gya∨～Gay）　　　　　　　　　　5QEとDM
5　　　(9)　　　～Fa∨～Gaa∨～Gaa　　　　　　　　　　　　　　8∀E
2,5　　(10)　　～Gaa∨～Gaa　　　　　　　　　　　　　　　　　　　2,9∨E
2,5　　(11)　　～Gaa　　　　　　　　　　　　　　　　　　　　　　　　10∨Idempotence
2,5　　(12)　　～Gaa∨∃y（Fy＆（Gya＆Gay））　　　　　　　　11∨I
2,5　　(13)　　Gaa→∃y（Fy＆（Gya＆Gay））　　　　　　　　　12∨→
2,5　　(14)　　Gaa⇔∃y（Fy＆（Gya＆Gay））　　　　　　　　　7,13⇔I
1,2　　(15)　　∃y（Fy＆（Gya＆Gay））　　　　　　　　　　　　　4,14RAA(5)
16　　(16)　　Fb＆Gba＆Gab　　　　　　　　　　　　　　　　　　　H（for 15∃E）
16　　(17)　　Fb　　　　　　　　　　　　　　　　　　　　　　　　　　　16＆E
16　　(18)　　Gba　　　　　　　　　　　　　　　　　　　　　　　　　　16＆E
16　　(19)　　Gab　　　　　　　　　　　　　　　　　　　　　　　　　　16＆E
1　　　(20)　　Fb→～（Gab⇔∃y（Fy＆（Gyb＆Gby）））　　　1∀E
1,16　(21)　　～（Gab⇔∃y（Fy＆（Gyb＆Gby）））　　　　　　17,20→E
1,16　(22)　　～Gab⇔∃y（Fy＆（Gyb＆Gby））　　　　　　　　21Neg⇔
1,16　(23)　　～∃y（Fy＆（Gyb＆Gby））　　　　　　　　　　　　19,22BT
1,16　(24)　　∀y（～Fy∨～Gyb∨～Gby）　　　　　　　　　　23QEとDM
1,16　(25)　　～Fa∨～Gab∨～Gba　　　　　　　　　　　　　　24∀E
1,16　(26)　　～Fa∨～Gab　　　　　　　　　　　　　　　　　　　18,25∨E
1,16　(27)　　～Fa　　　　　　　　　　　　　　　　　　　　　　　　19,26∨E
1,2　　(28)　　～Fa　　　　　　　　　　　　　　　　　　　　　　　　15,27∃E(16)
1　　　(29)　　～Fa　　　　　　　　　　　　　　　　　　　　　　　　2,28RAA(2)


【自然演繹】　別の証明ルート

1　　　(1)　　∀x（Fx→～（Gax⇔∃y（Fy＆（Gyx＆Gxy））））　　A
2　　　(2)　　Fa　　　　　　　　　　　　　　　　　　　　　　　　　　H（for RAA）
1　　　(3)　　Fa→～（Gaa⇔∃y（Fy＆（Gya＆Gay）））　　　1∀E
1,2　　(4)　　～（Gaa⇔∃y（Fy＆（Gya＆Gay）））　　　　　　2,3→E
1,2　　(5)　　～Gaa⇔∃y（Fy＆（Gya＆Gay））　　　　　　　　4Neg⇔
1,2　　(6)　　～Gaa→∃y（Fy＆（Gya＆Gay））　　　　　　　　5⇔E
1,2　　(7)　　∃y（Fy＆（Gya＆Gay））→～Gaa　　　　　　　　5⇔E
1,2　　(8)　　Gaa∨∃y（Fy＆（Gya＆Gay））　　　　　　　　　　6∨→
9　　　(9)　　Gaa　　　　　　　　　　　　　　　　　　　　　　　　　　H（for →I）
1,2,9　(10)　～∃y（Fy＆（Gya＆Gay）） 　　　　　　　　　　　　7,9MTT
1,2,9　(11)　∀y（～Fy∨～Gya∨～Gay）　　　　　　　　　　　10QEとDM
1,2,9　(12)　～Fa∨～Gaa∨～Gaa　　　　　　　　　　　　　　11∀E
1,2,9　(13)　～Gaa∨～Gaa　　　　　　　　　　　　　　　　　　　2,12∨E
1,2,9　(14)　～Gaa　　　　　　　　　　　　　　　　　　　　　　　　13∨Idem
1,2　　(15)　Gaa→～Gaa　　　　　　　　　　　　　　　　　　　　14→I(9)
16　　(16)　∃y（Fy＆（Gya＆Gay））　　　　　　　　　　　　　　H（for →I）
1,2,16(17)　～Gaa　　　　　　　　　　　　　　　　　　　　　　　　　7,16→E
1,2　　(18)　∃y（Fy＆（Gya＆Gay））→～Gaa　　　　　　　　17→I(16)
1,2　　(19)　～Gaa　　　　　　　　　　　　　　　　　　　　　　　　8,15,18SimDil
1,2　　(20)　∃y（Fy＆（Gya＆Gay））　　　　　　　　　　　　　　6,19→E
21　　(21)　Fb＆Gba＆Gab　　　　　　　　　　　　　　　　　　　H（for ∃E）
21　　(22)　Fb　　　　　　　　　　　　　　　　　　　　　　　　　　　21＆E
21　　(23)　Gba　　　　　　　　　　　　　　　　　　　　　　　　　　21＆E
21　　(24)　Gab　　　　　　　　　　　　　　　　　　　　　　　　　　21＆E
1　　　(25)　Fb→～（Gab⇔∃y（Fy＆（Gyb＆Gby））） 1∀E
1,21　(26)　～（Gab⇔∃y（Fy＆（Gyb＆Gby））） 　　　　22,25→E
1,16　(27)　～Gab⇔∃y（Fy＆（Gyb＆Gby）） 　　　　　　26Neg⇔
これ以降は上記のものとほぼ同じ手順で証明される

名/項（Names）
名前とは、例えば、"a,b,c,d・・・"である。
(Pa＆Qa)

個体変項（Variables）
変項とは、例えば、 "x,y,z,w,v・・・"である。
∃x（Fx＆Gx）　

例化（Instantiation）
全称量化もしくは存在量化された式の例化は、最初の量化子を外してそれが束縛している変項を名に置き換えることによってなされる。
∀x（Fx＆Gx）をaで例化すると（Fa＆Ga）になり、bで例化すると（Fb＆Gb）になる。

---

推論規則（Primitive Rules of Proof）

普遍記号導入Unversal-Introduction
略記：∀E
説明：普遍量化された式は、どのような名でも例化できる。

1　　(1)　　∀xFx　　　　A
1　　(2)　　Fa　　　　　　1∀E
1　　(3)　　Fb　　　　　　1∀E

普遍記号除去（Universal-Elimination）
略記：∀I
説明：仮定の集合Γにのみ基づいて例化式（例えばFa）を使用し、また、Γにその名（この場合a）が含まれない場合にのみ普遍量化することができる。つまり、前提における全称量化子を例化した文のみ再度全称量化できるということである。この制限を守らない場合は、あらゆる個別事例が一般化可能であるということになってしまう。

1　　　(1)　　∀xFx　　　　　　　　　　A
1　　　(2)　　Fa　　　　　　　　　　　1∀E
1　　　(3)　　∀xFx　　　　　　　　　2∀I
1　　　(4)　　∀yFy　　　　　　　　　2∀I
∀Iを行なう(2)が基づく前提（この場合(1)）に個体定項aが現れてはならない。

・誤用例
1　　　(1)　　∀x（Fx →Gx）　　　　A
2　　　(2)　　Fa　　　　　　　　　　　A
1　　　(3)　　Fa→Ga　　　　　　　1∀E
1,2　　(4)　　Ga　　　　　　　　　　2,3→E
1,2　　(5)　　∀xGx　　　　　　　　4∀I

∀Iを行なう(4)が基づく前提1,2の中で前提2にaがあるためこの全称量化子は成り立たない。

存在記号導入（Existential-Introduction）
略記：∃I
説明：特定の名をもつ式であれば、それを存在量化することができる。

1　　　(1)　　Fa　　　　　　　　　　A
1　　　(2)　　∃xFx　　　　　　　　1∃I

1　　　(1)　　Faaa　　　　　　　　　A
1　　　(2)　　∃xFxaa　　　　　　　1∃I
1　　　(3)　　∃y∃xFxay　　　　2∃I

仮にFaaのように同じよ個体定項をもつ式であったとしても、それぞれを別々に存在量化することができる。もちろん、おなじ変項（∃xFxxx）にすることもできる。

存在記号除去（Existential-Elimination）
略記：∃E
説明：この規則は∃ｘFxからFaを導くものだが、ここには複数の制限があるため、具体例でみたほうがわかりやすい。

1　　(1)　　∃xFx　　　　　　　　　A
2　　(2)　　Fa　　　　　　　　　　　H
2　　(3)　　Fa∨Ga　　　　　　　　2∨I
2　　(4)　　∃x（Fx∨Gx）　　　　3∃I
1　　(5)　　∃x（Fx∨Gx）　　　　1,4∃E(2)

上記のように(2)のFaで(1)の∃xFxを例化している。しかし、この時点では(2)は仮説として導入する。そして、この仮定にもとづいて目的の式β（多くの場合、結論の式）が導けたならば、この前提を消去できるというものである。ただし、βが基づく前提の中に例化した項（この場合a）が含まれていなはならない（その前提自身は除いて）。ようするに、前提に既出の個体定項を使って例化してはならない、同じ個体定項で存在量化を例化してはならない、という点に気をつければよい。

・誤用例
1　　(1)　　∃xFx　　　　　　　　A
2　　(2)　　Fa　　　　　　　　　　H
3　　(3)　　Ga　　　　　　　　　　H
2,3　(4)　　Fa＆Ga　　　　　　　2,3＆I
2,3　(5)　　∃x（Fx＆Gx）　　　　4∃I
1,3　(6)　　∃x（Fx＆Gx）　　　　1,5∃E(2)

(1)を(2)と(3)で例化しているが、同じ項（a）で例化している。そのため、(6)が依存する前提1,3の3にaが含まれており、これは規則に反している。

同一性記号導入（Identity-Introduction）
略記：=I
説明：これは定理なので、α=αの形であれば前提なしで導入することができる。

　　　(1)　　a=a　　　　　　　　　=I

同一性記号除去（Identity- Elimination）
略記：=E
説明：たとえばFaという式と、aを含むイコール記号の式がある場合、このaをイコールで結ばれているもう一方の記号と交換することができる。

1　　(1)　　Ｆａ　　　　　　　　　A
2　　(2)　　a=b　　　　　　　　　A
1,2　(3)　　Fb　　　　　　　　　1,2=E

---

発展規則（Derived Rules）
見やすさのため「┤├」の代わりに「＝」を使用

～∀xPx ＝ ∃x～Rx　　　　　　　　　　　　　　　　Quantified Exchange(QE)
～∃xPx ＝ ∀x～Px　　　　　　　　　　　　　　　　 QE
～∀x～Px ＝ ∀xPx　　　　　　　　　　　　　　　　 QE
～∃x～Px ＝ ∃xPx　　　　　　　　　　　　　　　　 QE
∀xFx ├ ∃xFx
∀x～Fx ├ ∃x～Fx
∀x（Px＆Qx） ＝ ∀xPx＆∀xQx　　　　　　　　＆Confinement(Conf)
∃x（Px＆Qx） ├ ∃xP＆∃xQx　　　　　　　　 ＆Conf
∀xPx∨∀xQx ├ ∀x（Px∨Qx）　　　　　　　　∨Conf
∃x（Px∨Qx） ＝ ∃xPx∨∃xQx　　　　　　　　∨Conf
∀x（Px→Qx） ├ ∀xPx→∀xQx　　　　　　　　→Conf
∀x（Px→Qx） ├ ∃xPx→∃xQx　　　　　　　　→Conf
∃x（Fx→Qx）　＝　∀xPx→∃xQx　　　　　　　　→Conf
∀x（Fx⇔Qx）　├　∀xPx⇔∀xQx　　　　　　　　→Conf
∀x（Px→Q） ＝ ∃xPx→Q　　　　　　　　　　　 →Conf
∃x（Px→Q） ＝ ∀xPx→Q　　　　　　　　　　　 →Conf
∃x（P→Qx） ＝ P→∃xQx　　　　　　　　　　　　→Conf
∀x（P→Qx） ＝ P→∀xQx　　　　　　　　　　　 →Conf

論証の証明（proof）
実際に自然演繹（フィッチスタイルの自然演繹）による論証の証明を行う。例えば、次の妥当な論証の演繹を見る：

（論証）　P∨～R、～R→S、～P　├　S

1　　　（1）　　P∨～R　　　　　　A
2　　　（2）　　～R→S　　　　　　A
3　　　（3）　　～P　　　　　　　　 A
1,3　　（4）　　～R　　　　　　　1,3 ∨E
1,2,3　（5）　　S　　　　　　　　 2,4 →E

手順としては、まず論証で与えられている前提を並べる。上記では、前提「P∨～R、～R→S、～P」を（1）,（2）,（3）に並べている。また、一番左に使用した前提を明記する。そして、これらに前回みた推論規則を使って結論（S）が演繹できることを証明している。これは単純な論証なので、ほとんど頭を悩ます必要はない。問題は、前提を仮説する必要が演繹だ。例えば、次の論証である。

（論証）　～P→P　├　P

1　　　（1）　　　～P→P　　　　　　A
2　　　（2）　　　～P　　　　　　　　H[RAA狙い：矛盾を目指す]
1,2　　（3）　　　～～P　　　　　　1,2MTT
1　　　（4）　　　～～P　　　　　　2,3RAA(2)
1　　　（5）　　　　P　　　　　　　　4DN

この論証は、与えられた前提だけからでは、結論を導くことができない。そのため、前提を自ら仮説する必要がある。だが、仮説した前提は演繹の過程でキャンセルしなければならないのだった。そしてキャンセルを行える推論規則は、→IとRAAの二つだけである。そのため、前提を仮説するときは、これらの規則の使用を見据える必要がある。つまり、RAAを狙う場合は、確実に矛盾が出現する結論の否定を仮説して、矛盾を目指す。→Iを狙う場合は、この規則は前件として仮説した前提をキャンセルできるのだから、求めている式（多くの場合、結論）の前件を仮説する。まとめると：

RAA狙い：結論の否定を仮説して、矛盾を目指す。
→I狙い：（条件文であれば）結論の前件を仮説して後件を目指す。

上記の演繹では結論の否定を仮説して矛盾を導きRAAを使っている。次は→Iのパターンを見てみる：

（論証）　（P∨R）→S、T→～S　├　T→～（P∨R）

1　　　（1）　　（P∨R）→S　　　　　A
2　　　（2）　　T→～S　　　　　　　A
3　　　（3）　　T　　　　　　　　　　　H[→I狙い：後件の～（P∨R）を目指す]
2,3　　（4）　　～S　　　　　　　　　2,3→E
1,2,3　（5）　　～（P∨R）　　　　　1,4MTT（ここで後件がでた）
1,2　　（6）　　T→～（P∨R）　　　5→I（3）

このRAAと→Iの使い方に慣れれば大体の証明は行える。しかし、結論が双条件文の時には注意しておきたい。（α⇔β）の否定式をRAAのために仮説する場合は、（α→β）と（β→α）に分けてそれぞれを否定する。～（α⇔β）で仮説すると、これだけではαとβという式を取り出せないので逆に複雑になる場合が多い。

（論証）　（P∨Q）→（P＆Q）　├　P⇔Q

1　　　（1）　　（P∨Q）→（P＆Q）　　　A
2　　　（2）　　～（P→Q）　　　　　　　　H[RAA狙い：矛盾を目指す]
ここで～（P⇔Q）を仮説しないようにする。
2　　　（3）　　P＆～Q　　　　　　　　　　2Neg→
2　　　（4）　　P　　　　　　　　　　　　　　3＆E
2　　　（5）　　～Q　　　　　　　　　　　　3＆E
2　　　（6）　　P∨Q　　　　　　　　　　　4∨I
1,2　　（7）　　P＆Q　　　　　　　　　　　1,6→E
1,2　　（8）　　Q　　　　　　　　　　　　　7＆E
1　　　(9）　　P→Q　　　　　　　　　　　5,8RAA（2）
同様の手順でQ→Pを演繹する。
1　　　(10)　　　Q→P　　　　　　　　　　RAA
1　　　(11)　　　P⇔Q　　　　　　　　　　9,10⇔I

---

定理（Theorem）
今まで見てきた「論証」は、前提から結論を導くというものだった（A1,A2,A3・・├ C）。しかし、ここでみる「定理」（theorem）は前提を置かずに推論規則だけで導ける式のことである（├ C）。例えば、非矛盾律を証明してみる：

（定理：非矛盾律）　├ ～（P＆～P）

1　　　（1）　　P＆～P　　　　　　　　　　H[RAA狙い：矛盾を目指す]
1　　　（2）　　￢P　　　　　　　　　　　　　1＆E
1,2　　（3）　　P　　　　　　　　　　　　　　1＆E
　　　　（6）　　～（P＆～P）　　　　　　　2,3RAA（1）

このように証明の最後の列に前提を残してはならない（左側は空欄でなければならない）。また、定理の証明は、複数回仮説を置く場合がある。そのため、明確な目的をもって式を仮説しないとただ混乱するだけなので、それなりの注意が必要である。

・前件を仮説する方法

（定理：添加律）　├ P→（Q→P）

1　　　（1）　　P　　　　　　　　　　　　　　H[→I狙い：（Q→P）を目指す]
1　　　（2）　　Q→P　　　　　　　　　　　1TC
　　　　（3）　P→（Q→P）　　　　　　　　2→I（1）

証明する式が条件文や選言文だったら、これの前件を仮説するのが基本である。そして、この前件から後件が導ければ→Iで定理を証明できる。

・前件と後件の否定を仮説する方法

（定理：パースの法則）　├ （（P→Q）→P）→P

1　　　（1）　　（P→Q）→P　　　　　　　H[→I狙い：後件のPを目指す]
2　　　（2）　　￢P　　　　　　　　　　　　　H[RAA狙い：矛盾を目指す]
1,2　　（3）　　～（P→Q）　　　　　　　　1,2MTT
1,2　　（4）　　P＆～Q　　　　　　　　　　3Neg→
1,2　　（5）　　P　　　　　　　　　　　　　　4＆E
1　　　（6）　　P　　　　　　　　　　　　　　2,5RAA（2）
　　　　（7）　（（P→Q）→P）→P　　　　6→I（1）

上記のように、条件文（α→β）の前件からだけでは後件（β）が導けない時は、後件の否定（～β）を仮説して矛盾を目指す。そして、矛盾がでたらRAAで後件の否定を否定して後件（β）を出して、これを→Iする。これは～（α→β）を仮説してNeg→を経てRAAを狙っても同じことだが、→Iの使い方にも慣れておいたほうがいい。

・部分式を別々に証明する方法

（定理）　├　（（P→R）→Q）⇔（（～P→Q）＆（R→Q））
　　　　　　　これの→方向の証明だけ行なう

1　　　（1）　　（P→R）→Q　　　H[→Iの後件（～P→Q）＆（R→Q）を目指す]
次に後件を求めるわけだが、RAA狙いで（（～P→Q）＆（R→Q））をそのまま否定したのでは、うまく式をばらすことができない。そのため、これの連言肢（（～P→Q）と（R→Q））を個々に導く（これらに★をつける）。
2　　　（2）　　　～P　　　　　　　　H[→I狙い：Qを目指す]
3　　　（3）　　　～Q　　　　　　　 H[RAA狙い]
1,3　　（4）　　 ～（P→R）　　　　1,3MTT
1,3　　（5）　　 P＆～R　　　　　　4Neg→
1,3　　（6）　　　P　　　　　　　　　　5＆E
1,2　　（7）　　　Q　　　　　　　　　　2,6RAA（3）
1　　　（8）　　 ～P→Q　　　　　　7→I(2)★
9　　　（9）　　　R　　　　　　　　　　H[→I狙い：Qを目指す]
10　　（10）　　～Q　　　　　　　　　H[RAA狙い]
1,10　（11）　　～（P→R）　　　　　1,10MTT
1,10　（12）　　 P＆～R　　　　　　11Neg→
1,10　（13）　　 ～R　　　　　　　　12＆E
1,9　　(14）　　 　Q　　　　　　　　　9,13RAA（10）
1　　　（15）　　 R→Q　　　　　　　14→I（9）★
1　　　（16）　（～P→Q）＆（R→Q）　8,15＆I
　　　　(17）　（（P→R）→Q）→（（～P→Q）＆（R→Q））　16→I(1)

～（α→β）や～（α∨β）の式はNeg→やDMを使えば連言式にできるため、αとβに分けることができる。しかし、～（α＆β）や～（α⇔β）という式はこれだけではαやβに分けることができない。そのため、上記のように、部分式を別々に証明するという方法をとる。

・ディレンマを狙う方法
（α∨β）や（α→β）の式は部分式にばらすことができない。そのため、これで行き詰まったらディレンマ（構成的両刀論法など）を使う。上記の論証をディレンマで証明してみる。

（定理）　├　（論証）　（P∨Q）→（P＆Q）　├　P⇔Q

1　　　（1）　　（P∨Q）→（P＆Q）　　　A
2　　　（2）　　～（P⇔Q）　　　　　　　　H[RAA狙い：矛盾を目指す]
2　　　（3）　　～P⇔Q　　　　　　　　　　2Neg⇔
2　　　（4）　　～P→Q　　　　　　　　　　3⇔E
2　　　（5）　　Q→～P　　　　　　　　　　3⇔E
2　　　（6）　　P∨Q　　　　　　　　　　　4∨→
7　　　（7）　　P　　　　　　　　　　　　　H[for →I狙いで（P&Q）を目指す（ディレンマ狙い）]
7　　　（8）　　P∨Q　　　　　　　　　　　7∨I
1,7　　(9）　　P＆Q　　　　　　　　　　　1,8→E
1　　　(10)　　（P∨Q）→（P＆Q）　　　9→I(7)
11　　(11)　　　Q　　　　　　　　　　　　H[for →I狙いで（P&Q）を目指す（ディレンマ狙い）]
11　　(12)　　P∨Q　　　　　　　　　　　11∨I
1,11　(13）　　P＆Q　　　　　　　　　　　1,12→E
1　　　(14)　　（P∨Q）→（P＆Q）　　　13→I(11)
1,2　　(15)　　P＆Q　　　　　　　　　　　6,10,14SimDil
1,2　　(16)　　Q＆P　　　　　　　　　　　＆Comm
2　　　(17)　　～（Q＆P）　　　　　　　　5Neg→
1　　　(18)　　P⇔Q　　　　　　　　　　　17,18RAA(2)

証明の手順が最初から見通せていれば、「部分式を別々に証明する方法」のほうが分かりやすくわざわざディレンマを使う必要はない。しかし、ディレンマは論証の途中で行き詰まった時に使える有用な方法。

---

統語論と意味論における論理的真理
意味論における論理的真理であるトートロジー（恒真命題）は、タブローによってチェックされるのだった。そして、ある式αがトートロジーである場合、　（├= α）と表記される。そして、上で見てきた統語論における論理的真理は定理（theorem）である。なぜなら、定理はいかなる前提も置かずに純粋に推論規則だけで導き出せる式であるからだ。定理は（├ α）と表記される。

意味論的真理＝トートロジー（├= α）
統語論的真理＝定理（├ α）

そして、この2つの真理の集合は一致している。この「├=Γ⇔├Γ」を証明するのが完全性定理である。

・論証
また、妥当な論証もまたタブローによって妥当性を確かめられるのる。そして、妥当な論証には自然演繹でそれを証明することができる。つまり、「A1、A2、・・An　├=　C」という論証がタブローによって妥当であることが確かめれたならば、この論証は統語論において証明を与えることができる。「A1、A2、・・An　├　C」。この妥当な論証とは反例（前提が真で結論が偽というパターン）がない論証のことである。そのため、論証を一つの式「（Γ＆A）→Δ）」とした場合、これはトートロジー（恒真命題）である（├=（Γ＆A）→Δ）。

自然演繹
以前概観した形式論理学の意味論的方法（タブロー）により論証の妥当性を確認することができた。だが、実際にその妥当な論証の過程、つまり、前提から結論を導く演繹の過程はどのようになっているか。この論証を証明するするのが統語論における自然演繹（Natural Deduction（ND））である（※１）。

・論証の評価手続き＝タブロー
・論証の構成手続き＝自然演繹

---

推論規則
自然演繹は、次の推論規則を使って行われる。

仮定の法則（Rule of Assumption）
略記：A、H
説明：いかなる命題でも前提として仮定することができる。前提は、与えられた論証の前提（Assumption（A））と証明に必要なための仮設する前提（Hypothesis（H））を区別すると混乱しないでよい。Hは証明の道中でキャンセル／dhischargeする必要がある。また、前提をキャンセルすることのできる法則はRAAと→Iの二つだけなので、常に新しい前提を導入するときは、この二つの法則のどちらかを使用することを見据える。

連言導入（Conjunction Introduction）
略記：＆I
他の名称：Ampersand Introduction
説明：上記にある二つの命題を＆でつなぐ事ができる。

1　　　(1)　　P　　　　　　　A
2　　　(2)　　Q　　　　　　　A
1,2　　(3)　　P＆Q　　　　　1,2 ＆I
1　　　(5)　　P＆P　　　　　1,1 ＆I

連言除去（Conjunction Elimination）
略記：＆E
他の名称：Ampersand Elimination、Simplification
説明：連言命題はその連言肢を個々の式に分けることができる。

1　　　(1)　P＆Q　　　　　　A
1　　　(2)　Q　　　　　　　1＆E
1　　　(3)　P　　　　　　　1＆E

選言導入（Disjunction Introduction）
略記：∨I
他の名称：Wedge-Introduction、Addition(ADD)
説明：選言でいかなる命題も導入することができる。

1　　　(1)　　　P　　　　　　　　　　　　A
1　　　(1)　　　P∨Q　　　　　　　　　1∨I
1　　　(1)　　(P⇔～Q＆R)∨P　　　　1∨I

選言除去（Disjunction Elimination）
略記：∨E
他の名称：Wedge Elimination、Modus Tollendo Pones、Disjunctive Syllogism
説明：選言命題とその中の一つの選言肢の否定によって、もう一方の選言肢が導くことができる。

1　　　(1)　P∨Q　　　　　　　　　　A
2　　　(2)　～P　　　　　　　　　　　　A
1,2　　(3)　Q　　　　　　　　　　　1,2∨E

条件的証明（Arrow-Introduction）
略記：→I
他の名称：Conditional Proof(CP)
説明：二つの式が得られたならば、それらで条件文を作ることができる。だが、条件文の前件は仮説した前提（H）でなけれなならず、そして、→Iの使用によりその前提はキャンセルされる。

1　　　(1)　　～P∨Q　　　　　　　　　A
2　　　(2)　　P　　　　　　　　　　　　H
1,2　　(3)　　Q　　　　　　　　　　　1,2∨E
1　　　(4)　　P→Q　　　　　　　　　3→I(2)

前件肯定（Modus Ponens）
略記：→E、MP
他の名称：Arrow-Elimination, Detachment, Affirming the Antecedent
説明：条件文（φ→Ψ）とこれの前件（φ）が得られた場合、これの後件（Ψ）を得ることができる。

1　　　(1)　　P→Q　　　　　　　　　A
2　　　(2)　　P　　　　　　　　　　　　A
1,2　　(3)　　Q　　　　　　　　　　　1,2→E

背理法（Reductio ad absurdum）
略記：RAA
他の名称：帰謬法、間接証明（Indirect Proof (IP)）、～導入（～Intro）/（～除去）～Elim
説明：ある式とそれの否定（つまり矛盾）が出現した場合、任意の前提を否定し、かつ、その前提をキャンセルことができる。下の例で、3に背理法を使用しており、そして、前提3がキャンセルされているのが分かる。

1　　　(1)　　P→Q　　　　　　　　　A
2　　　(2)　　～Q　　　　　　　　　　　A
3　　　(3)　　P　　　　　　　　　　　　H
1,3　　(4)　　Q　　　　　　　　　　　1,3→E
1,2　　(5)　　～P　　　　　　　　　　2,4 RAA (3)

双条件法導入（Double-Arrow-Introduction）
略記：⇔I
説明：（φ→ψと（ψ→φ） という二つの命題がすでに得られている場合、これらを双条件法で導入することできる。P⇔Qは（（P→Q）＆（Q→P））なので、⇔Iは＆Iと同じものである。

1　　(1)　　P→Q　　　　　　　　　　　A
2　　(2)　　Q→P　　　　　　　　　　　A
1,2　(3)　　P⇔Q　　　　　　　　　1,2⇔I
1,2　(4)　　Q⇔P　　　　　　　　　1,2⇔I

双条件法除去（Double-Arrow-Elimination）
略記：⇔E
説明：（φ⇔ψ）は（φ→ψ）、もしくは／そして、（ψ→φ）に分けることができる。これも＆Eで理解できる。.

1　　(1)　　P⇔Q　　　　　　　　　　A
2　　(2)　　P→Q　　　　　　　　　1⇔E
1,2　(3)　　Q→P　　　　　　　　　1⇔E

---

発展法則/同値定理（Derived rules）
これらは定理なので一つの式にする場合は「 ┤├ 」を「⇔」、「├」を「→」に置き換える。

P ┤├ ～～P　　　　　　　　　　　　　　Double Negation (DN)/二重否定律
P→Q, ～Q ├ ～P　　　　　　　　　　Modus Tollendo Tollens (MTT)/後件否定
P→Q, Q→R ├ P→R　　　　　　　Hypothetical Syllogism (HS)/推移律・仮言三段論法
P ├ Q→P　　　　　　　　　　　　　　True Consequent （TC)/添加律
～P ├ P→Q　　　　　　　　　　　　　False Consequent (FC)
P→Q, P→～Q ├ ～P　　　　　　　 Impossible Antecedent (IA)
～P∨Q ┤├ P→Q　　　　　　　　　　Wedge Arrow (∨→)/実質条件法律
P∨Q, P→R, Q→R ├ R　　　　　　Simple Dilemma (SimDil)/構成的両刀論法
P∨Q, P→R, Q→S ├ R∨S　　　Complex Dilemma(ComDil)
P→Q, ～P→Q ├ Q　　　　　　　　　Special Dilemma
～(P＆Q) ┤├ ～P∨～Q　　　　　　　De Morgan's laws(DM)/ド・モルガンの法則
～(P→Q) ┤├ P＆～Q　　　　　　　　Negated Arrow (Neg→)
P＆Q ┤├ Q＆P　　　　　　　　　　　＆Commutativity (＆Comm)/交換律
P∨Q ┤├ O∨P　　　　　　　　　　　∨Commutativity (∨Comm)/交換律
P⇔Q ┤├ Q⇔P　　　　　　　　　　　⇔Commutativity (⇔Comm)
P ┤├ P＆P　　　　　　　　　　　　　　＆Idempotence（＆Idem）/同文反復律
P ┤├ P∨P　　　　　　　　　　　　　　∨Idempotence（∨Idem）/同文反復律
P→Q ┤├ ～Q→～P　　　　　　　　　Transposition (Trans)/対偶律
P＆(Q＆R) ┤├ (P＆Q)＆R　　　　＆Associativity (＆Assoc)/結合律
P∨(Q∨R) ┤├ (P∨Q)∨R　　　　∨Associativity (∨Assoc)/結合律
P＆(Q∨R) ┤├ (P＆Q)∨(P＆R)　　＆/∨Distribution(＆/∨Dist)/分配律
P∨(Q＆R) ┤├ (P∨Q)＆(P∨R)　　∨/＆Distribution(∨/＆Dist)/分配律
P→(Q→R) ┤├ (P＆Q)→R　　　　　Imp/Exportation　(Imp/Exp)/移入律・移出律
P⇔Q,P ├ Q　　　　　　　　　　　　　Biconditional Ponens(BP)
P⇔Q,～P ├ ～Q　　　　　　　　　　　Biconditional Tollens (BT)
P⇔Q ┤├ ～Q⇔～P　　　　　　　　　　BiTransposition(BiTrans)
～(P⇔Q) ┤├ ～P⇔Q　　　　　　　　　Negated⇔(Neg⇔)

---

※１
統語論の体系は、大きく三つに分けられる：公理的方法、論理計算LK、自然演繹ND。後者の二つはゲンツェンによって体系化されたもので、NDはLKをより日常的な推論の形に近づけたものである。