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

結合子の対称性

要約

この課は、否定論理和、選言、連言、双条件、排他的選言について、引数の順序が演繹されるものを変えないことを証明する。本コースの公式の略記のもとでは、これらの対称性は自明ではない。否定論理和は原始結合子であり、ウカシェヴィチの公理は否定と含意についてしか語らず、二重否定の置換の規則は二重否定を付けるか外すことしかしないからである。そこでこの課は、まず三つの道具を確立する。第一は、証明可能な同値が等式のようにふるまうということである。第二の基本補題は、否定論理和を公理の言語に翻訳する。二重否定の置換の規則と二重否定によって、(φ↓ψ)(\varphi \downarrow \psi) は ¬(¬φ→ψ)\neg(\neg\varphi \rightarrow \psi) と同値になる。第三の同値なものの置換は、二重否定の置換の規則があっても余分にはならず、否定のもとで、含意の両側で、そして否定論理和の両側で、論理式をそれと同値な任意の論理式に置き換えることを可能にする（θ\theta を ¬¬θ\neg\neg\theta に置き換えるだけではない）。これらを用いて、選言と連言の別形（ほかの本はこれを定義とする）を同値として証明し、さらに五つの対称性を、両方の向きで、定義が課す順序に従って証明する。まず否定論理和、そしてそこから順に残りのものである。

学習目標

  1. 公式の略記を展開して、二つの表現が同じ論理式を表すのか、それとも同値性に演繹を要する異なる論理式を表すのかを判定する。
  2. 二重否定の置換の規則と二重否定によって基本補題 (φ↓ψ)⊣⊢¬(¬φ→ψ)(\varphi \downarrow \psi) \dashv\vdash \neg(\neg\varphi \rightarrow \psi) を証明し、略記が隠している二重否定の位置を突き止める。
  3. 同値なものの置換を用いて、同値を否定、含意、否定論理和の内部へ移し、それを θ\theta と ¬¬θ\neg\neg\theta を入れ替えるだけの二重否定の置換の規則と区別し、同値の連鎖の中で証明可能な同値を等式として用いる。
  4. すでに証明した結果をつなぎ合わせて、選言と連言の別形と、五つの対称性を両方の向きで証明する。
  5. 論理式の複雑さに関する帰納法によって、同値なものの置換を任意の論理式に拡張する。

用いるものと証明すべきもの

形式的演繹体系の課は、ウカシェヴィチの体系を定めた。すなわち公理 A1、A2、A3 とモーダス・ポネンスである。その課はさらに、反射性（φ∈Γ\varphi \in \Gamma ならば Γ⊢φ\Gamma \vdash \varphi）、単調性、カット（Γ⊢φi\Gamma \vdash \varphi_{i} がすべての ii について成り立ち、かつ Γ∪{φ1,…,φn}⊢ψ\Gamma \cup \{\varphi_{1}, \ldots, \varphi_{n}\} \vdash \psi ならば、Γ⊢ψ\Gamma \vdash \psi）、演繹定理とその逆、そして証明可能な同値 φ⊣⊢ψ\varphi \dashv\vdash \psi（{φ}⊢ψ\{\varphi\} \vdash \psi かつ {ψ}⊢φ\{\psi\} \vdash \varphi であることを意味する）を確立し、公理とモーダス・ポネンスが保存する標識によって、この体系が否定論理和に関するある種の論理式を導かないことを示した。四つの演繹技法の課は、仮言三段論法（{(φ→ψ),(ψ→χ)}⊢(φ→χ)\{(\varphi \rightarrow \psi), (\psi \rightarrow \chi)\} \vdash (\varphi \rightarrow \chi)）、前提の交換（前提交換）、二重否定（φ⊣⊢¬¬φ\varphi \dashv\vdash \neg\neg\varphi。その二つの定理 ⊢(¬¬φ→φ)\vdash (\neg\neg\varphi \rightarrow \varphi) と ⊢(φ→¬¬φ)\vdash (\varphi \rightarrow \neg\neg\varphi) を伴う）、そして三つの形をもつ対偶を加えた。

(φ→ψ)⊣⊢(¬ψ→¬φ),(¬φ→ψ)⊣⊢(¬ψ→φ),(φ→¬ψ)⊣⊢(ψ→¬φ)(\varphi \rightarrow \psi) \dashv\vdash (\neg\psi \rightarrow \neg\varphi), \qquad (\neg\varphi \rightarrow \psi) \dashv\vdash (\neg\psi \rightarrow \varphi), \qquad (\varphi \rightarrow \neg\psi) \dashv\vdash (\psi \rightarrow \neg\varphi)

二重否定を証明したあと、同じ課は二つめの原始規則である二重否定の置換によって本コースの体系を完成させた。χ′\chi' が、χ\chi において部分論理式 θ\theta の一つの出現を ¬¬θ\neg\neg\theta で置き換えるか、部分論理式 ¬¬θ\neg\neg\theta の一つの出現を θ\theta で置き換えることで得られるならば、χ\chi から χ′\chi' を推論してよい。こうして行 ii から得た行は 二重否定置換(i)(i) で根拠づける。それ以後、⊢\vdash は本コースの体系（A1 から A3、モーダス・ポネンス、二重否定の置換）を指し、そこでも反射性、単調性、カット、演繹定理とその逆は引き続き成り立つ。この規則は基本言語の記号列に作用するので、略記が隠している出現にも、否定論理和の二つの引数のどちらにも届く。その直接の帰結には次のものがある。

(φ↓ψ)⊣⊢(¬¬φ↓ψ),(φ↓ψ)⊣⊢(φ↓¬¬ψ)(\varphi \downarrow \psi) \dashv\vdash (\neg\neg\varphi \downarrow \psi), \qquad (\varphi \downarrow \psi) \dashv\vdash (\varphi \downarrow \neg\neg\psi)

一般に、χ⊣⊢χ′\chi \dashv\vdash \chi' は、χ′\chi' が χ\chi から二重否定の置換によって得られるときにはいつでも成り立つ。この形の同値の行は、行番号を付けずに「二重否定置換」で根拠づける。「二重否定」や「対偶」の行がすでに証明された同値を引用するのと同じである。 そこでと同じく、すでに証明した定理は演繹の一行として書いてよい。その定理自身の演繹をその場所に挿入できるからである。また、その課の「結果から規則へ」の補題により、各技法は前提の任意の集合 Γ\Gamma のもとでも規則として適用でき、そのときは 対偶(i)(i) や 仮言三段論法(i,j)(i, j) のように、適用する行の番号を添えて引用する。演繹についての演繹では、「前提」は証明しようとしている規則の仮定を表す。

命題論理の言語の課で定めた公式の略記が、結合子の唯一の定義である。

¬φ:=(φ↓φ),(φ∨ψ):=¬(φ↓ψ),(φ∧ψ):=¬(¬φ∨¬ψ)\neg\varphi := (\varphi \downarrow \varphi), \qquad (\varphi \vee \psi) := \neg(\varphi \downarrow \psi), \qquad (\varphi \wedge \psi) := \neg(\neg\varphi \vee \neg\psi)
(φ→ψ):=(¬φ∨ψ),(φ↔ψ):=((φ→ψ)∧(ψ→φ)),(φ⊻ψ):=¬(φ↔ψ)(\varphi \rightarrow \psi) := (\neg\varphi \vee \psi), \qquad (\varphi \leftrightarrow \psi) := ((\varphi \rightarrow \psi) \wedge (\psi \rightarrow \varphi)), \qquad (\varphi \veebar \psi) := \neg(\varphi \leftrightarrow \psi)

「定義」で根拠づけた行は何も演繹しない。同じ論理式を別の名前で書くだけであり、注記はどの略記を展開するのか畳み込むのかを示す（「定義 →\rightarrow」、「定義 ∨\vee」）。自然言語の形式化の課で見た現象を思い出しておくとよい。同じ論理式がいくつもの名前をもちうるので、連言は記号列としては選言でもある。たとえば、¬φ\neg\varphi を φ\varphi の代わりにして含意を展開すると、次が得られる。

(¬φ→ψ)=(¬¬φ∨ψ)=¬(¬¬φ↓ψ)(\neg\varphi \rightarrow \psi) = (\neg\neg\varphi \vee \psi) = \neg(\neg\neg\varphi \downarrow \psi)

そして φ\varphi の前に現れ、略記によって隠されているこの二重否定こそ、二重否定の置換の規則が以下のすべてに関わってくる理由である。

等式としての証明可能な同値

この課の証明は、ほとんどすべてが同値の連鎖である。φ1⊣⊢φ2\varphi_{1} \dashv\vdash \varphi_{2}、φ2⊣⊢φ3\varphi_{2} \dashv\vdash \varphi_{3}、以下同様である。連鎖から φ1⊣⊢φn\varphi_{1} \dashv\vdash \varphi_{n} を結論するには、証明可能な同値が等式のようにふるまわなければならない。それを確立したのが、形式的演繹体系の課の、証明可能な同値の性質についての命題である。この関係は反射的（φ⊣⊢φ\varphi \dashv\vdash \varphi）、対称的（φ⊣⊢ψ\varphi \dashv\vdash \psi ならば ψ⊣⊢φ\psi \dashv\vdash \varphi）、推移的（φ⊣⊢ψ\varphi \dashv\vdash \psi かつ ψ⊣⊢χ\psi \dashv\vdash \chi ならば φ⊣⊢χ\varphi \dashv\vdash \chi）であり、証明可能な同値である二つの論理式は結論として互いに置き換えられる（Γ⊢φ\Gamma \vdash \varphi かつ φ⊣⊢φ′\varphi \dashv\vdash \varphi' ならば Γ⊢φ′\Gamma \vdash \varphi'。これは論理式の任意の集合 Γ\Gamma について成り立つ）。最後の二つがどう証明されたかを思い出しておくとよい。この課全体がそれに依拠しているからである。{φ}⊢φ′\{\varphi\} \vdash \varphi' から単調性によって Γ∪{φ}⊢φ′\Gamma \cup \{\varphi\} \vdash \varphi' に移り、これと Γ⊢φ\Gamma \vdash \varphi からカットによって Γ⊢φ′\Gamma \vdash \varphi' に至る。推移性は、一方の向きでは Γ={φ}\Gamma = \{\varphi\} として、他方の向きでは Γ={χ}\Gamma = \{\chi\} として、これを適用すれば得られる。

以下では、同値の連鎖を一つの同値にまとめる一歩を「カット」で根拠づける。それがその命題の道具だからである。ところで、各環 φi⊣⊢φi+1\varphi_{i} \dashv\vdash \varphi_{i+1} は行きと帰りの二つの演繹を含む。ゆえに、同値の連鎖はその結論の両方の向きを同時に証明し、何も「練習問題として」残らない。