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

四つの演繹技法

要約

前の課のウカシェヴィチの体系は、三つの公理図式とただ一つの規則、モーダス・ポネンスからなる。これほど乏しい手段では、どの演繹も公理から組み立てなければならず、論理式 (φ→φ)(\varphi \rightarrow \varphi) でさえ五行を要する。この課は、一度だけ証明すればその後くり返し使える四つの技法を加える。含意を連鎖させる仮言三段論法、前件の順序を入れ替えることを可能にする前提の交換、続けて並ぶ二つの否定を付けたり外したりすることを可能にする二重否定、そして三つの形をもち、含意の項を否定してその向きを逆にすることを可能にする対偶である。どの技法も、三つの公理、モーダス・ポネンス、前の課のメタ定理によって一行ずつ完全に証明され、三つの形で得られる。前提からの演繹として、定理として、そして任意の前提集合のもとで適用できる規則としてである。二重否定を証明したのち、この課は第二の原始規則、二重否定の置換によって体系を完成させる。これは論理式のどの位置でも二つの否定を付けたり外したりすることを可能にし、三つの公理の届かない否定論理和の内部でもそれができる。さらに、この規則を要請しなければならない理由を説明し、演繹の性質が保たれることを確かめ、演繹定理を新しい場合で補い、その最初の帰結を導く。

学習目標

  1. {α1,…,αn}⊢β\{\alpha_{1}, \ldots, \alpha_{n}\} \vdash \beta という形の結果を、演繹定理によって定理に変え、単調性とカットによって、任意の前提集合 Γ\Gamma のもとで適用できる規則に変える。
  2. 仮言三段論法と前提の交換を、A1 と A2 からの直接の演繹によっても、演繹定理を用いた演繹についての推論によっても証明し、それらを用いて含意を連鎖させ、並べ替える。
  3. 二重否定の二つの向きを A1 から A3 とモーダス・ポネンスによって証明し、それらを適用して、演繹の中で続けて並ぶ二つの否定を付けたり外したりする。
  4. 二重否定の置換の規則を述べ、基本言語の記号列における部分論理式の出現を、略記が隠す出現も含めて見つけ、その規則を演繹の中で適用する。
  5. 二重否定の置換を要請しなければならない理由を標識によって説明し、演繹の性質と演繹定理が拡張された体系でも成り立つことを証明する。
  6. 対偶を三つの形で証明し、否定を含む含意に対して、ふさわしい形を選ぶ。
  7. 四つの技法と新しい規則を、公理、モーダス・ポネンス、演繹定理と組み合わせて自明でない演繹を組み立て、各行を対応する略記で根拠づける。

出発点の道具

形式的演繹体系の課で、ウカシェヴィチの体系が定められた。その言語は白丸と黒丸の言語であり、命題論理の言語の課の公式の略記で書かれる。その公理は次の三つの図式のすべての代入例であり（φ\varphi、ψ\psi、χ\chi は任意の論理式）、その唯一の規則はモーダス・ポネンスである。

  • 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))。
  • MP：φ\varphi と (φ→ψ)(\varphi \rightarrow \psi) から ψ\psi が導かれる。

φ\varphi の、論理式の集合 Γ\Gamma からの演繹とは、φ\varphi で終わる有限の論理式の列であって、その各論理式が公理であるか、Γ\Gamma の要素であるか、先行する二つの論理式にモーダス・ポネンスを適用した結果であるものをいう。そのような列が存在するとき Γ⊢φ\Gamma \vdash \varphi と書き、Γ\Gamma が空ならば ⊢φ\vdash \varphi と書いて、φ\varphi は定理であるという。同じ課で、ここで用いるメタ定理が証明された。反射性（φ∈Γ\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 が 11 から nn までのそれぞれについて成り立ち、かつ Γ∪{φ1,…,φn}⊢ψ\Gamma \cup \{\varphi_{1}, \ldots, \varphi_{n}\} \vdash \psi ならば Γ⊢ψ\Gamma \vdash \psi）、有限性（Γ⊢φ\Gamma \vdash \varphi ならば、Γ\Gamma のある有限部分集合で足りる）、演繹定理（Γ∪{φ}⊢ψ\Gamma \cup \{\varphi\} \vdash \psi ならば Γ⊢(φ→ψ)\Gamma \vdash (\varphi \rightarrow \psi)）とその逆（演繹定理の逆）、そして定理 ⊢(φ→φ)\vdash (\varphi \rightarrow \varphi) であり、最後のものは根拠欄では同一律と略記する。最後に、φ⊣⊢ψ\varphi \dashv\vdash \psi（証明可能な同値）は、{φ}⊢ψ\{\varphi\} \vdash \psi かつ {ψ}⊢φ\{\psi\} \vdash \varphi であることを意味する。

¬\neg と →\rightarrow は基本言語の記号ではなく、略記であることを思い出しておこう。¬φ\neg\varphi は記号列 (φ↓φ)(\varphi \downarrow \varphi) であり、(φ→ψ)(\varphi \rightarrow \psi) は (¬φ∨ψ)(\neg\varphi \vee \psi)、すなわち ¬(¬φ↓ψ)\neg(\neg\varphi \downarrow \psi) である。三つの公理は否定と含意についてしか語らず、同じ課は、公理とモーダス・ポネンスが保存する、00 と 11 の値をとる標識を用いて、そこから生じる限界を示した。ウカシェヴィチの体系では、(v1↓v2)(v_{1} \downarrow v_{2}) から (¬¬v1↓v2)(\neg\neg v_{1} \downarrow v_{2}) は導かれず、否定論理和は部分的にその手の届かないところにある。したがって、この課は二段階で進む。二重否定まで（二重否定を含む）は、⊢\vdash はウカシェヴィチの体系を指し、証明されることはどれも略記の展開に依存しない。二重否定を証明したのち、体系に第二の原始規則として二重否定の置換を加える。これは展開された記号列に作用する。その時点から、⊢\vdash は本コースの体系、すなわちウカシェヴィチの体系にこの規則を加えたものを指す。前者の演繹はどれも後者の演繹でもあるので、それまでに証明したことは何も失われない。

演繹の二つの書き方

演繹の書き方は二通りあり、どちらも用いる。第一は本来の意味での演繹、すなわち論理式の列であって、各行が公理、前提、またはモーダス・ポネンスの結果であるものである。各行の根拠は A1、A2、A3、前提、または MP(i,j)(i, j) と書く。ここで行 ii は前件であり、行 jj は、その前件がちょうど行 ii であるような含意である（新しい規則を導入したあとは、二重否定置換(i)(i) も加わる）。第二は演繹についての演繹であり、その行は論理式ではなく、Γ⊢φ\Gamma \vdash \varphi という形の主張である。各行はすでに証明されたメタ定理によって根拠づけられ、列全体はメタ言語の推論であって、第一の書き方の演繹が存在することを、それを書き出すことなく保証する。この第二の書き方の根拠は次のように読む。

  • 反射性：右の論理式は左の集合に属する。
  • A1、A2、A3：右の論理式はその図式の代入例である。公理の代入例は、任意の Γ\Gamma から一行だけの演繹で導かれる。
  • MP(i,j)(i, j)：演繹どうしのモーダス・ポネンスを、行 ii の Γ⊢φ\Gamma \vdash \varphi と行 jj の Γ⊢(φ→ψ)\Gamma \vdash (\varphi \rightarrow \psi) に、同じ Γ\Gamma で適用したもの。
  • 演繹定理(i)(i) と演繹定理の逆(i)(i)：行 ii に適用した演繹定理またはその逆。
  • すでに証明された定理の名前、たとえば同一律や二重否定：右の論理式はその定理の代入例であり、任意の Γ\Gamma から単調性によって導かれる。空集合は Γ\Gamma に含まれるからである。
  • 前提（演繹についての演繹の中で）：その行は、証明しようとしている規則の仮定の一つである。

この課の結果はどれもメタ変数で述べられ、したがって任意の論理式について成り立つ。その証明は図式であり、その中の各メタ変数に論理式を代入すると別の証明が得られる。公理図式の代入例は代入例のままであり、モーダス・ポネンスの各適用もそのままだからである（新しい規則の各適用についても同じことが成り立つ）。こうして、⊢(φ→φ)\vdash (\varphi \rightarrow \varphi) から ⊢(¬ψ→¬ψ)\vdash (\neg\psi \rightarrow \neg\psi) が従う。¬ψ\neg\psi を φ\varphi の代わりに用いればよい。結果を、述べられたものより複雑な論理式に適用するこの手段は、以下で最も役に立つ。

結果から規則へ

この課の技法は、{(φ→ψ),(ψ→χ)}⊢(φ→χ)\{(\varphi \rightarrow \psi), (\psi \rightarrow \chi)\} \vdash (\varphi \rightarrow \chi) のような固定した前提から証明される。しかし使われるのは別の前提をもつ演繹の途中であり、そこでは (φ→ψ)(\varphi \rightarrow \psi) と (ψ→χ)(\psi \rightarrow \chi) は前提ではなく、すでに導かれた論理式である。単調性とカットから直接従う次の補題が、そのような使い方を一度にすべて正当化する。

補題結果から規則へ

{α1,…,αn}⊢β\{\alpha_{1}, \ldots, \alpha_{n}\} \vdash \beta ならば、論理式の任意の集合 Γ\Gamma について、Γ⊢α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)) である。

証明

  1. Γ∪{α1,…,αn}⊢β\dato{mon}{\Gamma \cup \{\alpha_{1}, \ldots, \alpha_{n}\} \vdash \beta}

    仮定により、β\beta は論理式 αi\alpha_{i} から導かれる。{α1,…,αn}\{\alpha_{1}, \ldots, \alpha_{n}\} は Γ∪{α1,…,αn}\Gamma \cup \{\alpha_{1}, \ldots, \alpha_{n}\} に含まれるので、単調性により前提に Γ\Gamma を加えることができる。

  2. Γ⊢β\Gamma \vdash \resaltar{\beta}

    さらに各 αi\alpha_{i} が Γ\Gamma から導かれるなら、カットが加えた前提を取り除く。

  3. ⊢(α1→(α2→⋯(αn→β)⋯ ))\vdash (\alpha_{1} \rightarrow (\alpha_{2} \rightarrow \cdots (\alpha_{n} \rightarrow \beta) \cdots))

    定理の形については、演繹定理を nn 回適用し、前提を最後のものから最初のものへと解除する。各適用は、解除した前提を含意の前件に変える。

したがって、前提から証明された技法はどれも三つの形をもつ。結果そのもの、その前提を解除して得られる定理、そして任意の Γ\Gamma のもとで適用される規則である。演繹についての演繹では、規則は技法の名前と、それを適用する行の番号によって、仮言三段論法(3,4)(3, 4) のように呼び出され、補題がその一歩の正当性を保証する。