book プレビュー

高階の論理

admin

import /common/word_logic.book

1 高階変数

普段のMatheliaは「すべての集合Xについて」のような、もの（集合）についての全称を扱います。ここで扱うのは「すべての性質Pについて」のような、性質・命題・関数そのものについての全称です。
次のFormを高階変数と呼びます。
　v^-Form（$P$）… 命題変数
　?v^-Form（${R}$・$\mathbin{S}$）… 述語変数（引数の個数は  の個数）
　?v-Form（${f}$・$\mathbin{f}$）… 関数変数
引数の型は綴りで決まります（ は s-Form を、 は c-Form を引数にとる）。周囲の量化子の名前や入れ子の順序から推測しません。

Thm $\mathcal{T}$ に自由に現れる高階変数は、全称で閉じたものと読みます（Thm 全体の外側で1回だけ閉じる＝goal と sos で同じものを指します。前提の中だけで閉じるのではありません）。
　$\mathcal{T}$ holds in $\mathbb{L}_{\rm H}$ … 高階変数にどの命題・述語・関数を入れても $\mathcal{T}$ が成り立つ

これが要る実例が、0_tutorial_AI/6.bookの分出公理・置換公理です。置換公理は「任意の関係について」という、無限個の公理をひとまとめにした公理図式（schema）です。
高階変数を含むThmの判定には2つの道があります。
① 高階変数を新しい記号に置き替えて一階の証明器で判定する（|v-elim）。
② 高階論理のまま高階の証明器 Satallax で判定する（backend は satallax+）。
高階変数へ具体的な式を代入するには、式に ∀ を書いた prop（prop 名 <- `∀ ??p^ ( ψ )`）か schema 宣言を使います（どちらも「すべての述語について」という同じ意味）。

2 型と依存関係

真理値の型を $o$ と書きます。一階側の個体の型を $s$、{s,c}ソート側の型を $s,c$ と書きます。
　$P:o$ … 引数を持たない命題（$P$）
　$R:s\to o$ … 集合の引数を1つ取る述語（${R}$）。適用は $R(x)$（ ${R} x$ ）
　$S:s\to s\to o$ … 集合の引数を2つ取る述語（$\mathbin{S}$）
　$B:s\to c\to o$ … 集合とクラスの引数を取る述語（$\mathbin{B}$）
　$f:s\to s$ … 集合を1つ取り集合を返す関数（${f}$）

同じ高階変数は、goal・sosを通じて同じ型と同じ引数の順序を持ちます。各出現では、その型に合う実引数をすべて明示します。
量化子で囲んだだけでは引数は増えません。$P$ は常に0項の命題です。

3 代入は型を合わせ、捕獲を避ける

述語 $R:s\to o$ には、同じ型の式を代入します。例えば、$a:s$ を定数として、
　$R:=\lambda u:s.\,(u=a)$
と指定できます。適用した結果は、通常の $\beta$ 簡約によって得ます。
　$(\lambda u.\,(u=a))(x)$ → $x=a$

変数 $y$ にも依存することを明示した例は、$S:s\to s\to o$ に対する次の代入です。
　$S:=\lambda u:s.\,\lambda v:s.\,(u=v)$
　$\forall x\,S(x,y)$ → $\forall x\,(x=y)$
この $x$ は、代入前から実引数として $\forall x$ に束縛されています。代入式の自由変数を名前の一致で新しく束縛したのではありません。

代入と $\beta$ 簡約は、いずれも変数の捕獲を避けます。必要な束縛変数の改名を先に行います。
例えば、自由なパラメータ $y$ を含む $\lambda u.\,(u=y)$ を、$\forall y\,R(y)$ の $R$ に代入すると、
　$\forall z\,((\lambda u.\,(u=y))(z))$ → $\forall z\,(z=y)$
となります。$\forall y\,(y=y)$ にはしません。

束縛変数を改名するときは、そこに束縛される実引数も一緒に改名します。$\forall x\,S(x,y)$ と $\forall z\,S(z,y)$ は $\alpha$ 同値で、どちらに同じ述語を代入しても結果は $\alpha$ 同値です。

一階側のインスタンス生成では、代入を $\lambda u_1\ldots u_n.\,\theta$ とし、$\theta$ はその対象言語の式とします。
$\theta$ の自由な個体変数は、すべて $u_1,\ldots,u_n$ に含めます。それ以外の個体への依存は、引数を追加して明示するか、言語中の定数として表します。

4 高階論理への翻訳と論理の定義

対象とする高階論理を $\mathbb{L}_{\mathrm H}$ と書きます。非空の基底型を持つ古典的な単純型理論で、Henkin意味論・外延性・選択を含めます（TPTP THF の TH0 の論理）。

通常のpropだけをsosに持つ $\mathcal{T}=G\blacktriangleleft A_1,\ldots,A_m$ を、次のように翻訳します。
各式を構造に沿って翻訳します。変数は同じ型の変数へ、定数は同じ型の定数へ移し、関数・述語の適用は引数の順序を保って高階の適用へ移します。
論理記号は対応する論理記号へ、個体の量化子は同じ基底型の量化子へ、等号は同じ型の等号へ移します。
$U(F)$ は、翻訳後の式 $F$ の自由な個体変数を、それぞれの型で全称閉包したものとします。高階変数はここでは閉じません。空のsosの連言は $\top$ とします。

$\mathcal{T}$ に現れる相異なる高階変数を $P_1,\ldots,P_k$ として、高階翻訳を次の閉じた式とします。
　$H(\mathcal{T})=\forall P_1\cdots\forall P_k\,((U(A_1)\land\cdots\land U(A_m))\Rightarrow U(G))$
高階変数の量化は、Thm全体の外側で1回だけ行います。sosの各propごとに独立した量化を付けてはいけません。

一階側では非空の基底型 $s$ のみを使い、この翻訳を $H_1$ とします。{s,c}ソート側では $s,c$ を互いに異なる独立な非空の基底型として使い、翻訳を $H_{\mathrm{sc}}$ とします。
$c$ を述語の型 $s\to o$ へ置き換えることはしません。所属を表す記号も、型 $s\to c\to o$ の通常の非論理記号として移します。クラスの外延性や集合とクラスを結ぶ公理を、翻訳が新たに仮定することはありません。

論理の定義：
　$\mathcal{T}$ holds in $\mathbb{L}_{\mathrm{Hsc}}$ $\Longleftrightarrow$ $H_{\mathrm{sc}}(\mathcal{T})$ が（基底型 $s,c$ の）高階論理で妥当
　$\mathcal{T}$|0 holds in $\mathbb{L}_{\mathrm H}$ $\Longleftrightarrow$ $H_1(\mathcal{T}$|0$)$ が（基底型 $s$ の）高階論理で妥当
（3.book「論理と定理」の $\mathbb{L}_{\mathrm{Hsc}}$・$\mathbb{L}_{\mathrm H}$ はこの意味です。）

5 高階変数の定数化 |v-elim

Thm $\mathcal{T}$ に現れる高階変数の集合からの単射 $\sigma$ で、
　$\sigma$ : v^-Form → $\mathbb{W}$(,p)
　$\sigma$ : ?v^-Form → $\mathbb{W}$(s,p)、??v^-Form → $\mathbb{W}$(ss,p)、…
　$\sigma$ : ?v-Form → $\mathbb{W}$(s,s)、…（関数変数は同じ引数と返り値の型の関数記号へ）
　$\sigma$の像全体は$\mathcal{T}$の他の記号と非交叉
を満たすものを1つ選び、$\mathcal{T}$の各高階変数を$\sigma$で置き替えたものを $\mathcal{T}$|v-elim とします。$\sigma$はgoal・sos共通で1つです。
例　( ${\perp} \Rightarrow P$ ◀ $P$)|v-elim … ${\perp} \Rightarrow \mathrm{P}$ ◀ $\mathrm{P}$（$\sigma$($P$) = $\mathrm{P}$ の場合）

単射でなければなりません。例えば $P \Rightarrow Q$ の $P$ と $Q$ を両方 $\mathrm{P}$ にすると $\mathrm{P} \Rightarrow \mathrm{P}$ となり、成り立たないThmが成り立ってしまいます。
像が他の記号と交わってもいけません。 ${f} x = {\mathrm{f}} x$ の ${f}$ を ${\mathrm{f}}$ にすると、成り立たないThmが成り立ってしまいます。

次の範囲を考えます。
① 高階変数は、基底型の引数をすべて与えた形でだけ出現する（0項も含む）。
② 式の内部の量化は個体変数に限る。高階変数の等号や、高階変数を引数に取る記号は含めない。
③ schema宣言を仮定として含めない。
この範囲では、$\sigma$の選び方によらず、
　$\mathcal{T}$|v-elim holds in $\mathbb{L}_1$ $\Longleftrightarrow$ $\mathcal{T}$ holds in $\mathbb{L}_{\mathrm H}$
　$\mathcal{T}$|v-elim holds in $\mathbb{L}_{\rm 1sc}$ $\Longleftrightarrow$ $\mathcal{T}$ holds in $\mathbb{L}_{\mathrm{Hsc}}$
が成り立ちます。これは一階論理の「解釈を決めていない記号について示せたことは、その記号を何にしても成り立つ」という事実によります。

理由：高階モデルで高階変数の値を固定すれば、それを新しい記号の解釈とする一階モデルが得られます。したがって、一階側で妥当なら高階側でも妥当です。
逆に、一階側の反例モデルは、各関数型を全関数空間とする高階モデルへ拡張できます。高階変数の値を新しい記号の解釈に選べば、同じ反例になります。
{s,c}ソート側でも、非空の領域 $D_s,D_c$ をそれぞれ基底型の領域として保つので、同じ議論が両ソートに適用できます。
選択演算子は、メタ理論の選択を用いて解釈します。全モデルはHenkinモデルの特別な場合なので、一方の向きで任意のHenkinモデルを一階側へ制限し、逆の向きで一階の反例を全モデルへ拡張すれば足ります。
この同値は上の範囲についてのものです。高階量化を含むschemaの仮定まで、同じ置換で処理できるという主張ではありません。

6 代入の危険

$( \forall x P ) \Leftrightarrow ( \exists x P )$ ◀ O は|v-elimで示せます（$\sigma$($P$)は x に依存しない定数で、領域は非空なので自明）。高階論理でも成り立ちます。
ここに $P$ := $x = y$ を代入すると $( \forall x x = y ) \Leftrightarrow ( \exists x x = y )$ となりますが、要素2個以上の領域では偽です。
$P$ は0項なので、x に依存する式は代入できません。2引数の述語変数 $S$ の $( \forall x S ( ) ) \Leftrightarrow ( \exists x S ( ) )$ は、$S:=\lambda u\,v.\,(u=v)$ が反例となり、一般には成り立ちません。
証明できたことは、高階変数へ具体的な式を代入してよいことを意味しません。代入には次の、∀ を書いた prop か schema 宣言を使います。

7 ∀ の述語変数・schemaとインスタンス指定列

通常の仮定 $A(P)$ と、「すべての $P$ について仮定する」というschemaは区別します。
schema宣言は公理宣言と同格です。「局所述語にどの式を代入しても成り立つ」という著者の保証であり、機械はその数学的な正しさを検証しません。

7.1 ∀ を書いた prop（基本の書き方）

　prop NAME <- `∀ ??p^ ( ψ )`
内部では schema と同じに扱います。仮引数は ψ の中の ??p^ の出現の引数です（x ??p^ y なら x, y。どの出現でも同じ名前の並びでなければ理由付きで拒否）。代入する式の中で、仮引数以外の自由変数はすべて共有変数として残ります。∀ に書ける述語変数は1つです（複数は schema 宣言で）。
例（0_tutorial_AI/6.book「置換公理」）
　prop ax_r <- `∀ ??p^ ( ∀ x \, [ ！ y \, x ??p^ y ] ⟹ ∀ X \, Exi \{ cls y | [ ∃ x ∈ X . x ??p^ y ] \} )`
　thm ax_s ◀ ax_r
　prf ax_s --| ax_r[??p^:= $x \in C , y = x$ ] v;
　　　ax_s ◀ ax_r h;

7.2 schema 宣言（仮引数と共有変数を宣言する書き方）

　schema NAME(??p^;x,y;C_) := $\psi$
最初の欄が局所述語、次の欄がその仮引数、最後の欄が共有変数です。共有変数に挙げた名前だけは、代入式の中で仮引数以外の自由な変数として使ってよく、代入後も自由なまま残ります。
複数の局所述語は、述語ごとに自分の括弧で仮引数を持ちます（schema NAME(P_1(x_1,...),P_2(y_1,...);shared_1,...) := $\psi$）。
インスタンスはSOURCE[P:=$\theta$]と書き、全ての局所述語へ同時に代入します（SOURCE[P_1:=,P_2:=]）。一部の局所述語だけを代入することはできません。
例（同じ置換公理を schema 宣言で）
　

schema ax_r(??p^;x,y;C_) :=  \(\forall x \, ! y \, x \mathbin{p} y \Longrightarrow \forall X \, \dot\exists \{ y \mid \exists x \in X . x \mathbin{p} y \}\)

インスタンスは prf の段の sos に直接書けます（!prop 名 <- SOURCE[P:=$\theta$] で名前を付けて使っても同じ）。インスタンスを使うThmの主張の sos には、その出所の名前（Σ）を裸で書きます。欠けていれば結論の段が通りません。Σ を書ける所は 6.book「分出公理」の節の表（∀ の prop と同じ）です。
主張（thm 行）の sos に生の SOURCE[P:=θ] を書くことはできません。

7.3 高階翻訳

schema宣言には宣言ごとの識別子を付け、型を指定した相異なる局所述語 $R_1,\ldots,R_j$ と本体 $\psi$ を持たせます。
局所変数のスコープは、そのschemaの本体だけです。本体中の同名の出現は、内側にその名前の束縛がなければ、この局所宣言に結び付けます。同名の共有変数や他のschemaの局所変数とは別の変数です。
スコープを解決した後、局所変数を他の変数と衝突しない名前に $\alpha$ 改名します。

schemaの高階翻訳を $K(S)=\forall R_1\cdots\forall R_j\,U(\psi)$ とします。
通常の仮定を $A_1,\ldots,A_m$、schemaを $S_1,\ldots,S_n$、共有する高階変数の列を $\bar P$ として、全体の翻訳は次です。
　$H(\mathcal{T})=\forall\bar P\,(((\bigwedge_i U(A_i))\land(\bigwedge_j K(S_j)))\Rightarrow U(G))$
例：通常の仮定が $R:o$、goalが $\bot$、schemaが「局所変数 $R:o$、本体 $R\Rightarrow Q$」の場合、
　$H(\mathcal{T})=\forall R\,\forall Q\,((R\land\forall R_0\,(R_0\Rightarrow Q))\Rightarrow\bot)$
schema内の局所 $R$ だけを $R_0$ に改名しました。schema本体にしか出てこない $Q$ も、外側の共有量化に含まれます。

7.4 インスタンス指定列 |inst[I]

|inst[I] の I は、sos中のschemaをSOURCEとして、局所述語への型の合う代入を指定した有限列です。同じSOURCEから複数のインスタンスを選べます。
代入式は指定箇所の共有環境で解決します。SOURCEの局所宣言は、代入式の中へスコープを伸ばしません。
生成した式を $B_1,\ldots,B_l$、通常の仮定の列を $\Gamma_0$、schema宣言の列を $\Sigma$ として、
　(G ◀ Γ₀ , Σ)|inst[I] = G ◀ Γ₀ , Σ , B₁ , … , Bₗ
とします。SOURCEを含まない指定や型の合わない代入は不適法です。空の I は恒等です。
高階側ではschema仮定の全称量化から各インスタンスを導けるので、この追加は元のThmの高階翻訳と同値です。
一階証明器には、通常の仮定と選んだインスタンスを渡します。schema宣言自体は証明の根拠を示す記録として保持し、普通の一階の仮定としては渡しません。
この一階の問題が証明できれば、元のschemaを含むThmも高階側で成立します。有限個のインスタンスを選ぶこの方法が、高階証明のすべてを再現できるとはしません。

8 翻訳と代入の対応

代入後に高階へ翻訳した式と、高階へ翻訳してから対応するラムダ式を代入した式は、捕獲を避ける同じ規則により、全称閉包を付ける前の式として $\alpha\beta$ 同値です。

全称閉包と代入の補題：同時代入 $\rho$ の各右辺が「代入は型を合わせ、捕獲を避ける」節の範囲に入り、型が一致するとします。代入は捕獲を避けて行い、結果を $\beta$ 簡約します。
このとき、$U(F[\rho])$ と $U(F)[\rho]$ は論理的に同値です。ここで $F$ は、翻訳後・個体変数の全称閉包前の式です。
右辺は新しい自由な個体変数を持ち込まず、もとの自由変数を消すことだけがありうるからです。差は消えた変数への空虚な全称量化で、非空の型ではそれを除いても論理的に同値です。
例：$F=R(x)$、$\rho(R)=\lambda u.\top$ の場合、$U(F[\rho])=\top$、$U(F)[\rho]=\forall x\,\top$ です。記号列としては一致しませんが、論理的には同値です。

インスタンス生成と構造的な翻訳の補題：型付きの式を構造に沿って移す翻訳を $f$ とします。次は交換の十分条件です。
① $f$ は元の通常の式、SOURCEの本体、代入式のすべてに定義され、型・適用・論理記号・束縛先を保つ。記号の対応はThmと指定列の全体で1つに固定し、変数を同じ型の変数へ移す。
② schemaを記録として保持し、宣言の識別子と局所・共有変数の対応を翻訳前後で保つ。適法性の判定も同じ結果になる。
③ 代入式は「代入は型を合わせ、捕獲を避ける」節の範囲に入り、生成する式も翻訳可能である。一階証明器に渡す式は|v-elimの節の範囲に入る。
このとき (T|inst[I])|f と (T|f)|inst[f(I)] の対応する式は、閉包前には $\alpha\beta$ 同値で、閉包後は論理的に同値です。
|0 や {s,c}ソート翻訳も、この条件を満たす範囲でこの補題を適用できます。変換で消える記号がある場合などは、代入前のSOURCE・代入式にも翻訳が定義されるかを別に確かめます。

9 推論関係とbackend

翻訳（どの .thmel でも同じ）：
　${\tt P}$が$\mathbb{W}$[c]を含んでいなければ ${\tt P}$|0 = (${\tt P}$を高階言語（ソートの無い言語）に自然に翻訳したもの)、そうでなければエラー（3.book「Thmの変換 |0」）
　素の ◀ と --| は{s,c}ソートのまま扱う（0_tutorial_AI/5.book「--| の仕組み」節）

trust文（Iはインスタンス指定列。省略時は空列で恒等）：
　trust $\mathcal{T}$ if Iが$\mathcal{T}$に対する適法なインスタンス指定列であり、$\mathcal{T}$|inst[I]|cvt+|0 holds in $\mathbb{L}_{\mathrm H}$
　trust $\mathcal{T}$ if Iが$\mathcal{T}$に対する適法なインスタンス指定列であり、$\mathcal{T}$|inst[I]|fn-elim|cls-elim +sos $\mathbb{W}_\mathrm{c}.$ holds in $\mathbb{L}_{\mathrm{Hsc}}$
略記：
　${\tt P}$ -| $\Gamma$ … (${\tt P}$ ◀ $\Gamma$)|inst[I]|cvt+|0
　${\tt P}$ --| $\Gamma$ … (${\tt P}$ ◀ $\Gamma$)|inst[I]|fn-elim|cls-elim +sos $\mathbb{W}_\mathrm{c}.$

Prover9・Vampireは高階変数を扱えないので、prover+・vampire+は|v-elimをしてから一階の問題にして投げます。
satallax+も、Thm に自由に現れる高階変数を、goal・sos 共通の1つの定数（THF の型付き定数）として渡します。これは $H(\mathcal{T})$ の外側の $\forall P$ を、新しい定数に置き替えたものと同値です（一階側の|v-elimと同じ考え方）。
式ごとに $\forall$ で閉じてはいけません。sos の $P$ を $\forall P\,P$ と閉じると矛盾になり、 ${\perp} P$ が示せてしまいます（2026-10-04 まで satallax+ がそうなっていて、外部の査読で見つかり直しました）。
したがって3つの投げ先は同じ主張を判定します。Thm に自由に現れる高階変数（∀ を書いていないもの）へ式を代入したいときは、証明器に探させず、∀ を書いた prop か schema の実例を書きます。
例外：.thmel に satallax+ predicate:all と書いた本で、--| … s; の段の sos に裸の名前で書いた ∀ の prop（∀ ?R^ ( ψ )）は、その式1本の中で ∀ を閉じた高階の公理 $\forall R\,\psi(R)$ として渡します。∀ が式に書いてあるので、これは前提の意味（すべての R について）そのものです。Satallax は代入する式を自分で探します（practice.book）。
2つの読み方の違い：Book の代入 θ に書けるのは、クラスや述語を量化しない式だけです（ZF の公理図式の読み方＝predicate:formula）。Satallax の高階の $\forall$ は、クラスや述語を量化するλ項も含めてすべてを走ります（predicate:all）。後者は ZF より強い集合論（MK 型）の強さで、ZF では示せない主張が〇になりえます。そこで既定は formula で、all は書いた本だけです。\cls の内包も同じで、formula では内包の定義公理を、式に出てきた述語（Thm 全体の定数）についての具体例だけにします。all では、定義公理の中の述語変数を ∀ で閉じます（任意のλ項の内包が取れる）。

例　 ${R} a \Rightarrow {R} a$ は
　-| … p;／-| … v;：|?R^ a ⇒ |?R^ a
　-| … s;：thf(ty_vs, type, vs: $i > $o).　thf(goal, conjecture, ((vs @ a) => (vs @ a))).（vs は ?R^ の定数）

10 高階変数を含むThm

$P \Rightarrow P$ $\blacktriangleleft$ O
|v-elimでgoal内の $P$ は新しい記号に替わり、 $\mathrm{P} \Rightarrow \mathrm{P}$ になります。
$P$ $\blacktriangleleft$ $P$
goal・sosの $P$ は同じ記号に替わるので、 $\mathrm{P} \mathrm{P}$ として1段で示せます。
${\perp} \Rightarrow P$ $\blacktriangleleft$ O
素の ◀ でも同じです。|v-elimをすると ${\perp} \Rightarrow \mathrm{P}$ ◀ O になり、vampire+ が判定します。
$x = y \Rightarrow {f} x = {f} y$ $\blacktriangleleft$ O
関数変数も同じです。${f}$ は新しい関数記号に替わります。

次は成り立ちません。
　${\perp}$ ◀ $Q$ , $\neg R$ … $\sigma$($Q$) $\ne$ $\sigma$($R$) なので矛盾しません（$Q=\top$、$R=\bot$ が反例）。
　 ${f} x = {g} x$ ◀ O … 異なる関数変数は異なる記号に替わります。
次は成り立ちます。
　${\perp}$ ◀ $P$ , $\neg P$ … 同じ $\sigma$($P$) による矛盾です。

11 参照した高階論理の仕様

TPTPの型・THF・ラムダ式と適用
TPTP言語仕様：TH0のHenkin意味論・外延性・選択
Leo-III：Henkin意味論と選択を持つ高階論理
Satallax：高階論理とHenkinモデルに対する証明手続き