コンテンツへスキップ
Topos Uranos
日本語

演繹：まとめと挑戦課題

要約

この課は、演繹を扱う単元を締めくくる。ウカシェヴィチの体系の定義（三つの公理図式とモーダス・ポネンス）から、演繹定理と、否定論理和の言語におけるこの体系の限界へ、そこから四つの基本技法と、本コースの体系を完成させる二重否定の置換の規則へ、否定論理和の基本補題から同値なものの置換と対称性へ、さらにそこから古典論理の規則と、ド・モルガンの法則および分配法則へと至る演繹の鎖を組み立て直し、各環でどの結果が使われ、それがどの課で証明されるかを示す。単元が証明したものと認めたものを区別し、達成したことをコースの計画に照らして位置づけ、単元が未解決のまま残す問い、すなわち導出可能なものが真なるものと一致するかという問いが、なぜ意味論の単元へ導くのかを説明する。まとめテストでは導入テストの技能を繰り返し、最後に、各課の問題より難しく、複数の課の道具を組み合わせることを求める六つの挑戦課題で終わる。

学習目標

  1. 単元の結果の論理的な順序を組み立て直し、各結果がよりどころとする先行する結果と、それが証明される課を特定する。
  2. 演繹定理、二重否定、二重否定の置換の規則、対偶、基本補題、同値なものの置換がどのようにつながるか、そしてなぜ古典的な規則とド・モルガンの法則および分配法則がそれらに依存するのかを説明する。
  3. 単元が証明したものを、認めたもの（公理図式、二つの原始規則、累積帰納法、構造帰納法、一意読み取り可能性）や、後の単元に残したもの、とくに演繹と真理の関係から区別する。
  4. 標識、二重否定の置換の規則、演繹定理、場合分けによる証明、背理法、同値なものの置換、ド・モルガンの法則と分配法則を組み合わせる問題を解く。

単元で達成したこと

この単元は、前の単元の言語に演繹体系を、すなわち論理式からほかの論理式を得る純粋に構文論的な方法を与え、その体系によって、数学が推論に用いる技法を一行ずつ証明することを目指した。この目的は、それぞれその場で明示したわずかな留保つきで果たされた。三つの公理図式と二つの原始規則は、証明されるのではなく選ばれるものであり、その選択が適切かどうかは、単元が提起しながら完全には答えていない問いである。累積帰納法、構造帰納法、一意読み取り可能性、再帰による定義は、前の単元で証明され、ここで用いられる。そして集合論の欠かせない部分（部分集合、和集合、有限集合）は、必要なところで思い出した。これらの留保のもとで、たどってきた道は、四つの区間からなる一本の演繹の鎖として読むことができる。

ウカシェヴィチの体系とその限界

形式的演繹体系の課は、体系を、言語、いくつかの公理、いくつかの規則として定義した。いずれも記号列を見るだけで確かめられるものである。そして本コースの体系の第一段階であるウカシェヴィチの体系を定めた。図式 A1、A2、A3 と、唯一の規則としてのモーダス・ポネンスであり、一意読み取り可能性によってこの規則はあいまいさなく適用できる。この課は、前提の集合 Γ\Gamma からの演繹と関係 Γ⊢φ\Gamma \vdash \varphi を定義し、⊢(φ→φ)\vdash (\varphi \rightarrow \varphi) を五行で導き、構造的性質、すなわち反射性、単調性、演繹どうしのモーダス・ポネンス、カット、有限性を証明した。これらと行数に関する累積帰納法によって、演繹定理とその逆を証明した。演繹定理の第二の場合は、あらかじめ (φ→φ)(\varphi \rightarrow \varphi) を導いておくことを必要とする。そこから、反射的、対称的、推移的な証明可能な同値を得た。最後に、この体系の限界を確立した。値 00 と 11 をとる標識は、原始的な形 (α↓β)(\alpha \downarrow \beta) の上で再帰によって定義され、否定と含意を通常どおりに扱い、A1、A2、A3 とモーダス・ポネンスによって保たれ、(v1↓v2)(v_{1} \downarrow v_{2}) のような論理式の値を自由のまま残す。このことから、((v1↓v2)→¬v1)((v_{1} \downarrow v_{2}) \rightarrow \neg v_{1}) はウカシェヴィチの体系の定理ではなく、(v1↓v2)(v_{1} \downarrow v_{2}) からは (¬¬v1↓v2)(\neg\neg v_{1} \downarrow v_{2}) が導かれず、逆も導かれない。どの標識も θ\theta と ¬¬θ\neg\neg\theta に同じ値を与えるので、この課はさらに、二重否定でさえ、証明されたとしても、この限界を解消しないことを指摘した。

四つの技法と新しい規則

四つの演繹技法の課は、まず「結果から規則へ」の補題を証明した。{α1,…,αn}⊢β\{\alpha_{1}, \ldots, \alpha_{n}\} \vdash \beta ならば、同じ結論は任意の集合 Γ\Gamma から得られる。ただしそれが各 αi\alpha_{i} を導くとする。さらに ⊢(α1→(α2→⋯(αn→β)⋯ ))\vdash (\alpha_{1} \rightarrow (\alpha_{2} \rightarrow \cdots (\alpha_{n} \rightarrow \beta) \cdots)) も成り立つ。各技法を三つの提示のしかた（前提から、定理として、規則として）で使えるのはこの補題による。対称性の課とド・モルガンの課は、同値の連鎖をカットと組み合わせるが、そのために第一の課の証明可能な同値の性質に依拠している。これは同じ考えを一つの前提に適用したものである。鎖の中では、各結果は証明される場所に一度だけ現れる。この補題を用いて、この課は、A1 と A2 から七行で仮言三段論法を、演繹定理によって前提の交換を、二重否定を（その第一の向きは A1 で作った含意に A3 を二回適用し、第二の向きは第一の向きを ¬φ\neg\varphi に適用して A3 を用いる）、そして三つの形の対偶を導いた。三つの形は、含意の否定を三通りに配分する。この四つはすでにウカシェヴィチの体系で成り立つ。

二重否定を証明したうえで、この課は第二の原始規則、二重否定の置換（二重否定置換）によって本コースの体系を完成させた。χ\chi から χ′\chi' を推論してよいのは、χ′\chi' が、χ\chi において部分論理式 θ\theta の一つの出現を ¬¬θ\neg\neg\theta で、または ¬¬θ\neg\neg\theta の一つの出現を θ\theta で置き換えて得られるときである。この規則は要請しなければならない。標識 m1m_{1} は二重否定の定理に 11 を与えるにもかかわらず、(v1↓v2)(v_{1} \downarrow v_{2}) と (¬¬v1↓v2)(\neg\neg v_{1} \downarrow v_{2}) を区別するからである。二重否定置換は m1m_{1} を保たないので導出可能なものを広げるが、誠実な標識は保つので、広げすぎることはない。規則は基本言語の記号列に作用し、そこでは否定がその引数を二重にする。(φ→ψ)(\varphi \rightarrow \psi) は部分論理式 ¬φ\neg\varphi を二回含み、その前件の前に二重否定を付けるには二回の適用が必要になる。同じ観察が演繹定理の拡張を支えている。ある行が規則によって得られるとき、帰納法の仮定は後件が前の行である含意を与え、その後件のコピーごとに一回ずつ、規則を二回適用すれば、求める含意が得られる。ほかの構造的性質は同じ証明で成り立つ。最初の帰結は、論理式は規則によってそれから得られるすべての論理式と同値であること、とくに (φ↓ψ)⊣⊢(¬¬φ↓ψ)(\varphi \downarrow \psi) \dashv\vdash (\neg\neg\varphi \downarrow \psi) と (φ↓ψ)⊣⊢(φ↓¬¬ψ)(\varphi \downarrow \psi) \dashv\vdash (\varphi \downarrow \neg\neg\psi) であること、そして対応する含意は、ほかの体系では公理とされるが、ここでは定理であることである。

結合子と置換

結合子の対称性の課は、白丸と黒丸の言語に固有の困難に取り組んだ。ウカシェヴィチの公理は否定と含意についてしか語らず、否定論理和はほとんどどれも、そのどちらでもない。基本補題 (φ↓ψ)⊣⊢¬(¬φ→ψ)(\varphi \downarrow \psi) \dashv\vdash \neg(\neg\varphi \rightarrow \psi) が橋を架ける。¬(¬φ→ψ)\neg(\neg\varphi \rightarrow \psi) は ¬¬(¬¬φ↓ψ)\neg\neg(\neg\neg\varphi \downarrow \psi) であるから、二重否定置換の規則が内側の二重否定を付け、二重否定が外側の二重否定を付ける。逆向きには、二重否定と規則がそれらを外す。これを用いて、同値なものの置換は、まず否定のもとと含意の両辺で対偶と仮言三段論法によって証明され、否定論理和の両方の引数へ、さらにそこから選言と連言へと拡張された。規則と置換は互いを不要にしない。規則は θ\theta と ¬¬θ\neg\neg\theta を入れ替えるだけであるが、置換は任意の同値な論理式を許す。そして基本補題で証明された置換は、今度は規則に依拠している。この課は次に、ほかの教科書が定義とみなす形が同値であることを証明した。(φ∨ψ)⊣⊢(¬φ→ψ)(\varphi \vee \psi) \dashv\vdash (\neg\varphi \rightarrow \psi) は規則の二回の適用を必要とし、外側の否定が作るコピーごとに一回ずつ適用する。(φ∧ψ)⊣⊢(¬φ↓¬ψ)(\varphi \wedge \psi) \dashv\vdash (\neg\varphi \downarrow \neg\psi) は二重否定を必要とする。これに対して、(φ∧ψ)(\varphi \wedge \psi) と ¬(φ→¬ψ)\neg(\varphi \rightarrow \neg\psi) は同じ記号列である。最後に、定義が課す順序で五つの対称性を証明した。否定論理和の対称性は基本補題と対偶で、残りはそれぞれ直前のもので証明し、必要なときには否定のもとの置換で移す。

古典的な規則と法則

古典論理の技法の課は、すべて行から行へ持ち越される前提の集合 Γ\Gamma のもとで、選言と連言の導入と除去、排中律と無矛盾律、爆発律、二つの形の背理法、そして論理式とその否定による場合分けと任意の選言による場合分けを証明した。依存の順序は厳密である。爆発律は選言の規則に、古典的な背理法は爆発律と A3 に、場合分けによる証明は対偶と背理法に依存する。これらの証明のどれも二重否定置換の規則を直接には持ち出さない。規則は別形と同値なものの置換を通じて働く。ド・モルガンの法則と分配法則の課は、これらの規則をともに働かせた。ド・モルガンの第一法則は連言の定義と二重否定から得られる。第二法則は否定論理和の内側に入ることを要し、そこで二重否定置換の規則が、各引数に一回ずつ、対称性を必要とせずに二回介入する。そこから、(φ↓ψ)(\varphi \downarrow \psi) は (¬φ∧¬ψ)(\neg\varphi \wedge \neg\psi) と同値であることが、すなわち前の単元が約束として定めた読み「φ\varphi でも ψ\psi でもない」が従う。変種には ¬(φ→ψ)⊣⊢(φ∧¬ψ)\neg(\varphi \rightarrow \psi) \dashv\vdash (\varphi \wedge \neg\psi) も含まれる。二つの分配法則は場合分けによって両方の向きに証明され、それぞれの向きで適した形の場合分けが選ばれた。

次の図は、四つの区間を一本の鎖にまとめたものである。列の各節点は定義か結果で、論理的な順序で番号が付き、その証明が用いる前の環と弧で結ばれている。そのまわりに浮かぶのが支え、すなわち鎖が何度も立ち返る原理と道具であり、それぞれはよりかかる環と実線で、確立される環と点線で結ばれる。ただし、この鎖が証明しないもの（認められる公理図式と、前の単元の道具）は輪として描かれる。二重否定の置換の規則は、やはり証明なしに認められるが、それを導入する環と結ばれている。そこで、なぜそれを要請しなければならないかが説明されるからである。支えを押すと、それを使うすべての環が強調され、各環はそれが証明される課へのリンクになっている。演繹定理と二重否定が、公理に次いで単元で最もよく使われる支えであること、そして新しい規則が、単元が否定論理和について述べることのすべて、すなわち拡張された演繹定理、基本補題、別形、ド・モルガンの第二法則を支えていることに注意しよう。

鎖の支え

  • A一意読み取り可能性と再帰. ∙φψ=∙φ′ψ′\sigI\varphi\psi = \sigI\varphi'\psi' であり、四つの記号列がすべて論理式ならば、φ=φ′\varphi = \varphi' かつ ψ=ψ′\psi = \psi' である。したがって、∙φψ\sigI\varphi\psi の値を、φ\varphi と ψ\psi とそれらの値から計算する規則は、論理式の上のただ一つの関数を定義する。前の単元で証明した。 この単元では証明なしに認める。
  • B累積帰納法. ある性質が、ある自然数より小さいすべての自然数について成り立つたびにその自然数について成り立つならば、その性質はすべての自然数について成り立つ。前の単元で単純な帰納法から導き、ここでは演繹の行数に適用する。 この単元では証明なしに認める。
  • Cウカシェヴィチの公理. 図式 A1 は (φ→(ψ→φ))(\varphi \rightarrow (\psi \rightarrow \varphi))、A2 は ((φ→(ψ→χ))→((φ→ψ)→(φ→χ)))((\varphi \rightarrow (\psi \rightarrow \chi)) \rightarrow ((\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \chi)))、A3 は ((¬ψ→¬φ)→(φ→ψ))((\neg\psi \rightarrow \neg\varphi) \rightarrow (\varphi \rightarrow \psi)) である。認めるものとする。 この単元では証明なしに認める。
  • D二重否定の置換. 本コースの体系の第二の原始規則。χ\chi から χ′\chi' を推論してよいのは、χ′\chi' が χ\chi から、部分論理式 θ\theta の一つの出現を ¬¬θ\neg\neg\theta で、または ¬¬θ\neg\neg\theta の一つの出現を θ\theta で置き換えて得られるときである。二重否定を証明した後に要請する。 確立される環: 8. 二重否定の置換.
  • E演繹定理. Γ∪{φ}⊢ψ\Gamma \cup \{\varphi\} \vdash \psi であるのは Γ⊢(φ→ψ)\Gamma \vdash (\varphi \rightarrow \psi) であるとき、かつそのときに限る。ウカシェヴィチの体系で証明され、本コースの体系でも、場合を一つ加えて成り立つ。 確立される環: 3. 演繹定理と証明可能な同値.
  • F結果から規則へ. {α1,…,αn}⊢β\{\alpha_{1}, \ldots, \alpha_{n}\} \vdash \beta であり、Γ⊢αi\Gamma \vdash \alpha_{i} がすべての ii について成り立つならば、Γ⊢β\Gamma \vdash \beta である。前提から証明されたすべての技法は、任意の前提の集合のもとで適用できる。 確立される環: 5. 結果から規則へ.
  • G二重否定. φ⊣⊢¬¬φ\varphi \dashv\vdash \neg\neg\varphi。定理 ⊢(¬¬φ→φ)\vdash (\neg\neg\varphi \rightarrow \varphi) と ⊢(φ→¬¬φ)\vdash (\varphi \rightarrow \neg\neg\varphi) を伴う。 確立される環: 7. 二重否定.
  • H同値なものの置換. φ⊣⊢φ′\varphi \dashv\vdash \varphi' ならば、φ′\varphi' を φ\varphi の代わりに、否定のもとで、含意、否定論理和、選言、連言の両辺で、同値を損なうことなく置くことができる。 確立される環: 12. 同値なものの置換.

  1. 第 1 区間 ウカシェヴィチの体系とその限界

    • 図式の代入例を見分け、論理式の並びが前提の集合からの演繹であるかどうかを判定する。
    • 演繹の構造的性質と演繹定理を、行数に関する累積帰納法で証明する。
    • 反射性、単調性、カット、演繹定理とその逆を用いて、演繹についての演繹を組み立てる。
    • 公理とモーダス・ポネンスが保つ標識によって論理式が導かれないことを証明し、それを用いてウカシェヴィチの体系の限界を説明する。

    1. 体系、演繹、同一律. ウカシェヴィチの体系の公理は A1 から A3 の一様代入例であり、その唯一の規則はモーダス・ポネンスである。Γ⊢φ\Gamma \vdash \varphi であるとは、φ\varphi で終わる有限の論理式の並びがあって、その各論理式が公理、Γ\Gamma の要素、または前の二つからモーダス・ポネンスで得られたものであることをいう。最初の定理 ⊢(φ→φ)\vdash (\varphi \rightarrow \varphi) は A1 と A2 によって五行で導かれる。

      支え: A (一意読み取り可能性と再帰), C (ウカシェヴィチの公理). 証明される授業: 形式的演繹体系.

    2. 構造的性質. φ∈Γ\varphi \in \Gamma ならば Γ⊢φ\Gamma \vdash \varphi。Γ⊆Δ\Gamma \subseteq \Delta かつ Γ⊢φ\Gamma \vdash \varphi ならば Δ⊢φ\Delta \vdash \varphi。Γ⊢φ\Gamma \vdash \varphi と Γ⊢(φ→ψ)\Gamma \vdash (\varphi \rightarrow \psi) から Γ⊢ψ\Gamma \vdash \psi が従う。Γ⊢φi\Gamma \vdash \varphi_{i} がすべての ii について成り立ち、Γ∪{φ1,…,φr}⊢ψ\Gamma \cup \{\varphi_{1}, \ldots, \varphi_{r}\} \vdash \psi ならば、Γ⊢ψ\Gamma \vdash \psi。そして Γ⊢φ\Gamma \vdash \varphi ならば、Γ\Gamma のある有限部分集合で足りる。

      使う結果: 1. 体系、演繹、同一律. 証明される授業: 形式的演繹体系.

    3. 演繹定理と証明可能な同値. Γ∪{φ}⊢ψ\Gamma \cup \{\varphi\} \vdash \psi であるのは Γ⊢(φ→ψ)\Gamma \vdash (\varphi \rightarrow \psi) であるとき、かつそのときに限る。行数に関する累積帰納法により、A1、A2、同一律を用いて証明される。このことから、証明可能な同値 φ⊣⊢ψ\varphi \dashv\vdash \psi は反射的、対称的、推移的であり、同値な二つの論理式は同じ集合から導かれる。

      使う結果: 1. 体系、演繹、同一律, 2. 構造的性質. 支え: B (累積帰納法), C (ウカシェヴィチの公理). 証明される授業: 形式的演繹体系.

    4. ウカシェヴィチの体系の限界. 再帰によって定義された、値 00 と 11 をとる標識は m(¬φ)=1−m(φ)m(\neg\varphi) = 1 - m(\varphi) と m((φ→ψ))=1−m(φ)(1−m(ψ))m((\varphi \rightarrow \psi)) = 1 - m(\varphi) \left( 1 - m(\psi) \right) を満たし、A1、A2、A3 とモーダス・ポネンスは標識 11 を保つ。したがって、((v1↓v2)→¬v1)((v_{1} \downarrow v_{2}) \rightarrow \neg v_{1}) はウカシェヴィチの体系の定理ではなく、{(v1↓v2)}⊬(¬¬v1↓v2)\{(v_{1} \downarrow v_{2})\} \nvdash (\neg\neg v_{1} \downarrow v_{2}) であり、逆も成り立たない。どの標識も二重否定に 11 を与えるので、置換は要請しなければならない。

      使う結果: 1. 体系、演繹、同一律. 支え: A (一意読み取り可能性と再帰), B (累積帰納法), C (ウカシェヴィチの公理). 証明される授業: 形式的演繹体系.

  2. 第 2 区間 四つの技法と新しい規則

    • 前提からの結果を、定理と、任意の前提の集合のもとで適用できる規則とに変える。
    • 含意をつなぎ、前件を並べ替え、二重否定を付けたり外したりし、各含意に対応する対偶の形を選ぶ。
    • 二重否定の置換の規則を、略記が隠す出現を突き止め、否定が作るコピーごとに繰り返して適用する。
    • 規則がなぜ要請されるのかを標識で説明し、演繹定理がその規則のもとでも成り立つことを証明する。

    1. 結果から規則へ. {α1,…,αn}⊢β\{\alpha_{1}, \ldots, \alpha_{n}\} \vdash \beta ならば、Γ⊢α1\Gamma \vdash \alpha_{1}、…\ldots、Γ⊢αn\Gamma \vdash \alpha_{n} から Γ⊢β\Gamma \vdash \beta が従い、さらに ⊢(α1→(α2→⋯(αn→β)⋯ ))\vdash (\alpha_{1} \rightarrow (\alpha_{2} \rightarrow \cdots (\alpha_{n} \rightarrow \beta) \cdots)) である。とくに、α⊣⊢α′\alpha \dashv\vdash \alpha' ならば、Γ⊢α\Gamma \vdash \alpha であるのは Γ⊢α′\Gamma \vdash \alpha' であるとき、かつそのときに限る。

      使う結果: 2. 構造的性質. 支え: E (演繹定理). 証明される授業: 四つの演繹技法.

    2. 仮言三段論法と交換. {(φ→ψ),(ψ→χ)}⊢(φ→χ)\{(\varphi \rightarrow \psi), (\psi \rightarrow \chi)\} \vdash (\varphi \rightarrow \chi)。A1 と A2 からの七行の演繹による。そして {(φ→(ψ→χ))}⊢(ψ→(φ→χ))\{(\varphi \rightarrow (\psi \rightarrow \chi))\} \vdash (\psi \rightarrow (\varphi \rightarrow \chi))。

      使う結果: 1. 体系、演繹、同一律. 支え: C (ウカシェヴィチの公理), E (演繹定理), F (結果から規則へ). 証明される授業: 四つの演繹技法.

    3. 二重否定. ⊢(¬¬φ→φ)\vdash (\neg\neg\varphi \rightarrow \varphi) は、A1 が ¬¬φ\neg\neg\varphi から作る含意に A3 を二回適用して得る。⊢(φ→¬¬φ)\vdash (\varphi \rightarrow \neg\neg\varphi) は、前の結果を ¬φ\neg\varphi に適用し、A3 を用いて得る。したがって φ⊣⊢¬¬φ\varphi \dashv\vdash \neg\neg\varphi は、すでにウカシェヴィチの体系で成り立つ。

      支え: C (ウカシェヴィチの公理), E (演繹定理). 証明される授業: 四つの演繹技法.

    4. 二重否定の置換. 二重否定置換の規則を要請する。標識は二重否定には 11 を与えるが、否定論理和の内側での置換にはそうしないからである。χ′\chi' が χ\chi から規則によって得られるならば、χ⊣⊢χ′\chi \dashv\vdash \chi' である。とくに (φ↓ψ)⊣⊢(¬¬φ↓ψ)(\varphi \downarrow \psi) \dashv\vdash (\neg\neg\varphi \downarrow \psi) と (φ↓ψ)⊣⊢(φ↓¬¬ψ)(\varphi \downarrow \psi) \dashv\vdash (\varphi \downarrow \neg\neg\psi) である。

      使う結果: 3. 演繹定理と証明可能な同値, 4. ウカシェヴィチの体系の限界. 支え: G (二重否定). 証明される授業: 四つの演繹技法.

    5. 本コースの体系における演繹定理. 反射性、単調性、カット、有限性は新しい規則のもとでも成り立ち、Γ∪{φ}⊢ψ\Gamma \cup \{\varphi\} \vdash \psi であるのは Γ⊢(φ→ψ)\Gamma \vdash (\varphi \rightarrow \psi) であるとき、かつそのときに限ることも成り立つ。新しい場合では、(φ→χ)(\varphi \rightarrow \chi) は ((¬φ↓χ)↓(¬φ↓χ))((\neg\varphi \downarrow \chi) \downarrow (\neg\varphi \downarrow \chi)) なので、規則は χ\chi のコピーごとに一回ずつ、二回適用される。このことから、⊢((φ↓ψ)→(¬¬φ↓ψ))\vdash ((\varphi \downarrow \psi) \rightarrow (\neg\neg\varphi \downarrow \psi)) とその逆は定理である。

      使う結果: 2. 構造的性質, 3. 演繹定理と証明可能な同値. 支え: B (累積帰納法), D (二重否定の置換). 証明される授業: 四つの演繹技法.

    6. 対偶. (φ→ψ)⊣⊢(¬ψ→¬φ)(\varphi \rightarrow \psi) \dashv\vdash (\neg\psi \rightarrow \neg\varphi)、(¬φ→ψ)⊣⊢(¬ψ→φ)(\neg\varphi \rightarrow \psi) \dashv\vdash (\neg\psi \rightarrow \varphi)、(φ→¬ψ)⊣⊢(ψ→¬φ)(\varphi \rightarrow \neg\psi) \dashv\vdash (\psi \rightarrow \neg\varphi)。項は辺を入れ替え、移るときにそれぞれ符号を変える。

      使う結果: 6. 仮言三段論法と交換. 支え: C (ウカシェヴィチの公理), E (演繹定理), G (二重否定), F (結果から規則へ). 証明される授業: 四つの演繹技法.

  3. 第 3 区間 結合子と置換

    • 略記を展開し、二つの表現が同じ記号列を表すのか、それとも同値であることに演繹を要する論理式を表すのかを判定する。
    • 基本補題によって、否定論理和を否定と含意に翻訳する。
    • 同値なものの置換によって同値を論理式の内部へ移し、それを二重否定の置換の規則と区別し、同値をつなぐ。
    • 定義が課す順序で五つの対称性を証明する。

    1. 基本補題. (φ↓ψ)⊣⊢¬(¬φ→ψ)(\varphi \downarrow \psi) \dashv\vdash \neg(\neg\varphi \rightarrow \psi)。¬(¬φ→ψ)\neg(\neg\varphi \rightarrow \psi) は ¬¬(¬¬φ↓ψ)\neg\neg(\neg\neg\varphi \downarrow \psi) であるから、二重否定置換の規則が内側の二重否定を付け、二重否定が外側の二重否定を付ける。逆向きには、二重否定と規則がそれらを外す。

      支え: D (二重否定の置換), G (二重否定). 証明される授業: 結合子の対称性.

    2. 同値なものの置換. φ⊣⊢φ′\varphi \dashv\vdash \varphi' ならば、¬φ⊣⊢¬φ′\neg\varphi \dashv\vdash \neg\varphi'、(φ→ψ)⊣⊢(φ′→ψ)(\varphi \rightarrow \psi) \dashv\vdash (\varphi' \rightarrow \psi)、(ψ→φ)⊣⊢(ψ→φ′)(\psi \rightarrow \varphi) \dashv\vdash (\psi \rightarrow \varphi') である。基本補題を用いれば、否定論理和の両辺でも同じことが成り立ち、そこから選言と連言でも成り立つ。二重否定置換の規則と異なり、任意の同値な論理式を許す。

      使う結果: 6. 仮言三段論法と交換, 10. 対偶, 11. 基本補題. 支え: E (演繹定理). 証明される授業: 結合子の対称性.

    3. 別形. (φ∨ψ)⊣⊢(¬φ→ψ)(\varphi \vee \psi) \dashv\vdash (\neg\varphi \rightarrow \psi) は、外側の否定が作るコピーごとに一回ずつ、二重否定置換の規則を二回適用して得る。(φ∧ψ)⊣⊢(¬φ↓¬ψ)(\varphi \wedge \psi) \dashv\vdash (\neg\varphi \downarrow \neg\psi) は二重否定による。そして (φ∧ψ)(\varphi \wedge \psi) は ¬(φ→¬ψ)\neg(\varphi \rightarrow \neg\psi) と同じ記号列である。

      支え: D (二重否定の置換), G (二重否定). 証明される授業: 結合子の対称性.

    4. 五つの対称性. (φ↓ψ)⊣⊢(ψ↓φ)(\varphi \downarrow \psi) \dashv\vdash (\psi \downarrow \varphi) は基本補題と対偶による。そこから順に、∨\vee、∧\wedge、↔\leftrightarrow、⊻\veebar の対称性が、それぞれ直前のものから得られ、必要なときには否定のもとの置換で移される。

      使う結果: 11. 基本補題, 10. 対偶. 支え: H (同値なものの置換). 証明される授業: 結合子の対称性.

  4. 第 4 区間 古典的な規則と法則

    • 前提のもとで、選言と連言の導入と除去、排中律、無矛盾律を証明する。
    • 爆発律、背理法、場合分けによる証明を前提のもとで証明し、前提なしではなぜ足りないのかを説明する。
    • ド・モルガンの法則、その変種、分配法則を両方の向きに演繹によって証明する。
    • 根拠を示した同値の連鎖によって、論理式を簡単な標準形に変形する。

    1. 結合子の規則. 任意の Γ\Gamma について、φ\varphi から (φ∨ψ)(\varphi \vee \psi) が従う。(φ∨ψ)(\varphi \vee \psi) と ¬φ\neg\varphi から ψ\psi。φ\varphi と ψ\psi から (φ∧ψ)(\varphi \wedge \psi)。(φ∧ψ)(\varphi \wedge \psi) から φ\varphi と ψ\psi。さらに ⊢(φ∨¬φ)\vdash (\varphi \vee \neg\varphi) かつ ⊢¬(φ∧¬φ)\vdash \neg(\varphi \wedge \neg\varphi) である。

      使う結果: 1. 体系、演繹、同一律, 2. 構造的性質, 6. 仮言三段論法と交換, 10. 対偶, 13. 別形, 14. 五つの対称性. 支え: C (ウカシェヴィチの公理), E (演繹定理), F (結果から規則へ), G (二重否定). 証明される授業: 古典論理の技法.

    2. 爆発律と背理法. Γ⊢φ\Gamma \vdash \varphi かつ Γ⊢¬φ\Gamma \vdash \neg\varphi ならば、Γ⊢ψ\Gamma \vdash \psi がすべての ψ\psi について成り立つ。Γ∪{¬φ}\Gamma \cup \{\neg\varphi\} から ψ\psi と ¬ψ\neg\psi が導かれるならば、Γ⊢φ\Gamma \vdash \varphi。Γ∪{φ}\Gamma \cup \{\varphi\} からそれらが導かれるならば、Γ⊢¬φ\Gamma \vdash \neg\varphi。

      使う結果: 1. 体系、演繹、同一律, 2. 構造的性質, 15. 結合子の規則. 支え: C (ウカシェヴィチの公理), E (演繹定理), G (二重否定). 証明される授業: 古典論理の技法.

    3. 場合分けによる証明. Γ∪{φ}⊢ψ\Gamma \cup \{\varphi\} \vdash \psi かつ Γ∪{¬φ}⊢ψ\Gamma \cup \{\neg\varphi\} \vdash \psi ならば、Γ⊢ψ\Gamma \vdash \psi。そして Γ∪{φ}⊢χ\Gamma \cup \{\varphi\} \vdash \chi、Γ∪{ψ}⊢χ\Gamma \cup \{\psi\} \vdash \chi、Γ⊢(φ∨ψ)\Gamma \vdash (\varphi \vee \psi) ならば、Γ⊢χ\Gamma \vdash \chi。

      使う結果: 2. 構造的性質, 10. 対偶, 15. 結合子の規則, 16. 爆発律と背理法. 支え: E (演繹定理). 証明される授業: 古典論理の技法.

    4. ド・モルガンの法則. ¬(φ∧ψ)⊣⊢(¬φ∨¬ψ)\neg(\varphi \wedge \psi) \dashv\vdash (\neg\varphi \vee \neg\psi) は定義と二重否定による。¬(φ∨ψ)⊣⊢(¬φ∧¬ψ)\neg(\varphi \vee \psi) \dashv\vdash (\neg\varphi \wedge \neg\psi) は、否定論理和の各引数に二重否定置換の規則を一回ずつ適用して得る。したがって (φ↓ψ)⊣⊢(¬φ∧¬ψ)(\varphi \downarrow \psi) \dashv\vdash (\neg\varphi \wedge \neg\psi) かつ ¬(φ→ψ)⊣⊢(φ∧¬ψ)\neg(\varphi \rightarrow \psi) \dashv\vdash (\varphi \wedge \neg\psi) である。

      支え: D (二重否定の置換), G (二重否定), H (同値なものの置換). 証明される授業: ド・モルガンの法則と分配法則.

    5. 分配法則. (φ∧(ψ∨χ))⊣⊢((φ∧ψ)∨(φ∧χ))(\varphi \wedge (\psi \vee \chi)) \dashv\vdash ((\varphi \wedge \psi) \vee (\varphi \wedge \chi)) と (φ∨(ψ∧χ))⊣⊢((φ∨ψ)∧(φ∨χ))(\varphi \vee (\psi \wedge \chi)) \dashv\vdash ((\varphi \vee \psi) \wedge (\varphi \vee \chi)) は、それぞれ両方の向きに場合分けで証明される。対称性を用いれば、右からも成り立つ。

      使う結果: 14. 五つの対称性, 15. 結合子の規則, 17. 場合分けによる証明. 支え: H (同値なものの置換). 証明される授業: ド・モルガンの法則と分配法則.

意味論へ. 鎖は、演繹が数学の推論に用いるすべての技法に届いたところで止まる。残るのは、導かれるものが、すべての付値のもとで真であるものとちょうど一致するかどうかを知ることである。次の単元は真理を定義し、最後の単元は二つの概念を比べる。

根拠の略記

単元の演繹は、各行の根拠を略記で示し、その略記はすべての課で同じである。ここではそれらを、導入した課の順に集める。「前提」は問題文の仮定を表し、演繹についての演繹では、証明される規則の仮定を表す。括弧内の数は、規則を適用する行を指す。すでに証明された同値は、一つの行として書くときは番号なしで引用し、ある行に適用するときは変形される行の番号を添えて引用する。その行の一部に適用するときも同様で、そのときは「同値置換」を用いる。

  • 第一の課：A1、A2、A3（公理図式）。MP(i,j)(i, j)（モーダス・ポネンス）。定義（略記の展開または畳み込み。展開する結合子を添える。「定義 ∨\vee」「定義 ⊣⊢\dashv\vdash」）。同一律（定理 ⊢(φ→φ)\vdash (\varphi \rightarrow \varphi)）。反射性（φ∈Γ\varphi \in \Gamma ならば Γ⊢φ\Gamma \vdash \varphi）。単調性。カット（導かれたものは前提として用いてよい）。有限性。演繹定理と演繹定理の逆。
  • 第二の課：仮言三段論法。前提交換。二重否定。二重否定置換(i)(i)（行 ii における二重否定の置換。番号のない二重否定置換は、論理式と、規則によってそれから得られる論理式との同値を指す）。対偶（三つの形のいずれでもよい）。「例題 nn」（同じ課の例題 nn の結果を一つの行として書いたもの）。
  • 第三の課：基本補題（(φ↓ψ)⊣⊢¬(¬φ→ψ)(\varphi \downarrow \psi) \dashv\vdash \neg(\neg\varphi \rightarrow \psi)）。同値置換（同値なものの置換。どの形でもよく、適用する同値を後に添える。「同値置換、ド・モルガン(i)(i)」）。別形（選言と連言の別形、(φ∨ψ)⊣⊢(¬φ→ψ)(\varphi \vee \psi) \dashv\vdash (\neg\varphi \rightarrow \psi) と (φ∧ψ)⊣⊢(¬φ↓¬ψ)(\varphi \wedge \psi) \dashv\vdash (\neg\varphi \downarrow \neg\psi)）。対称性（結合子の対称性）。
  • 第四の課：∨\vee導入と ∨\vee除去（選言の導入と除去）。∧\wedge導入と ∧\wedge除去（連言の導入と除去）。排中律。無矛盾律（この略記は定理の名であり、単元のどの行の根拠にもならない）。爆発律。場合分け(i,j)(i, j) と場合分け(i,j,k)(i, j, k)（場合分けによる証明。論理式とその否定によるもの、または選言によるもの）。「前提なし場合分け」（集合 Γ\Gamma をもたない場合分けによる証明で、一つの問題にだけ現れる）。背理法（二つの形）。
  • 第五の課：ド・モルガン（ド・モルガンの法則）。分配律。結合律（選言の結合律）。代入例(i)(i)（任意の論理式について成り立つ行 ii を、そのメタ変数の代わりに別の論理式を入れて書き直したもの。代入を明記する）。
  • この課の挑戦課題：M3（第三の挑戦課題が A3 の代わりに置く図式）。