h5i

付録 A

証明が項になることの証明

第 4 章では、二階命題論理のあらゆる証明が、カーネルの受理する項に変換できると主張した（定理 4.1）。本付録ではその主張を精密に述べ、完全に証明する。変数と仮定の扱いを明確にすれば証明は短く、論理の判断の導出に関する帰納法であり、各ケースは第 4 章の表の一行を左から右へ読んだものにあたる。

考え方

論理における導出は規則適用の木であり、第 4 章の変換は各論理規則を一つの型付け規則と対にしたので、自然な方針は、導出を葉から上へたどり、各節点で、対になる型付け規則が与える型付け導出を組み立てることである。仮定は変数の参照になり、含意の導入は λ\lambda に、含意の除去は適用になる。二つの量化子規則は、Sort 0\Sort{0} 上の λ\lambda と、型への適用になる。

注意を要する細部が二つあり、どちらも文脈に関わる。

  • 論理の規則は、どの命題変数がスコープ内にあるかを述べないが、命題変数 PP は仮定 P:Sort 0P : \Sort{0} が文脈に入ってはじめて使えるので、型付けの側はそれを知る必要がある。そこで精密な主張は、命題変数の明示的なリスト Θ\Theta を携える。
  • 型付け規則は文脈を右側に拡張するが、第 4 章の変換 Δ∗\Delta^\ast は、すべての命題変数をすべての仮定の前に置く。任意の並び順を許したほうが証明は楽なので、以下で定義する意味で論理の判断を表現するあらゆる文脈について定理を証明する。

精密な主張

定理 4.1 では、どの命題変数がスコープ内にあるかが暗黙になっていた。証明のためにこれを明示し、

Θ;Δ⊢φ,\Theta; \Delta \vdash \varphi,

と書く。ここで Θ\Theta は相異なる命題変数のリストであり、Δ\Delta または φ\varphi に自由に現れる命題変数はすべて Θ\Theta に属する。命題変数を明示すると、第 4 章の規則は次のようになる。

φ∈ΔΘ;Δ⊢φ;(Hyp)Θ;Δ,φ⊢ψΘ;Δ⊢φ→ψ;(→-intro)Θ;Δ⊢φ→ψΘ;Δ⊢φΘ;Δ⊢ψ;(→-elim)\dfrac{\varphi \in \Delta}{\Theta; \Delta \vdash \varphi}\rulename{Hyp} \qquad \dfrac{\Theta; \Delta, \varphi \vdash \psi}{\Theta; \Delta \vdash \varphi \to \psi}\rulename{$\to$-intro} \qquad \dfrac{\Theta; \Delta \vdash \varphi \to \psi \qquad \Theta; \Delta \vdash \varphi}{\Theta; \Delta \vdash \psi}\rulename{$\to$-elim}
Θ,P;Δ⊢φP∉ΘΘ;Δ⊢∀P. φ;(∀-intro)Θ;Δ⊢∀P. φFV(ψ)⊆ΘΘ;Δ⊢φ[P↦ψ];(∀-elim)\dfrac{\Theta, P; \Delta \vdash \varphi \qquad P \notin \Theta}{\Theta; \Delta \vdash \forall P.\,\varphi}\rulename{$\forall$-intro} \qquad \dfrac{\Theta; \Delta \vdash \forall P.\,\varphi \qquad \FV(\psi) \subseteq \Theta}{\Theta; \Delta \vdash \subst{\varphi}{P}{\psi}}\rulename{$\forall$-elim}

Δ\Delta に自由に現れる命題変数はすべて Θ\Theta にあり、PP はそこにないので、第 4 章の側条件 P∉FV(Δ)P \notin \FV(\Delta) は、いまや P∉ΘP \notin \Theta から従う。論理式は α\alpha 同値を除いて扱うので、束縛された PP はつねに側条件を満たすように改名できる。第 4 章と同じく、φ∗→ψ∗\varphi^\ast \to \psi^\ast は、xx を新鮮な変数として Π(x:φ∗). ψ∗\tPi{x}{\varphi^\ast}{\psi^\ast} を表す。

第 4 章の文脈 Δ∗\Delta^\ast は、命題変数を先に並べ、仮定をその後に並べるが、証明では文脈を右側に拡張する必要があるので、任意の順序を許すのが都合がよい。

定義 A.1（表現）. 文脈 Γ\Gamma が (Θ;Δ)(\Theta; \Delta) を表現するとは、⊢Γ;ok\ctxok{\Gamma} であり、Γ\Gamma が各 P∈ΘP \in \Theta に対する仮定 P:Sort 0P : \Sort{0} を一つずつと、各 χ∈Δ\chi \in \Delta に対する仮定 h:χ∗h : \chi^\ast を一つずつ、何らかの順序で並べたものからなることをいう。

定理 A.2（定理 4.1 の精密な形）. Θ;Δ⊢φ\Theta; \Delta \vdash \varphi であり、Γ\Gamma が (Θ;Δ)(\Theta; \Delta) を表現するならば、ある項 tt について Γ⊢t:φ∗\Gamma \vdash t : \varphi^\ast が成り立つ。

定理 4.1 は Γ=Δ∗\Gamma = \Delta^\ast という特別な場合であり、Θ\Theta が自由な命題変数を列挙するとき、文脈 Δ∗\Delta^\ast はちょうど必要な仮定を含む。それが整形式であることは、命題変数がスコープに入れば各仮定の型 χ∗\chi^\ast は命題なので、後述の補題 A.3 と規則 C-Ext から従う。

変換についての事実

変換 φ↦φ∗\varphi \mapsto \varphi^\ast は代入と可換である。

(φ[P↦ψ])∗=φ∗[P↦ψ∗].(\subst{\varphi}{P}{\psi})^\ast = \subst{\varphi^\ast}{P}{\psi^\ast}.

両辺とも PP の自由な出現を ψ∗\psi^\ast で置き換えるのであり、変換は命題変数に対してその名前を保つ以外に何もしないので、これは φ\varphi に関する定型的な帰納法で示せる。主証明の ∀\forall-elim のケースはこの等式に依存する。

次の補題は、第 13 章の宇宙構造が入ってくる唯一の箇所であり、変換されたすべての論理式が命題である、すなわち型 Sort 0\Sort{0} を持つことを述べる。これがなければ、型付け規則 T-Lam を仮定に適用できず、∀\forall-elim のケースで量化子を任意の論理式で具体化できない。

補題 A.3（論理式は命題である）. ⊢Γ;ok\ctxok{\Gamma} であり、すべての P∈FV(φ)P \in \FV(\varphi) について (P:Sort 0)∈Γ(P : \Sort{0}) \in \Gamma ならば、Γ⊢φ∗:Sort 0\Gamma \vdash \varphi^\ast : \Sort{0} である。

φ\varphi に関する帰納法による。

命題変数 PP の場合、仮定から (P:Sort 0)∈Γ(P : \Sort{0}) \in \Gamma なので、T-Var により Γ⊢P:Sort 0\Gamma \vdash P : \Sort{0} である。

φ→ψ\varphi \to \psi の場合、帰納法の仮定から Γ⊢φ∗:Sort 0\Gamma \vdash \varphi^\ast : \Sort{0} なので、新鮮な xx について Γ,x:φ∗\Gamma, x : \varphi^\ast は C-Ext により整形式である。この拡張した文脈で ψ\psi に帰納法の仮定を適用すると Γ,x:φ∗⊢ψ∗:Sort 0\Gamma, x : \varphi^\ast \vdash \psi^\ast : \Sort{0} が得られ、T-Pi により Γ⊢Π(x:φ∗). ψ∗:Sort imax(0,0)=Sort 0\Gamma \vdash \tPi{x}{\varphi^\ast}{\psi^\ast} : \Sort{\imax(0, 0)} = \Sort{0} となる。

∀Q. χ\forall Q.\,\chi の場合、Q∉dom(Γ)Q \notin \dom(\Gamma) となるように QQ を改名する。T-Sort により Γ⊢Sort 0:Sort 1\Gamma \vdash \Sort{0} : \Sort{1} なので、Γ,Q:Sort 0\Gamma, Q : \Sort{0} は C-Ext により整形式である。この文脈で χ\chi に帰納法の仮定を適用すると Γ,Q:Sort 0⊢χ∗:Sort 0\Gamma, Q : \Sort{0} \vdash \chi^\ast : \Sort{0} が得られ、T-Pi により Γ⊢Π(Q:Sort 0). χ∗:Sort imax(1,0)=Sort 0\Gamma \vdash \tPi{Q}{\Sort{0}}{\chi^\ast} : \Sort{\imax(1, 0)} = \Sort{0} となる。

証明

定理 A.2 を、Θ;Δ⊢φ\Theta; \Delta \vdash \varphi の導出に関する帰納法で、表現するすべての文脈 Γ\Gamma について同時に証明する。各ケースは、第 4 章の表の右列に示した型付け導出を組み立てる。

仮定（Hyp）. この規則は φ∈Δ\varphi \in \Delta から Θ;Δ⊢φ\Theta; \Delta \vdash \varphi を結論する。Γ\Gamma は (Θ;Δ)(\Theta; \Delta) を表現するので仮定 h:φ∗h : \varphi^\ast を含み、T-Var により Γ⊢h:φ∗\Gamma \vdash h : \varphi^\ast である。

→\to-intro. 前提は Θ;Δ,φ⊢ψ\Theta; \Delta, \varphi \vdash \psi、結論は Θ;Δ⊢φ→ψ\Theta; \Delta \vdash \varphi \to \psi である。補題 A.3 により Γ⊢φ∗:Sort 0\Gamma \vdash \varphi^\ast : \Sort{0} なので、新鮮な hh について、文脈 Γ,h:φ∗\Gamma, h : \varphi^\ast は C-Ext により整形式であり、(Θ;Δ,φ)(\Theta; \Delta, \varphi) を表現する。前提とこの文脈に帰納法の仮定を適用すると、ある tt について Γ,h:φ∗⊢t:ψ∗\Gamma, h : \varphi^\ast \vdash t : \psi^\ast が得られ、T-Lam により

Γ⊢λ(h:φ∗). t:Π(h:φ∗). ψ∗.\Gamma \vdash \tLam{h}{\varphi^\ast}{t} : \tPi{h}{\varphi^\ast}{\psi^\ast}.

となる。ψ∗\psi^\ast の自由変数は命題変数であり、hh はそのどれでもないので、hh は ψ∗\psi^\ast に現れず、この Π\Pi は非依存的で、この型は φ∗→ψ∗\varphi^\ast \to \psi^\ast である。

→\to-elim. 前提は Θ;Δ⊢φ→ψ\Theta; \Delta \vdash \varphi \to \psi と Θ;Δ⊢φ\Theta; \Delta \vdash \varphi である。帰納法の仮定から、x∉FV(ψ∗)x \notin \FV(\psi^\ast) となる Γ⊢f:Π(x:φ∗). ψ∗\Gamma \vdash f : \tPi{x}{\varphi^\ast}{\psi^\ast} と、Γ⊢a:φ∗\Gamma \vdash a : \varphi^\ast が得られる。T-App により Γ⊢f  a:ψ∗[x↦a]\Gamma \vdash f\;a : \subst{\psi^\ast}{x}{a} であり、xx は ψ∗\psi^\ast に現れないので代入は何もせず、ψ∗[x↦a]=ψ∗\subst{\psi^\ast}{x}{a} = \psi^\ast である。

∀\forall-intro. 前提は P∉ΘP \notin \Theta を満たす Θ,P;Δ⊢φ\Theta, P; \Delta \vdash \varphi、結論は Θ;Δ⊢∀P. φ\Theta; \Delta \vdash \forall P.\,\varphi である。Θ\Theta の変数を新鮮な変数に改名しても導出が保たれることは定型的な帰納法で示せるので、必要なら PP を改名して P∉dom(Γ)P \notin \dom(\Gamma) と仮定する。T-Sort と C-Ext により Γ,P:Sort 0\Gamma, P : \Sort{0} は整形式であり、(Θ,P;Δ)(\Theta, P; \Delta) を表現する。帰納法の仮定から Γ,P:Sort 0⊢t:φ∗\Gamma, P : \Sort{0} \vdash t : \varphi^\ast が得られ、T-Lam により

Γ⊢λ(P:Sort 0). t:Π(P:Sort 0). φ∗,\Gamma \vdash \tLam{P}{\Sort{0}}{t} : \tPi{P}{\Sort{0}}{\varphi^\ast},

となり、これは ∀P. φ\forall P.\,\varphi の変換である。

∀\forall-elim. 前提は FV(ψ)⊆Θ\FV(\psi) \subseteq \Theta を満たす Θ;Δ⊢∀P. φ\Theta; \Delta \vdash \forall P.\,\varphi、結論は Θ;Δ⊢φ[P↦ψ]\Theta; \Delta \vdash \subst{\varphi}{P}{\psi} である。帰納法の仮定から Γ⊢f:Π(P:Sort 0). φ∗\Gamma \vdash f : \tPi{P}{\Sort{0}}{\varphi^\ast} が得られる。ψ\psi の命題変数はすべて Θ\Theta にあり、したがって Γ\Gamma に仮定 Q:Sort 0Q : \Sort{0} を持つので、補題 A.3 により Γ⊢ψ∗:Sort 0\Gamma \vdash \psi^\ast : \Sort{0} である。T-App により

Γ⊢f  ψ∗:φ∗[P↦ψ∗]=(φ[P↦ψ])∗,\Gamma \vdash f\;\psi^\ast : \subst{\varphi^\ast}{P}{\psi^\ast} = (\subst{\varphi}{P}{\psi})^\ast,

となり、最後のステップは前節の代入の等式である。

論理のすべての規則を扱ったので、定理はあらゆる導出について成り立つ。

組み立てるすべての型付け導出は、束縛変数の名前を除いて型を構文的にのみ比較するので、この証明は T-Conv を一度も必要としない。変換が必要になるのは、第 II 部の帰納型のように、論理に計算を加えたときだけである。

覚えておくこと

  • 定理の精密な形は命題変数の明示的なリスト Θ\Theta を携え、(Θ;Δ)(\Theta; \Delta) を任意の順序で表現するあらゆる文脈について主張を証明する。
  • 変換されたすべての論理式は Sort 0\Sort{0} に住み（補題 A.3）、これは ∀\forall のケースで非述語性を使っており、∀\forall-elim が量化子を任意の論理式で具体化できるのはそのおかげである。
  • 証明は導出に関する帰納法であり、各論理規則はちょうど一つの型付け規則に対応し、Hyp は T-Var に、二つの導入は T-Lam に、二つの除去は T-App に対応する。
  • 論理には計算がないので、T-Conv は一度も使われない。
前の章体系の性質次の章α 同値アルゴリズムの正しさ