日本ソフトウェア科学会第 39 回大会 (2022 年度) 講演論文集

帰納的推論の計算複雑性
伊藤 宗平

龍田 真

帰納的に定義された関係や構造に関する形式的推論は, 数学的興味のみならず計算機科学的重要性も広く認識されており, プログラムやアルゴリズムの性質の検証などへの応用を持つ. 帰納的推論の体系として近年注目を集めている
ものにシーケント計算に基づく LKID, LKIDω , CLKIDω と呼ばれる体系がある. これらの証明能力の関係についてはこれまで明らかにされてきたが, 証明可能性の計算複雑性については議論されてこなかった. 本稿では LKID と
CLKIDω の計算複雑性は Σ01 完全であることを示す. また LKIDω の計算複雑性は Π11 完全であることを示す.

無限木となる. 最後に CLKIDω は LKIDω の証明の

1 はじめに中で正規なもの, つまり有限個の異なる部分木のみを

帰納あるいは再帰は様々な集合の定義ならびに計算含むような証明木のみを許した体系である. これらはを行うにあたり不可欠な原理である. プログラミング

いずれも互いに証明能力が異なることが知られてい言語においては木やリストなど様々なデータ構造がる [4] [1] [17].

帰納的に定義され, そのような構造上の計算も帰納的

これらの体系により, 帰納的に定義された述語のに定義されることが多い. したがって, 帰納的に定義

様々な性質の証明が形式化できるため, 計算機によりされた構造や関係に対しては, 帰納的推論により数学

その証明の探索を実現したいというのは自然な発想で的にその性質を議論することが必要となる. このようある. しかしながらこれらの体系による証明探索の計な帰納的推論を形式化した推論体系として近年注目

算複雑性についてはこれまで議論されてこなかった.

を集めているのが, シーケント計算に基づく LKID,

そこで本研究ではこれらの体系の計算複雑性についωω

LKID ,CLKID [3] [4] と呼ばれる体系である. これて調査し明らかにすることを目的とする.

らの推論体系はいずれも一階述語論理に帰納的述語

本稿で明らかにする事実は以下の３つである.

の定義を含めた論理（FOLID と呼ばれる）に対する

1. LKID の証明可能性は Σ01 完全である.

ものである.

2. CLKIDω の証明可能性は Σ01 完全である.

LKID は Martin-Löf の帰納的推論体系 [15] をシー

3. LKIDω の証明可能性は Π11 完全である.

ケント計算で形式化した体系であり, 通常の帰納法のΣ01 関係は帰納的可算関係と等価であり, 例えば一原理を形式化したものである. 一方 LKIDω は無限降

階述語論理の証明可能性も Σ01 完全である. したがっ下法による推論を形式化したもので, 証明木は一般にて LKID と CLKIDω の証明可能性問題は計算可能で∗ Complexity of inductive reasoning.

This is an unrefereed paper. Copyrights belong to
the Author(s).
Sohei Ito, 長崎大学情報データ科学部, Dept. of Information and Data Sciences, Nagasaki University.
Makoto Tatsuta, 国立情報学研究所 / 総合研究大学院大学, National Institute of Informatics / Sokendai.

あり, 計算機による証明探索に適した推論体系である
ことが示される.
一方 LKIDω については証明可能性が Π11 完全であることから, LKIDω の証明可能性問題は計算不可能
であり, 自動推論には不向きであることが明らかになった.

本論文は以下のように構成されている. 2 節では

チャΣ を一つ固定し, 関数記号を f1 , f2 , ..., 通常の述関連研究について述べる. 3 節では帰納的述語を含語記号を Q1 , Q2 , ..., 帰納的述語記号を P1 , P2 , ..., Pn

む一階述語論理 FOLID を紹介する. 4 節では, 推論と表すこととする. また, t(x1 , ..., xm ) は項で, t 中に

体系 LKID, LKID , CLKID を紹介する. 5 節では出現する変数が {x1 , ..., xm } に含まれることを表す.

LKID の証明可能性の計算複雑性について述べる. 6

FOLID の式は, 等号を含む通常の一階述語論理の論

ω

ω

ω

節では CLKID の証明可能性の計算複雑性について
ω理式である.

述べる. 7 節では LKID の証明可能性の計算複雑性

FOLID の関数記号, 通常の述語記号は通常の一階述について述べる. 8 節では明らかになった事実に対す語論理と同様の構造 M で解釈される. 変数は環境 ρ

る考察を述べる. 9 節ではまとめと今後の課題を述で M の台 D の要素として解釈される. FOLID の式

べる.

F がモデル M で充足されることを M |=ρ F と表す.
帰納的述語はそれが意図する意味の通りに解釈が2 関連研究与えられる. 帰納的述語の意図する意味は次のような

循 環 証 明 体 系 は, [4] に よ り 提 案 さ れ, そ の 後,

定義集合 (deﬁnition set) で与えられる.

Martin-Löf 式の従来の帰納的定義の論理体系との証明可能性の比較 [2] [17] [1] [7] や, 他の論理への適用

定義 1 (帰納的定義集合) シグネチャΣ に対する帰納としてプログラム停止性の論理体系 ( [5]), 分離論理的定義集合 Φ は以下のような生成規則 (production[12] [20] [19] など活発に研究されてきている.

rule) の有限集合である.
Q1 (u1 ) ... Qh (uh ) Pj1 (t1 )Pi (t)

論理の証明可能性の計算複雑性に関しては以下のも...

Pjm (tm )のが知られている. Σ01 完全であることが知られてい(1)る論理としては, 通常の一階述語論理や, 一階の証明

ここで j1 , ..., jm , i ∈ {1, ..., n} で, 太字の記号は各述可能性である PA, PRA [8] がある. Π11 完全であるこ

語記号のアリティと等しい長さの項のベクトルである.

とが知られている論理としては, 二階の証明可能性である PRA2 , PA2 , ω-logic [8] などがある. 他に, ダ

以下では表記を単純化するために Q(u) などの括

イナミック論理 (DL) やおよび構成的無限論理 Lωck ω

弧を省略し Qu 等のように表すことがある. また, 項の証明可能性も Π11 完全であることが知られている中に含まれる変数を明示するために Q(u(x)) のよう[11] [13] [10]. また, 特定のシグネチャを持つ論理に対な表記を用いることもある（x は変数のベクトル）.

1

する計算複雑性に関する研究も行われており, 例えばPersburger 算術や Skolem 算術 (自然数上の × と =の算術) に一つ単項述語記号を加えた論理も Π11 完全

例 1 帰納的述語 N を以下の生成規則により定める.
Nx
N 0 N sxであること [9] [18] や, ラベル付き木の部分木関係を持ここで s は「後継者関数」を意図する単項関数記号でつ一階の論理が Σ11 完全であること [14] [6] が分かってある. この述語 N は「自然数である」という関係をいる.

意図している.

3 帰納的述語を含む一階述語論理 FOLID

帰納的述語の生成規則より, 任意の対象領域 D 上で単調な作用素が自然に定められる. ここで帰納的述語

この節では帰納的に定義される述語（帰納的述語）

Pi のアリティを ki とすると, 対応する単調な作用素はを持つ一階述語論理 FOLID の構文と意味論を紹介

φi : P(Dk1 ) × ... × P(Dkn ) → P(Dki ) の型の作用素する.

となる. 直感的には, 各 P1 , ..., Pn の解釈 X1 , ..., Xn

FOLID の言語は通常の一階述語論理の (可算な) 言
語に加え, 帰納的述語 (inductive predicate) として区別される有限個の述語記号からなる. 本節ではシグネが与えられたとき, 新たな Pi の解釈は φi (X1 , ..., Xn )

で定まることになる.

対し PiM =S

αα Pi であることをいう.

定義 2 (定義集合作用素) M をシグネチャΣ の一階

FOLID (Σ, Φ) の別の意味論として Henkin 意味論の構造とし, その台を D とする. 各 i ∈ {1, ..., n}(Henkin semantics) がある. Henkin 意味論 (Henkinに 対 し, ki を 帰 納 的 述 語 記 号 Pi の ア リ ティと すsemantics) では, ある Henkin クラス H = {Hk ⊆る. 定義集合 Φ 中の Pi を結論に持つ生成規則のP(Dk ) | k ∈ N} が与えられたとき, 帰納的述語 Pi は集合を Φi とする. Φi 中の r 番目の規則を式 (1)H 中の最小前不動点として解釈される. したがって,の 形 の も の と す る と き (1 ≤ r ≤ |Φi |), 作 用 素Henkin 意味論におけるモデルは M と H の対 (M, H)

φi , r : P(D ) × · · · × P(Dである. Henkin クラスの正式な定義については文献

k1kn) → P(D ) を以下
ki[4] を参照されたい.

のように定める.

一つ言及すると, 標準モデル M は Hk = P(Dk ) と

φi,r (X1 , ..., Xn ) =M{ρ(t) | QM
1 (ρ(u1 )), . . . , Qh (ρ(uh ))},

ρ(t1 ) ∈ Xj1 , ..., ρ(tm ) ∈ Xjm , ρは環境 }ここで環境 ρ は項のベクトルに対し適用されているが, これは要素ごとに ρ を適用したベクトルである.
次に, 作用素 φi を i ∈ {1, ..., n} に対し以下のように定める.

φi (X1 , ..., Xn ) =[φi,r (X1 , ..., Xn )r

最後に Φ の定義集合作用素 φΦ を次のように定める.

φΦ (X1 , ..., Xn )=(φ1 (X1 , ..., Xn ), ..., φn (X1 , ..., Xn ))定めた時の H = {Hk | k ∈ N} の場合の Henkin モデ
ル (M, H) とみなすことができるため, 標準モデルはHenkin モデルの特殊な場合である.
標準意味論を用いることで自然数上の順序を表現することができる.
補題 1 ΣN を二項関係記号 ≥, 単項関係記号 N , 単項関数記号 s, 定数記号 0 からなるシグネチャとする.
ここで N と ≥ は以下の生成規則 ΦN により定義される帰納的述語である.
Nx
Nx
N 0 N sx x ≥ 0x≥ysx ≥ sy

定義 3 (近似値) M をシグネチャΣ の一階の構造とM を (ΣN , ΦN ) の 標 準 モ デ ル で, ∀x(sx 6= 0) とし, その台を D とする. φΦ を Φ の定義集合作用素と∀x∀y(sx = sy → x = y) を満たすモデルとすると, N M ∼= N で ≥M は N 上の自然な順序関係 ≥N とする. このとき, 順序数でインデックス付けされた集
k1
kn))α≥0 を次のように合 (φαΦ ⊆ P(D ) × · · · × P(D同型である. さらに, ≥M は反射律, 推移律, 反対称律

定める.

を満たす.

φα
Φ =

[

φΦ (φβΦ )β<α

証明 N M ∼= N であることは, 標準意味論の重要な帰これより φ0Φ = (∅, . . . , ∅) であることに注意されたい.

結であり詳しくは [4] を参照されたい. いま, M は標

このとき πin (φαΦ ) を Pi の α 番目の近似値 と呼び,準モデルなので, 標準モデルの定義より∞[≥M =φn (∅).

Piα と表す. ここで πin は πin (X1 , ..., Xn ) = Xi で与えられる.

(X1 , ..., Xn )n=0

こ こ で, φ(X) = {((sM )n 0M , 0M ) | n ∈ N} ∪⊆φΦ (X1 , ..., Xn ) を 満 た す 組(X1 , ..., Xn ) を, φΦ の前不動点という. φΦ の最小{(sM x, sM y) | (x, y) ∈ X} である. これより
≥M = {((sM )n 0M , (sM )m 0M ) | n ≥ m, n ∈ N, m ∈ N}

前不動点は ∪α φαΦ で与えられることは周知の事実である.

(2)が成り立つ. 次に, n ≥N m ⇔ ((s ) 0 , (s ) 0 ) ∈≥M
M n M

M m M

を示す.
定義 4 (標準モデル) 一階の構造 M が (Σ, Φ) に対する標準モデルであるとは, すべての i ∈ {1, ..., n} に(⇒ の 証 明) n≥Nm な ら, 式 (2) よ り((sM )n 0M , (sM )m 0M ) ∈≥M であるため成り立つ.
(⇐ の証明) ((s ) 0 , (s ) 0 ) ∈≥
M n M

M m M

M

（これを帰納規則 (induction rule) と呼ぶ）を述べる

なら, 式(2) より n ≥N m である.

まえに, 一つ定義をしておく. 生成規則の集合を Φ とし, Φ 中の帰納的述語 Pi を結論に持つ生成規則におしたがって 0M 7→ 0 ∈ N, (sM )n 0M 7→ n ∈ N で定められる一対一対応により ≥Mは N 上の自然な順序

いて, Pj が前提に出現している場合, Prem(Pi , Pj ) が成り立つと定める. Prem の反射推移閉包を Prem ∗とする. Prem ∗ (Pi , Pj ) かつ Prem ∗ (Pj , Pi ) が成り立関係 ≥N と同型であることが示される.

≥M が反射律, 推移律, 反対称律を満たすことは式□(2) より自明である.

つとき, Pi と Pj が相互に依存するという.
帰納的述語 Pj をシーケントの左側に導入する規則を述べる. まず, 全ての帰納的述語 Pi に対し帰納変

4 帰納的推論体系

数と呼ばれる変数の組 zi を対応付ける. zi の長さは

本節では, 前節で導入した帰納的述語を含む論理

Pi のアリティki と一致するものとする. さらに, Pjω

と相互に依存する全ての帰納的述語 Pi に対し, 帰納を紹介する. いずれも Brotherston らによって導入さ法の仮定と呼ばれる勝手な式 Fi が定まっているとすれた推論体系だが, いずれも能力的に異なることが知る. Fi は帰納変数 zi の（いくらかを）含んでいてもられている [4] [1].

よい. この時, i ∈ {1, ..., n} に対し式 Gi を以下のよω

FOLID に対する推論体系 LKID, LKID , CLKID

4. 1 LKID
本節では帰納的推論体系 LKID について述べる.

LKID は Gentzen のシーケント体系 LK に帰納的述語に対する推論規則を加えたものである. 図 1 に LKの推論規則の一覧を示す. なお, シーケント Γ ` ∆では Γ と ∆ は論理式の集合であるとし, 縮約規則

(contraction rule) は暗黙に含まれている. LK の推

うに定める
 .
 F
i
Gi =
 Pi (zi )Pi と Pj が相互に依存している

それ以外
帰納的述語 Pj に対する帰納規則のインスタンスは以下の図式で与えられる.
小前提

Γ, Fj (u) ` ∆(Ind Pj )Γ, Pj (u) ` ∆論規則で結論部に新しく導入される式を, その規則のPj と相互に依存するすべての帰納的述語 Pi に対し,インスタンスの主式 (principal formula) という. 帰Pi を結論に持つ Φ 中の規則すべてに対応した小前提

納的述語の生成規則に基づき, 帰納的述語をシーケン(minor premise) がこの規則の前提に現れる. ここでトの右側に導入する規則と左側に導入する規則を各Pi を結論に持つ生成規則
Q1 u1 (x) ... Qh uh (x) Pj1 t1 (x)Pi t(x)

帰納的述語ごとに用意する.
例として帰納的述語 Pi に対する式 (1) の形の生成規則
Q1 u1 (x)...

Qh uh (x) Pj1 t1 (x)Pi t(x)...

Pjm tm (x)...

Pjm tm (x)に対し, これに対応する小前提は

Γ, Q1 u1 (y), ..., Qh uh (y),Gj1 t1 (y), ..., Gjm tm (y) ` Fi t(y), ∆を考えたとき（これを Pi を結論部に持つ規則のうちとなる. ここで y は x と同じ長さの, 異なる変数のベクの r 番目のものとする）, シーケントの右側に導入すトルで, 全ての y ∈ y に対し y ∈/ FV (Γ ∪ ∆ ∪ {Pj u})

る規則は以下のようになる.

である（FV は自由変数を返す関数である）. また, tを ki 個の項からなる組とするとき, Gi (t) で Gi [t/zi ]Γ ` Q1 u1 (u), ∆...

Γ ` Qh uh (u), ∆Γ ` Pj1 t1 (u), ∆...

Γ ` Pjm tm (u), ∆Γ ` Pi t(u), ∆を表すものとする. Gi [t/zi ] は Gi 中に出現する変数(Pi Rr )zi を対応する t 中の項で置き換えたものである.
例 2 例 1 の「自然数である」という関係を表す単項

帰納的述語 Pj をシーケントの左側に導入する規則

帰納的述語記号 N に対する帰納規則は以下のように

構造規則

Γ`∆

Γ′ ` ∆′(Wk) ただしΓ′ ⊆ Γかつ∆′ ⊆ ∆Γ`∆(Axiom) ただしΓ ∩ ∆ 6= ∅Γ ` F, ∆ Γ, F ` ∆
(Cut)
Γ`∆

論理規則

Γ`∆
(Subst)Γ[θ] ` ∆[θ]Γ ` F, ∆(¬L)
Γ, ¬F ` ∆Γ, F ` ∆(¬R)Γ ` ¬F, ∆Γ, F ` ∆ Γ, G ` ∆(∨L)Γ, F ∨ G ` ∆Γ ` F, G, ∆(∨R)
Γ ` F ∨ G, ∆Γ ` F, ∆ Γ ` G, ∆(∧R)
Γ ` F ∧ G, ∆Γ, F, G ` ∆(∧L)Γ, F ∧ G ` ∆Γ ` F, ∆ Γ, G ` ∆(→ L)Γ, F → G ` ∆Γ, F ` G, ∆(→ R)
Γ ` F → G, ∆Γ, F [t/x] ` ∆(∀L)Γ, ∀xF ` ∆Γ ` F, ∆(∀R) ただし x ∈/ FV (Γ ∪ ∆)Γ ` ∀xF, ∆Γ, F ` ∆(∃L) ただし x ∈/ FV (Γ ∪ ∆)Γ, ∃xF ` ∆Γ ` F [t/x], ∆(∃R)Γ ` ∃xF, ∆Γ[u/x, t/y] ` ∆[u/x, t/y](= L)Γ[t/x, u/y], t = u ` ∆[t/x, u/y]Γ ` t = t, ∆

図1

LK の推論規則Γ ` ∆ は Henkin 妥当である. さらに, Γ ` ∆ がなる.

Γ ` F 0, ∆(= R)

Γ, F x ` F sx, ∆Γ, N t ` ∆Γ, F t ` ∆Henkin 妥当ならば LKID でカットなしに証明可能で(Ind N )ある.
すなわち, LKID は FOLID の Henkin 意味論にお次に, シーケント Γ ` ∆ の意味論における妥当性

いて完全で健全な推論体系である.

について定義する.
定義 5 (M, H) を (Σ, Φ) の Henkin モデルとする.
シーケント Γ ` ∆ が (M, H) で真であるのは, 全ての
環境 ρ に対し, 全ての J ∈ Γ に対し M |=ρ J である
ならば, ある K ∈ ∆ に対し M |=ρ K であることをいう. シーケントが全ての Henkin モデルで真のとき,

Henkin 妥当 (Henkin valid) という. シーケントがすべての標準モデルで真のとき, 妥当 (valid) という.

LKID については以下の事実が知られている.
定理 1 ( [4]) Γ ` ∆ が LKID で 証 明 可 能 な ら ば

4. 2 LKIDω
本節では FOLID の無限降下法による証明を形式化した推論体系 LKIDω を紹介する. LKIDω は無限の導出木を証明とする推論体系である. LKID では LKの推論規則に加え, 帰納的述語をシーケントの左側に導入する規則として (Ind) 規則を用いたが, LKIDω
では以下のようなケース分割規則 (case-split rule) を用いる.

(複数の) ケース別前提
Γ, Pi u ` ∆(Case Pi )

ここで帰納的述語 Pi が下記の生成規則を持つとす
ると,Q1 u1 (x)スはシーケントの列 (Si )0≤i<α (α ∈ N ∪ {∞}) であり, 全ての i + 1 < α に対し Si+1 が Si の子であるも...

Qh uh (x) Pj1 t1 (x)Pi t(x)...

Pjm tm (x)

この規則に対応するケース別前提 (case distinction)
は以下のようになる.

のをいう.
定義 8 (トレース) D を LKIDω の前証明とし, (Γi `∆i )i≥0 を D 中のパスとする. この時 (Γi ` ∆i )i≥0 を

Γ, u = t(y), Q1 u1 (y), ..., Qh uh (y),追跡する (follow) トレースは Γi 中の原子論理式の列

Pj1 t1 (y), ..., Pjm tm (y) ` ∆(τi )i≥0 ですべての i に対し以下を満たすものをいう.

ここで y は x と同じ長さの, 異なる変数のベクトルで,全ての y ∈ y に対し y ∈/ FV (Γ ∪ ∆ ∪ {Pj u}) である.
ケース別前提中に現れる式 Pj1 t1 (y), ..., Pjm tm (y)は主式 Pi u のケース後続 (case-descendant) と呼ばれる.

1. τi = Pji ti , ここで ji ∈ {1, ..., n}2. Γi ` ∆i が推論規則 (Subst) の結論であるならば, τi = τi+1 [θ]. ここで θ はこの推論規則のインスタンスによって定まる代入である.

3. Γi ` ∆i が推論規則 (=L) の結論で, その主式が例 3 例 1 の「自然数である」という関係を表す単項
帰納的述語記号 N に対するケース分割規則は以下のようになる.

s = t であるならば, ある式 F と変数 x, y に対し
τi = F [t/x, u/y] で τi+1 = F [u/x, t/y] である.
4. Γi ` ∆i がケース分割規則の結論であるならば,(a) τi+1 = τi であるか, (b) τi はこの規則インス

Γ, t = 0 ` ∆Γ, t = sx, N x ` ∆Γ, N t ` ∆タンスの主式で τi+1 は τi のケース後続である.

(Case N )5. Γi ` ∆i がそれ以外の規則の結論であるならば,この推論規則の主式は N t, ケース後続は N x である.

LKIDω の証明は無限でもよい導出木となる. ここで, 導出木に出現する子ノードを持たないノードのうち, 公理（すなわち前提を持たない推論規則の適用例）
であるものを葉 (leaf ), それ以外のものを芽 (bud) と呼ぶ. 芽はまだ推論規則を適用されていないシーケン
トを意味している.

LKIDω の推論規則を適用していって得られた（無限）導出木が健全な証明であることは保証されない.
定義 6 (LKIDω の前証明) シーケント Γ ` ∆ を結論に持ち, LKIDω の推論規則に従って構成した（無限になることもある）芽を持たない導出木 D を LKID

後者の場合, i は前進点 (progress point) という.

τi+1 = τi である.
無限個の前進点を持つトレースを無限に前進するト
レースと呼ぶ.
定義 9 (大域トレース条件, LKIDω の証明) LKIDω
の前証明 D 中の全ての無限パス (Γi ` ∆i )i≥0 に対し, ある末尾パス (Γi ` ∆i )i≥k (k ≥ 0) を追跡する無限に前進するトレースが存在するとき, D は大域ト
レース条件を満たすという. LKIDω の前証明 D が大域トレース条件を満たすとき, D は LKIDω の証明であるという.

LKIDω については以下の事実が知られている.

ωの前証明 (pre-proof ) と呼ぶ.

定理 2 ( [4]) Γ ` ∆ が LKIDω で証明可能ならば

Γ ` ∆ は（標準意味論において）妥当である. さら
前証明が正しい証明であることを保証するのが後述
する大域トレース条件 (global trace condition) であに, Γ ` ∆ は（標準意味論において）妥当であるならば Γ ` ∆ は LKIDω で証明可能である.

る. この条件を正確に定義する前に必要な定義を行う.
すなわち, LKIDω は FOLID の標準意味論において
定義 7 (パス) 導出木中の（有限または無限の）パ完全で健全な推論体系である. 妥当性は Henkin 妥当性に含まれるため, LKIDω で証明可能な式は LKID

で証明可能な式よりも真に大きい.

である.

Q1 x1 ...Qn xn ϕ
4. 3 CLKIDω

ここで各 Qi は ∃, 各 xi は個体変数 (individual vari-

CLKIDω は LKIDω を正規木に制限した証明体系able), ϕ は決定可能な論理式である.

である. すなわち, 有限個の異なる部分木しか持たないような導出木である. そのような木は直感的には循
環的な構造で表現できるため有限の表現を持つ. これより CLKIDω の証明を形式的に定義する.

証明 LKID の証明は有限木であるため, （ゲーデル
符号化などにより）自然数で表現することができる.

定義 10 (供) B を導出木 D の芽とする. D 中の内部ノード C が B と同じシーケントであるとき, C を

B の供 (companion) という.
定義 11 (循環前証明) シ ー ケ ン ト Γ

定理 4 LKID の証明可能性は Σ01 関係である.

したがってすべての自然数を列挙し, それぞれが証明したいシーケントの正しい証明であるかどうかを判定すれば良い. これは明らかに通常のチューリング機
械で計算可能である.

`∆ のCLKIDω 前証明 P は対 (D, R) である. ここで D□

定理 5 LKID の証明可能性は Σ01 困難である.

は Γ ` ∆ を根に持つ LKIDω の推論規則によって構

証明 LKID の証明可能性は FOLID の Henkin 妥当

成された有限導出木であり, R は D 中の全ての芽を性と等価である. ここで FOL の妥当性は FOLID の供に対応させる関数である. P のグラフ GP は, D に(Henkin/標準) 妥当性でもあるのは明らかである（帰おいて全ての芽 B をその供 R(B) と同一視すること

納的述語の集合を ∅ とすればよい）. FOL の妥当性により得られるグラフである.

は Σ01 完全であることは良く知られた事実であるた

定義 12 (循環証明) CLKIDω の前証明 D において,め, FOLID の妥当性は Σ01 困難である.

□

定理 4 と 5 より以下が成り立つ.

そのグラフが大域トレース条件を満たすとき, D を

CLKIDω の証明と呼ぶ.

系 1 LKID の証明可能性は Σ01 完全である.

ペアノ算術の公理を含むとき, LKID と CLKIDω
の証明可能性は一致することが知られているが [2],6 CLKIDω の計算複雑性

LKID と CLKIDω の証明能力の違いについては以下

本節では CLKIDω の証明可能性問題が Σ01 完全での事実が知られている.

あることを示す. この証明には以下の補題を用いる.

定理 3 ( [1]) LKID で 証 明 可 能 な 式 の 集 合 は

補題 2 ( [11],Proposition 2.5) 集合 A が帰納的可ω

CLKID で証明可能な式の集合よりも真に小さい.

算であるのは, ある決定可能な二項述語 φ が存在してA = {x | ∃yφ(x, y)}

5 LKID の計算複雑性
本節では LKID の証明可能性問題, すなわち FOLIDの Henkin 意味論における妥当性問題が Σ01 完全であることを示す. Σ01 関係は算術的階層の一つであり, 通常のチューリング機械で (部分) 計算可能な関係, すなわち帰納的可算な関係である.
形式的には以下の論理式で定められる N 上の関係と表せるとき, かつその時に限る.
定理 6 CLKIDω の証明可能性問題は Σ01 完全である.
証明 まず, CLKIDω の証明可能性問題が Σ01 困難であることを示す. あるシグネチャΣ を持つ FOL のシー

ここで各 Qi は ∃ または ∀ のいずれかであり, 各 Xi

ケント Γ ` ∆ を考える. この時, シグネチャ(Σ, ∅) をは関係あるいは関数変数記号で, ϕ は算術的階層の論

持つ FOLID において CLKIDω で Γ ` ∆ が証明可能

理式, つまりある n に対して Σ0n または Π0n であるよ

であるならば, 明らかに Γ ` ∆ は LK で証明可能でうな論理式である.

ある. また, 逆に CLKID で Γ ` ∆ が証明可能でな

この時, Σ11 関係は全ての Qi が ∃ の論理式で定義ければ明らかに Γ ` ∆ は LK でも証明可能ではない.

可能な関係であり, Π11 は全ての Qi が ∀ の論理式でこれにより LK の証明可能性は CLKIDω に還元でき定義可能な関係である. これをそれぞれ Σ11 の式, Π11

る. LK の証明可能性は Σ01 完全であるため CLKIDω

の式と呼ぶことにする.

ωΣ1n の式は ∃X1 ...∃Xn ϕ で ϕ が Π1n−1 の式であるよの証明可能性は Σ01 困難である.
これより CLKIDω の証明可能性問題が Σ01 に属す

うな式であり, Π1n は ∀X1 ...∀Xn ϕ で ϕ が Σ1n−1 であることを示す. CLKIDω の前証明 P = (D, R) の Dるような式である. Σ1n 関係は Σ1n の式で定義可能なは有限木なので自然数で符号化可能である. また, R関係であり, Π1n 関係は Π1n の式で定義可能な関係では D 中の bud から D の内部ノードへの写像で, 定義ある.

域および値域が有限なので有限関係である. したがって R も自然数で符号化可能である. (D, R) は自然数

7. 1 LKIDω の証明可能性の上界の対で表せるため, これも自然数で符号化可能である.

本節では LKIDω の証明可能性が Π11 関係であるこよって「CLKIDω でシーケント s が証明可能である」
ことは以下の論理式で表現できる.

とを証明する.
まず, 可算な一階の言語のモデルの濃度に関して以∃x(ψP (s, x) ∧ ψG (x))

下が成り立つ.

ここで ψP (s, x) は x が s を根とする CLKIDω の正しい前証明であることを表し, ψG (x) は前証明 x のグ
ラフが大域トレース条件を満たすことを表す述語である. ψP (s, x) が論理式として表現できることは, xが表す有限木が s を根とする正しい前証明となってい補題 3 L をシグネチャΣ を持つ可算な一階の言語とする. M が L のモデルなら, L の可算なモデル M ′ があって, 全ての L の閉式 A に対し M |= A ⇔ M ′ |= Aが成り立つ.

ることが決定可能なことからわかる. また, ψG (x) が証 明 言 語 L の 理 論 T を, 非 論 理 的 公 理 の 集 合論理式として表現できることは [3] より, 前証明 x の{A は L の閉式 | M |= A} として定める. 明らか

グラフが大域トレース条件を満たすかどうかが決定に M |= T である. T は可算なので, Löwenheim-

可能な事よりわかる. よって ψP (s, x) ∧ ψG (x) は決

Skolem 定理から, T は可算モデル M ′ を持つ. この

定可能な二項述語であり, これを φ(s, x) と表すと上とき, 全ての L の閉式 A に対し, M |= A ⇔ M ′ |= Aの式は ∃xφ(s, x) の形になり, これは補題 2 より Σ01を示す. (⇒ の証明) M ′ |= T より従う. (⇐ の証明)□

M 6|= A と仮定すると, M |= ¬A より, ¬A ∈ T . し関係である.

たがって M ′ |= ¬A. したがって M 6|= A が成り立ち,
ω

7 LKID の計算複雑性

対偶により示された.

□

本節では LKIDω の証明可能性判定問題, すなわち

次の定理を, Girard の ω 言語に対する真理値定義

FOLID の標準意味論における妥当性問題が Π11 完全( [8], P. 346, 定理 6.1.4) を FOLID に拡張することでであることを示す.

証明する.

Π11 は解析的階層の一つであり, 解析的階層は N 上の関係を定義する論理式の複雑さによって定められる. ここでは以下の形式の二階論理式を考える.

Q1 X1 ...Qn Xn ϕ

定理 7 LKIDω の標準意味論における妥当性は Π11 関
係である.
証明 シグネチャL = (Σ, Φ) の FOLID のシーケントΓ ` A (Γ は閉論理式の集合, A は閉論理式) を考え

定理 7 と定理 2 より以下が成り立つ.

る. Σ に定数記号 0̂ と単項関数記号 ŝ を追加したもの
を Σ′ とし, L′ = (Σ′ , Φ) とする. 補題 3 より, L′ の定理 8 LKIDω の証明可能性は Π11 関係である.

可算なモデルだけを考えればよい. したがって, L′ の閉項の集合 {t0 , t1 , t2 , ...} に対しモデルのドメインへ

7. 2 LKIDω の Π11 困難性の全射があると仮定してよい (L′ の閉項の集合が可

本節では LKIDω の証明可能性が Π11 困難であるこ算無限であることは導入された記号 0̂, ŝ を用いることにより導かれる). このとき, 関数変数記号 f に対し I(f ) を以下のように定める. ここで P1 , ..., Pn は帰納的述語記号である.

とを示す.
定理 9 LKIDω の証明可能性は Π11 困難である.
このことは Σ11 完全であることが知られている∀B(B ∈ Γ → f (B) = 0)∧Harel の反復ドミノ (recurring dominoes) 問題 [10] が∀B(f (¬B) = 1 − f (B))∧

LKIDω の証明可能性の補問題に還元できることによ∀B∀C(f (B ∧ C) = sup(f (B), F (C)))∧

り示す. なお, ここでは文献 [11] で第四タイル張り問∀B∀C(f (B ∨ C) = inf(f (B), f (C)))∧

題として言い換えられている問題を利用する.

∀B∀C(f (B → C) = inf(1 − f (B), f (C)))∧

LKIDω の証明可能性の補問題は以下のようになる.

∀B(f (∀xB(x)) = sup{f (B(ti )); i ∈ N})∧` φ が証明可能でない∀B(f (∃xB(x)) = inf{f (B(ti )); i ∈ N})∧

⇔ 6|= φ（LKIDω の完全性より）∀t(f (t = t) = 0)∧⇔¬φ は標準意味論で充足可能∀i∀j∀x∀B(f (ti = tj ∧ B[x := ti ] → B[x := tj ]) = 0)∧ ここではシーケントの前件は空集合であり, また後件^
∀t(f (Pi (t)) = inf{f (Pei (t, k)); k ∈ N})
はただ一つの式 φ であるが一般性は失わないことにi∈{1,...,n}

ここで, Pei は以下のように定義される述語である. Φiは Φ 中で Pi を結論に持つ生成規則の集合である.

Pei (x, 0) = false_
Pei (x, k + 1) =な FOLID の式 ¬φ を構成することが目標となる. こ

Fr (Pi , k)

こで, 第四タイル張り問題とは次のような問題である.

1≤r≤|Φi |

Pj1 (t1 )Pi (t)...

以上より, 第四タイル張り問題の解が存在するとき,かつそのときに限り標準意味論で充足可能となるよう

ここで Fr (Pi , k) は, Φi 中の r 番目の生成規則が以下の形であるとき,Q1 (u1 ) ... Qh (uh )注意してほしい.

C を色の有限集合とする. タイルは正方形で東西南北の各辺には C 中の色が塗られている. タイルの種

Pjm (tm )類は有限で, それを A とする. これらのタイルを東方F (Pi , k) = ∃y(x = t(y)∧Q1 u1 (y)∧· · ·∧Qh uh (y)∧ggP
j1 (t1 (y), k) ∧ · · · ∧ Pjm (tm (y), k)) で定義される.

向と北方向に無限に伸びる N × N のグリッドに並べ

Pei は k に関する帰納法により定義されているが, こき, 隣り合うタイルの色はその重なり合う辺が同じ色

れは算術論理式で記述可能である. このとき, シーケ

でなければならない. 各種類のタイルは何枚でも使用

ント Γ ` A が L′ のすべての可算標準モデルで真であできるが, タイルを回転させることはできない. このることは, ∀f (I(f ) → f (A) = 0) と表せる. これは論時, 南の境界と西の境界は全て特定の色, 例えば青色理式および変数記号を適切に符号化した場合 Π11 の式

で, さらに特定の色, 例えば赤色がタイル張り中に無である. このとき, Γ, A は L の式 (集合) であるため,

限にしばしば出現するようにタイルを並べることがΓ ` A は L のすべての可算標準モデルにおいても真可能かどうかを判定する問題が第四タイル張り問題である. 以上は閉論理式のみの議論であったが, 自由である.

変数を含む論理式においても同様に成り立つ.

□ていく. 各セルには一枚のタイルのみを置くことがで

定理 9 の証明 シグネチャΣ を三項関係記号 North,

いる.

South, East, West, 二項関係記号 ≥, 単項関係記

ψred ⇔ ∀x∃y∃z(z ≥ x ∧ (Red(y, z) ∨ Red(z, y)))号 N , 単項関数記号 s, 定数記号 0, r, b, y, g, k, ...(r 以

最後に φN を以下のように定義する.

降は色に対応) から成るものとする. North(x, y, c)

φN ⇔∀x(sx 6= 0)∧

def

def

∀x∀y(sx = sy → x = y)

はグリッド上の位置 (x, y) のセル上のタイルの北側の色が c であることを表している. また, N と ≥ は補次の主張をこれより示す.

φtile ∧ φN ∧ ψred が充足可能のとき, かつその題 1 の生成規則 ΦN により定義される帰納的述語で主張ある. 色の有限集合を C, タイルの種類の有限集合をときに限り 色の有限集合を C, タイルの種類を T とT とする. 各タイル種類 A ∈ T に対し, 「グリッド位する第四タイル張り問題の解が存在する.

置 (x, y) にあるタイルの種類は A である」という述語を TileA (x, y) と書く. 例えばタイル種類 A は北(⇒ の証明) ある構造 A に対し A |= φtile ∧φN ∧ψredであるとする. A |= φN と補題 1 より, (N A , ≥A ) ∼=が青色 (b), 東が赤色 (r), 南が黒色 (k), 西が緑色 (g)(N, ≥N ) である. したがって, N A をグリッドの一つのである場合, その事実は次のように表現できる.
^
def¬North(x, y, c)
TileA (x, y) ⇔North(x, y, b) ∧き, グリッド位置 (x, y) ∈ N A × N A に種類 A のタイ

c∈C
c̸=b

∧South(x, y, k) ∧^ルを置くことにすると, A |= φtile よりこれは正しいタ¬South(x, y, c)

c∈C
c̸=k

^

∧East(x, y, r) ∧¬East(x, y, c)

c∈C
c̸=r

∧West(x, y, g) ∧^次に φtile を次のように定義する. これは「グリッ
ド上のタイルが正しくタイル張りされている」ことを意味する. 特に, 最初の節によりタイルの置かれている位置は N を真とする点のみであることが強制され
def

φtile ⇔∀x∀y(N x ∧ N y ↔

_イル張りとなっており, x ∈/ N A, y ∈/ N A なる (x, y)に対してはどの種類 A に対しても TileA (x, y) は真ではない. このようなタイル張りにおいては A |= ψredより, 赤色を持つタイルがグリッド上に無限にしばし¬West(x, y, c)

c∈C
c̸=g

ていることに注意されたい.

軸に対応させることができる. A |= TileA (x, y) のと

TileA (x, y))∧A∈T

ば現れる. したがって, N × N のグリッド上で色の有限集合を C, タイルの種類を T とする第四タイル張り問題の解となるタイル張りが得られる.

(⇐ の証明) 第四タイル張り問題の解が存在するとき,
A |= φtile ∧ φN ∧ ψred となるモデル A を構成して見せればよい. A の台を N とし, N A = N, sA : x 7→ x + 1,

≥A を ≥N と解釈する. North, South, East, Westの解釈はタイル張りの通りに与える. このモデル A∀xSouth(x, 0, b)∧が φtile ∧ φN ∧ ψred を満たすことは明らかである. □∀yWest(0, y, b)∧^∀x∀y((East(x, y, c) → West(sx, y, c)))∧定理 8 と 9 より以下の系が導かれる.

^

c∈C

∀x∀y(

(North(x, y, c) → South(x, sy, c)))c∈C

系 2 LKIDω の証明可能性は Π11 完全である.

Red(x, y) を以下のように定義する. これは「グリッド位置 (x, y) のタイルが赤色を含む」という意味
である.

8 考察

Red(x, y) ⇔North(x, y, r) ∨ South(x, y, r)

5 節より, LKID の証明可能性の計算複雑性は Σ01∨ East(x, y, r) ∨ West(x, y, r)

完全であり, さらに定理 6 より CLKIDω の証明可能

def

更に ψred を以下のように定義する. これは「無限性の計算複雑性も同じく Σ01 完全であることが分かっにしばしば赤色のタイルが現れる」ことを意味してた. したがっていずれも証明探索問題は計算可能であるため自動推論に適した推論体系であることが分かる.
ま た, Beraridi と Tatsuta は 証 明 能 力 に お い て

LKID よりも CLKIDω のほうが真に強力であることを明らかにした [1](本稿の定理 3). しかしいずれも Σ01
完全であることより, CLKIDω で証明可能な式の集合
から LKID で証明可能な式の集合への多対一還元 σが存在する. そのような還元を利用すれば CLKIDω
では証明可能だが LKID では証明不可能である式 H（例えば [1] の 2-Hydra 言明）でも, LKID で証明可能な式 σ(H) が存在する. 逆に, LKID で証明可能な式の集合から CLKIDω で証明可能な式の集合への多対一還元も存在するが, そのような還元は恒等写像ではないこともわかる (上記のような式 H は CLKIDω において証明不可能な式に移されなければならないた
め).

9 まとめ
本稿では帰納的述語に関する推論体系である LKID,

CLKIDω , LKIDω の証明可能性の計算複雑性について考察し, LKID と CLKIDω の証明複雑性は Σ01 完
全, LKIDω の証明複雑性は Π11 完全であることを明らかにした. 本研究の成果により, LKID および

CLKIDω は (通常のチューリング機械で) 計算可能であることが分かったため, 推論の (半) 自動化が理論上は可能であることが明らかになった. 一方, LKIDω
の推論は計算機上で行うことが困難であることも明らかになった.
今後の方向性としては, シグネチャを限定したときにそれぞれの証明体系の計算複雑性がどのように変化するかを調査することが考えられる. また, CLKIDω
は Cut 規則を除去することが不可能であることが示されているが [16], 使用する論理式の数を制限することで Cut 除去可能かどうかを検討することも考えられる.
謝辞 この研究は JSPS 科研費 JP21K11756 と２０
２２年度国立情報学研究所公募型共同研究（22FP02）の助成を受けています. また, 中澤 巧爾 名古屋大学
准教授に, ご助言を感謝します.

参 考 文 献[ 1 ] Berardi, S. and Tatsuta, M.: Classical System
of Martin-Löf’s Inductive Deﬁnitions Is Not Equivalent to Cyclic Proof System, Foundations of Software Science and Computation Structures - 20th
International Conference, FOSSACS 2017, Held as
Part of the European Joint Conferences on Theory
and Practice of Software, ETAPS 2017, Uppsala,Sweden, April 22-29, 2017, Proceedings, Esparza, J.
and Murawski, A. S.(eds.), Lecture Notes in Computer Science, Vol. 10203, 2017, pp. 301–317.
[ 2 ] Berardi, S. and Tatsuta, M.: Equivalence of inductive deﬁnitions and cyclic proofs under arithmetic, 32nd Annual ACM/IEEE Symposium on
Logic in Computer Science, LICS 2017, Reykjavik,
Iceland, June 20-23, 2017, IEEE Computer Society,2017, pp. 1–12.
[ 3 ] Brotherston, J.: Sequent Calculus Proof Systems
for Inductive Deﬁnitions, PhD Thesis, University of
Edinburgh, 2006.
[ 4 ] Brotherston, J. and Simpson, A.: Sequent calculi for induction and inﬁnite descent, J. Log. Comput., Vol. 21(2011), pp. 1177–1216.
[ 5 ] Brotherston, J., Bornat, R., and Calcagno,
C.: Cyclic proofs of program termination in separation logic, ACM SIGPLAN Notices, Vol. 43,
No. 1(2008), pp. 101–112.
[ 6 ] Cintioli, P. and Tulipani, S.: Σ11 -Completenessof a Fragment of the Theory of Trees with Subtree Relation, Notre Dame Journal of Formal Logic,
Vol. 35, No. 3(1994), pp. 426–432.
[ 7 ] Das, A.: On the logical complexity of cyclic
arithmetic, Logical Methods in Computer Science,Vol. 16, No. 1(2020).
[ 8 ] Girard, J.-Y.: Proof theory and logical complexity. Volume I., Bibliopolis, 1987.
[ 9 ] Halpern, J. Y.: Presburger Arithmetic with
Unary Predicates is Π11 complete, The Journal of
Symbolic Logic, Vol. 56, No. 2(1991), pp. 637–642.
[10] Harel, D.: Recurring dominoes: Making thehighly undecidable highly understandable., Annals
of Discrete Mathematics, Vol. 24(1985), pp. 51–72.
[11] Harel, D., Kozen, D., and Tiuryn, J.: Dynamic
Logic, MIT Press, 2000.
[12] Iosif, R., Rogalewicz, A., and Simácek, J.: The
Tree Width of Separation Logic with Recursive Definitions, Automated Deduction - CADE-24 - 24th
International Conference on Automated Deduction,
Lake Placid, NY, USA, June 9-14, 2013. Proceedings, Bonacina, M. P.(ed.), Lecture Notes in Computer Science, Vol. 7898, Springer, 2013, pp. 21–38.
[13] Keisler, H. J.: Model Theory for Inﬁnitary
Logic, North-Holland, 1974.
[14] Marongiu, G. and Tulipani, S.: Undecidable
fragments of term algebras with subterm relation,
Fundamenta Informaticae, Vol. 19(1993), pp. 371–
382.
[15] Martin-Löf, P.: Haupstatz for the intuitionis-

tic theory of iterated inductive deﬁnitions, Proc.
the Second Scandinavian Logic Symposium, NorthHolland, 1971, pp. 179–216.
[16] Masuoka, Y. and Tatsuta, M.: Counterexample to cut-elimination in cyclic proof systemfor ﬁrst-order logic with inductive deﬁnitions,
arXiv:2106.11798, 2021.
[17] Simpson, A.: Cyclic Arithmetic Is Equivalent
to Peano Arithmetic, Proc. FoSSacS2017, Springer
Berlin Heidelberg, 2017, pp. 283–300.
[18] Speranski, S. O.: A note on deﬁnability infragments of arithmetic with free unary predicates,
Archive for Mathematical Logic, Vol. 52(2013),

pp. 507–516.
[19] Ta, Q., Le, T. C., Khoo, S., and Chin, W.:
Automated lemma synthesis in symbolic-heap separation logic, Proc. ACM Program. Lang., Vol. 2,
No. POPL(2018), pp. 9:1–9:29.
[20] Tatsuta, M., Nakazawa, K., and Kimura, D.:
Completeness of Cyclic Proofs for Symbolic Heaps
with Inductive Deﬁnitions, Programming Languages
and Systems - 17th Asian Symposium, APLAS
2019, Nusa Dua, Bali, Indonesia, December 1-4,
2019, Proceedings, Lin, A. W.(ed.), Lecture Notes
in Computer Science, Vol. 11893, Springer, 2019,
pp. 367–387.