【Dedukti入門 ①】Lean 4・Rocq・Isabelle が検証した証明を、もう一度、別の証明検査器で検査する ── 翻訳器と符号化ファイルの仕組み

本記事について

本記事は、Dedukti という言語を扱う連載の初回です。

全体で何回になるかは、いまのところ決めていません。
３回以上にはなる見込みです。

初回である本記事だけで、ひとつの話が完結します。

次回以降を読まなくても、Dedukti が何をするものかは分かるように書きました。

想定する読者。

プログラムを書いた経験がある方を想定しています。

型理論 や 数理論理学 の知識は、前提にしません 。

本記事中の専門用語は、初出時にわかりやすく解説するように心がけました。
また、記事末尾にも用語のミニ解説を置きました。

なお、入門者向けの分かりやすい解説を優先する執筆方針をとりましたので、中上級者や専門家の方からご覧になると、厳密な議論を欠いている点や、議論を単純化している点など、精密な定義をするようご指導をいただいてしまう点もあろうかとは思いますが、分かりやすさを優先した故の簡便的な説明や定義付けであることをご寛恕頂けますと幸いです。

本記事に出てくるコードについて。

Dedukti のコード と Lean 4 のコードが出てきます。

いずれも筆者の環境で実際に実行し、結果を確かめたものです。
実行環境と手順は、記事末尾の「実機検証について」にまとめました。

本記事の流れ

問い

この記事は、ひとつの問いをめぐる物語 です。

その 問い とは、次のようなものです。

AI（LLM/ Ai Agent）が数学の定理の証明を書き、定理証明器がそれを検査（検証）する時代が到来したいま、その定理証明器を、誰が検査するのか？

この問いに対するひとつの可能な答えは、数学定理の証明が正しいかどうかを検査（検証）した定理証明器とは独立した、別の検証器（機械）を使って、その証明が本当に正しい（定理として成立する）のかどうかをダブルチェックする、というものです。

ここで 課題となる のは、2026年９月時点で、よく使われる定理証明器は一つだけでなく、複数あること です。

代表的な名前を挙げてみただけでも、Rocq（旧 Coq） 、Lean 4 、Isabelle 、Agda 、HOL Lightなど があります。

ある状況において、ダブルチェックすべき数学定理の証明の正しさを、最初に検証した定理証明器がどの定理証明言語（定理証明支援系）であるのかは、事前に予想することは困難 です。

ここで、この記事が 光を当てる のは、ある数学定理の証明が成立するのか、しないのかを検証した定理証明支援系が、Rocq（旧 Coq）、Lean 4、Isabelle、Agda、HOL Light 等の いずれであったとしても、その証明検証の正しさをダブルチェックすることができる言語が実在すること です。

その言語の名前は、Dedukti です。

Dedukti を 利用する場面 は、Rocq（旧 Coq）、Lean 4、Isabelle 等が、ある数学定理についての証明の検証を完了した状況からスタートします。

ところで、この状況で、それぞれの定理証明支援系の手元に何が残っているかは、定理証明支援系によって違います。

Rocq、Lean 4、Agda は、「証明項」と呼ばれるデータ
（証明の全手順を、ひとつの式として書き表したもの。定理証明支援系の利用者が書くのは「まず帰納法を使え、次に両辺を展開せよ」といった指示ですが、**処理系はその指示を実行した結果を、関数と関数適用だけからなる式に落とします。**この式が 「証明項」 です。詳しくは、この記事で後述します）を、コンパイル結果のファイルの中に保存します。

• Rocq なら .vo ファイル
• Lean 4 なら .olean ファイル
• Agda なら .agdai ファイル

の中に、です。

ところが、Isabelle と HOL Light は事情が異なります。

Isabelle と HOL Lightは、（何らかの数学定理等の）証明が成立しているかどうかの検査（検証）が終わると、「証明項」をファイルの中などに保存せずに、捨ててしまうのです。

データとして残されるのは、「この定理は証明された」という記録だけです。

但し、証明項を記録させる設定を有効にした場合は、Isabelle と HOL Lightであっても、「証明項」がデータとして保存されます。

前置きが長くなりましたが、Dedukti が （間接的に）利用するのは、この「証明項」 です。

Rocq（旧 Coq）、Lean 4、Agda、Isabelle等の定理証明支援系が、ある数学定理の証明が成立しているか、していないかの検査を終えたときにファイルに保存される 「証明項」を受け取って、それを Dedukti が理解可能な形式に翻訳するソフトウェア が、定理証明支援系それぞれに対応する形で 作成・公開されています。

Dedukti は、このような「翻訳」ソフトウェアが、（Deduktiのために）翻訳してくれたファイルを受け取り、そのファイルに書かれていることが、成立するのか、しないのかを検査（ダブルチェック）するものです。

先ほど、Dedukti は、「証明項」を「間接的に」利用すると表現したのは、証明項とDeduktiの間に、こうした翻訳ソフトウェアが介在しているからです。

ところで、Rocq（旧 Coq）、Lean 4、Agda、Isabelle等の定理証明支援系は、それぞれ異なる論理体系と型理論に立脚するものであるにもかかわらず 、各言語が定理証明の検証を終えたときにファイルに出力される「証明項」は、（それぞれの定理証明支援言語ごとに用意された翻訳器によって、）どのようにして、ひとつの「Deduktiが理解可能な形式」へと翻訳することが可能なのでしょうか？

まず、翻訳先の形式を確認します。

Dedukti が読み込むのは、拡張子が .dk のテキストファイルです。以降、.dk ファイルと呼びます。

この「.dk ファイル」に 記述できるものは、たった2種類しかありません 。

• 識別子の宣言
• 書き換え規則

の ２種類 です。

識別子の宣言

識別子の宣言 は、imp : prop -> prop -> prop. のように書きます。
imp という識別子を、prop を 2 つ受け取って prop を返すものとして使う、という意味です。

ここで prop は、命題の全体を表す識別子です。
「2 は素数である」も「1 + 1 = 2」も、prop に属します。
prop 自身も、prop : Type. という 1 行で、あらかじめ宣言しておきます。

Type は、Dedukti が最初から持っている識別子です。
A : Type. と書くと、A は型である、という意味になります。

したがって prop : Type. は、prop という型を新しく作る宣言です。
imp は、命題 a と命題 b から、「a ならば b」という新しい命題を作る識別子です。

書き換え規則

書き換え規則 は、[a, b] Prf (imp a b) --> Prf a -> Prf b. のように書きます。左辺の式が現れたら、右辺の式に置き換えてよい、という意味です。

ここで Prf は、命題を受け取って「その命題の証明の型」を返す識別子です。
Prf : prop -> Type. と宣言しておきます。

したがってこの規則は、「a ならば b」の証明の型は、「a の証明を受け取って b の証明を返す関数」の型に置き換えてよい、と述べています。

鍵を握るのは、符号化（encoding）と呼ばれる仕掛けです。

符号化 とは、ある論理体系や型理論を、識別子の宣言と書き換え規則の組に置き換える、固定的な置き換え規則 です。

翻訳器 は、自分が担当する定理証明支援系が立脚する 論理体系と型理論 を、Dedukti が理解可能な「識別子の宣言と書き換え規則の組」に置き換える ための 固定ルール を持っています。

この 固定ルール は、翻訳器のソースコードに同梱された .dk ファイルに記述されています。 本記事では、符号化ファイル と呼ぶことにします。

例えば、定理証明言語Lean（Lean, Lean 2, Lean 3, Lean 4）の翻訳を受け持つlean2dk の場合、リポジトリの dk/enc/ というフォルダに、enc.dk、lvl.dk など 7 本の符号化ファイルが置かれています。

7 本の符号化ファイルの中に、Lean 4 の型理論 CIC の記号にあたる識別子の宣言と、CIC の計算の規則にあたる書き換え規則が記述されています。

符号化ファイル 7 本の中身は、リポジトリに置かれたまま書き換わりません。翻訳のたびに作られるものではありません。本記事の実機検証でも、lean2dk を実行する前と後で、7 本の中身は同じでした。

翻訳器は、この 符号化の固定ルールを適用する ことで、担当する定理証明支援系がファイルに出力した 証明項 を、符号化ファイルで宣言された識別子だけを使った式に書き直し、新しい .dk ファイルへ出力 します。

本記事では、この局面で登場する「.dkファイル」のことを、証明ファイルと呼ぶことにします。

ここまでを振り返ってみると、 「符号化ファイル」 と **「証明ファイル」**は、どちらも拡張子が .dk です。

同じ拡張子のファイルですが、中身の役割が違います。

符号化ファイル には、識別子の宣言と書き換え規則 が記述されています。
他方で、証明ファイル には、翻訳された証明項 が記載されています。

符号化ファイルは翻訳器にあらかじめ同梱されており、証明ファイルは翻訳のたびに新しく作られるのです 。

それでは、翻訳前の証明項と、翻訳後の証明項は、何が違うのでしょうか？

実物で比較してみましょう。

以下は、Lean 4 のコードである定義を記述したものです。

MyTrue という 命題 を作り、「MyTrue ならば MyTrue」を 証明 しています。

def test : MyTrue → MyTrue := fun x : MyTrue => x

Lean 4 は、この定義を 検証 し、証明項 を .olean ファイルに保存 します。

証明項 の中身は、Lean 4 の型理論 CIC の記号 ── Sort、Pi、El など ── で書かれています。 Dedukti は、CIC の記号を理解できません。

証明項の中身 を見てみます。
以下は、.olean に保存された test の型と値を、Lean 4 の内部表現のまま出力したものです。

    型
    Lean.Expr.forallE
      (Lean 4 が内部で生成した変数名)
      (Lean.Expr.const `MyTrue [])
      (Lean.Expr.const `MyTrue [])
      (Lean.BinderInfo.default)

    値
    Lean.Expr.lam `x
      (Lean.Expr.const `MyTrue [])
      (Lean.Expr.bvar 0)
      (Lean.BinderInfo.default)

forallE が依存関数型、lam がラムダ抽象、const が定数の参照、bvar が束縛変数です。

値のほうを読むと、「x という名前で MyTrue を受け取り、0 番目の束縛変数をそのまま返す関数」となります。恒等関数です。

次に、翻訳器 lean2dk が出力した証明ファイル の中身を見てみます。

以下の通りです。

def test :
  enc.El lvl.z
    (enc.Pi lvl.z lvl.z AuxLvls.l7
       MyTrue
       (x0 : enc.El lvl.z MyTrue => MyTrue)).

[] test --> x0 : enc.El lvl.z MyTrue => x0.

書かれている内容は同じです。
どちらも、「MyTrue を受け取って MyTrue を返す関数」です。

両者で異なるのは、使用されている識別子です。

Lean 4 の forallE が enc.Pi に、lam が Dedukti の => に、bvar 0 が x0 という名前の変数に置き換わっています。

enc.Pi も enc.El も lvl.z も、符号化ファイルの中で宣言されている識別子 です。

Lean 4 が出力した証明項	lean2dk が出力した証明項（翻訳結果）
Lean.Expr.forallE（依存関数型）	enc.Pi
Lean.Expr.lam（ラムダ抽象）	=>
Lean.Expr.bvar 0（0 番目の束縛変数）	x0（名前を付けた変数）
Lean.Expr.const \MyTrue []`（定数 MyTrue の参照）	MyTrue
[]（宇宙のレベルの空リスト）	lvl.z（レベル 0）
対応するものなし	enc.El（型を表すデータから、型を取り出す）
対応するものなし	AuxLvls.l7（レベルの計算のための補助の識別子）

enc.Pi、enc.El、lvl.z は、いずれも符号化ファイルの中で宣言されている識別子です。

表の下2行について補足します。

enc.El は、lean2dk の符号化の都合で入っています* 。

lean2dk の符号化では、Lean 4 の型を、Dedukti の側ではまずデータとして表します。
enc.Pi ... が、そのデータにあたります。

そのデータが表す型を取り出すために、enc.El を被せます。

AuxLvls.l7 は、lean2dk がレベルの計算のために生成した補助の識別子です。

つまり、翻訳とは、証明項の構造をそのまま保ったまま、使っている識別子を符号化ファイルで宣言したものに差し替える作業 です。

証明の内容は変わりません 。

Dedukti は、証明ファイルと符号化ファイルをあわせて受け取り、そこに綴られている証明が正しいかどうかをダブルチェックする のです。

ここまで、Lean 4 が、ある数学定理の証明の検証を終えたときにファイルに出力する 証明項 と、その証明項を lean2dk が （Dedukti が理解できる）「新しい証明項」に翻訳した結果 を比較しながら見ていただきました。

Lean 4 を例にとりましたが、Rocq 、Isabelle 、その他の定理証明支援系 が出力した証明項も、同様に、各言語を担当する専門の翻訳器によって、Dedukti が理解可能な（つまり、ダブルチェック可能な）「新しい証明項」に翻訳することができます。

参考までに、Lean 4 以外の定理証明支援系について、各言語の内部表現と、専用の翻訳器が使う符号化の識別子との対応を、lean2dk の場合と同様に掲げます。

以下の表は、各翻訳器のリポジトリに置かれた符号化ファイルの中身を、筆者が読んで作成したものです。翻訳器を実際に動かして得た出力ではありません（lean2dk の表だけは、筆者の環境で実行した結果です）。

Rocq（旧 Coq）── 翻訳器 CoqInE

符号化ファイルは、リポジトリの encodings/interfaces/original.dk などです。

Rocq の内部表現	CoqInE の符号化の識別子
宇宙（Prop、Set、Type_i）	Sort
型を表すデータ	Univ s
データが表す型	Term s a
依存関数型（Prod）	prod s1 s2 a b
宇宙の後続（Type_i の 1 つ上）	axiom
依存関数型の宇宙を決める規則	rule
累積性による型の持ち上げ	lift

HOL Light ── 翻訳器 hol2dk

符号化ファイルは、リポジトリの theory_hol.dk です。

HOL Light の内部表現	hol2dk の符号化の識別子
単純型の全体	Set
型を表すデータから、型を取り出す	El
真理値型 bool	bool
関数型	fun a b
命題の証明の型	Prf
等式	eq
カーネルの推論規則 REFL	REFL
カーネルの推論規則 TRANS	TRANS
カーネルの推論規則 MK_COMB	MK_COMB
カーネルの推論規則 EQ_MP	EQ_MP
関数の外延性	fun_ext
命題の外延性	prop_ext

HOL Light の 符号化 には、含意と全称量化について次の書き換え規則 が置かれています。

Lean 4 の符号化とは 対象が違いますが、識別子の宣言と書き換え規則の組である点は同じ です。

    [p,q] Prf (imp p q) --> Prf p -> Prf q.
    [a,p] Prf (all a p) --> x : El a -> Prf (p x).

Agda ── 翻訳器 Agda2Dedukti

符号化ファイルは、リポジトリの theory/dk/eta/Agda.dk などです。

Agda の内部表現	Agda2Dedukti の符号化の識別子
宇宙（Set、Prop、Setω、SizeUniv）	Sort、set、prop、sortOmega、sizeUniv
型を表すデータ	Univ s
データが表す型	Term s a
依存関数型（Pi）	prod s1 s2 A B
宇宙の後続	axiom
依存関数型の宇宙を決める規則	rule
η 展開	etaExpand

3つの表を見比べると、共通点が見えます。

どの符号化にも、「型を表すデータ」と「そのデータが表す型」を分ける識別子があります。

• CoqInE と Agda2Dedukti では Univ と Term
• hol2dk では Set と El
• lean2dk では enc.Sort と enc.El

です。
名前は違いますが、役割は同じ です。

違いは、それぞれの定理証明支援系が立脚する論理体系と型理論の違いに対応します。

• Rocq と Agda には 宇宙の階層 があるので、axiom と rule が要ります。
• HOL Light には 宇宙の階層がない ので、Set 1 つで足ります。
• Agda には $η$ 変換がある ので、etaExpand が要ります。

このように、定理証明支援系ごとの違いは、翻訳器が持つ符号化ファイルの中身として吸収されます。

翻訳した先の形式は、どの定理証明支援系についても同じ .dk ファイルです 。

Dedukti が行うことも、どの場合も同じです。
証明ファイルと符号化ファイルを受け取り、型検査するだけ です。

Isabelle ── 翻訳器 isabelle_dedukti

符号化ファイルは、リポジトリの STTfa.dk です。

STTfa は Simple Type Theory with functional arrows の略で、Isabelle/HOL の土台にあたる単純型理論を指します。

Isabelle の内部表現	isabelle_dedukti の符号化の識別子
単純型の全体	Set
型を表すデータから、型を取り出す	El
関数型	arr a b
命題型 prop	prop
含意	imp
全称量化	all
命題の証明の型	Prf

STTfa.dk は全体で 13 行です。
書き換え規則は3本しかありません。

    [a, b] El (arr a b) --> El a -> El b.
    [a, b] Prf (imp a b) --> Prf a -> Prf b.
    [a, b] Prf (all a b) --> x:El a -> Prf (b x).

2 本目は、本記事の前半でお見せした 含意の書き換え規則 と 同じ形 です。

Isabelle/HOL の土台が 単純型理論 であり、宇宙の階層や帰納型の計算規則を持たない ため、符号化がこれだけの分量で済んでいます。

Rocq や Agda や Lean 4 の符号化が数百行に及ぶのとは対照的です。

Dedukti は、各定理証明支援系について掲げた表の右側の列 ── 専用の翻訳器が翻訳し、生成した「新しい証明項」に登場する識別子 ── を、すべて理解できます。

なぜ、Rocq 用の Univ も、HOL Light 用の Set も、Isabelle 用の arr も、Lean 4 用の enc.Pi も、Dedukti は等しく理解できるのでしょうか？

理由は2つ あります。

（理由 1） 識別子の宣言が、証明ファイルと一緒に Dedukti へ渡されるからです。

Dedukti は、Univ も Set も arr も enc.Pi も、あらかじめ知っているわけではありません。
Dedukti が最初から持っている識別子は Type だけです。

しかし、翻訳器は、証明ファイルを生成するとき、符号化ファイルも一緒に Dedukti に渡します。

符号化ファイルには、その翻訳器が使う識別子の宣言と書き換え規則が、すべて書かれています。Dedukti は、符号化ファイルを先に読み込み、そこで宣言された識別子を、その場で使えるようにするのです。

つまり、Dedukti は識別子を知っているのではなく、その都度教えられているのです。

Rocq の証明を検査するときは CoqInE の符号化ファイル を、
Isabelle の証明を検査するときは isabelle_dedukti の符号化ファイル

を読み込みます。

読み込む符号化ファイルが変われば、扱える識別子も変わります。

理由 2。どの翻訳器も、識別子の宣言と書き換え規則の 2 種類しか使わないからです。

理由 1 は、Dedukti が識別子を知る経路を述べたものです。
しかし、経路があるだけでは足りません。

たとえば、ある翻訳器が「識別子の宣言」と「書き換え規則」だけを使い、別の翻訳器が、それに加えて「関数を再帰的に定義する構文」や「型のクラスを宣言する構文」を使ったとします。

この場合、Dedukti は後者の翻訳器のために、新しい構文を読み取る機能を足す必要があります。翻訳器が増えるたびに、Dedukti の側も作り替えることになります。

そうならないのは、Dedukti の言語 λΠ計算 modulo rewriting で書けるものが、識別子の宣言と書き換え規則の 2 種類しかないから です。

翻訳器の設計者は、この 2 種類の範囲内で符号化を設計 します。

CoqInE の符号化も、hol2dk の符号化も、
isabelle_dedukti の符号化も、
Agda2Dedukti の符号化も、
lean2dk の符号化も、

すべてこの2種類だけでできています。

上に掲げた4つの表の右側の列に並ぶ識別子は、例外なく、どこかの符号化ファイルで宣言されたものです。

Dedukti が行う処理は、どの符号化ファイルを読み込んだ場合も同じです。

宣言された識別子の型を照合し、書き換え規則を適用しながら、証明項の型を検査します 。

Rocq 用の符号化を読み込んだからといって、Dedukti が Rocq 専用の動作をするわけではありません。
翻訳器が新しく増えても、Dedukti の側は変わらない のです。

そして、ある定理証明支援系が行った証明検査を、別の証明検査器 ── つまり Dedukti ── によって再検査できることは、この記事の冒頭で述べた問いへの、ひとつの答え になります。

AI（LLM / AI Agent）が研究レベルの数学定理の証明を書き、Lean 4 などの定理証明支援系がその証明を検査する。

この構図では、立案された証明が成立するのか、しないのかという判定の確からしさ（信頼性）のすべてが、Lean 4などの定理証明支援系がもつ「信頼度」に依存する形になります。

万が一、Lean 4のソースコードに瑕疵（バグなどの誤り）が潜んでいた場合、すべての信頼性が失われる結果となってしまいます。その定理証明支援系の実装に誤りがあれば、誤った証明が通ってしまうからです。

Dedukti は、その判定に second opinion を与えます。

Lean 4 が受理した証明項を、lean2dk が翻訳し、Dedukti が独立に型検査する。

Lean 4 と Dedukti は別のプログラムであり、実装を共有していません。
両方が受理したのであれば、Lean 4 の実装の誤りだけで誤った証明が通る、という筋道は塞がれます。

ここまでのまとめ

初回記事では、次の 4 点を述べました。

1 点目。AI が数学の証明を書き、定理証明支援系がその証明を検査する時代に、その定理証明支援系を誰が検査するのか、という問いがあります。

2 点目。Rocq、Lean 4、Agda、Isabelle などの定理証明支援系は、証明の検証を終えたとき、証明項を保存しています。ただし、保存のされ方は定理証明支援系によって違います。

3 点目。定理証明支援系ごとに専用の翻訳器があり、翻訳器は符号化ファイルという固定ルールを持っています。翻訳器は、符号化ファイルで宣言された識別子だけを使って、証明項を .dk ファイルに書き直します。

4 点目。Dedukti は、証明ファイルと符号化ファイルをあわせて読み込み、証明項を型検査します。Dedukti が論理体系をひとつも内蔵していないからこそ、複数の定理証明支援系を対象にできます。

次回記事へ

初回記事では、Dedukti が何をするものかを述べました。次回記事では、Dedukti の中身に踏み込みます。

次回以降の記事で扱うのは、次の 5 点です。

Dedukti の言語そのもの。
λΠ計算 modulo rewriting とは何か。
依存型と書き換え規則という 2 つの部品で、なぜ複数の論理体系を記述できるのか。実物のコードで示します。

Logical Framework という考え方。

Logical Framework とは、複数の論理体系の推論規則を記述するための言語のことです。初回記事で見た符号化は、この考え方の実例にあたります。

この考え方は、1987 年に Harper、Honsell、Plotkin が提案した Edinburgh LF に始まります。

Edinburgh LF が取った方針は、次のとおりです。

Edinburgh LF の言語には、一階述語論理の推論規則も、高階論理の推論規則も、入っていません。この言語が与えるのは、推論規則を記述するための道具立てだけです。

推論規則そのものは、Edinburgh LF の言語で書いたファイルに記述します。一階述語論理を使いたいなら、一階述語論理の推論規則を記述したファイルを用意します。高階論理を使いたいなら、高階論理の推論規則を記述したファイルを用意します。

一階述語論理の推論規則を記述したファイルを読み込んで、そのファイルの上で書かれた証明を検査するプログラムが、別に作られます。実装のひとつが、後述する Twelf です。Twelf には、どの論理体系の推論規則も組み込まれていません。Twelf は、読み込んだファイルに記述された推論規則にしたがって、証明を検査します。

この方針の利点は、証明を検査するプログラムを 1 つ作れば、どの論理体系にも使えることです。一階述語論理を記述したファイルを読み込ませれば一階述語論理の証明を検査でき、様相論理を記述したファイルを読み込ませれば様相論理の証明を検査できます。プログラムの側は、どちらの場合も同じです。論文は、この利点を「論理に依存しない証明エディタや証明検査器を構築できる」と述べています。

Edinburgh LF が導入した原理が、judgments as types です。「A は成り立つ」といった判断を、メタ言語の型として表します。この原理により、証明の検査が型検査に還元されます。初回記事で見た Prf : prop -> Type. という宣言は、この原理を Dedukti の上で実現したものです。

Edinburgh LF の用途は、次のとおりです。

まず、論理体系をひとつ定義します。一階述語論理を使いたいなら、一階述語論理の推論規則を記述したファイルを用意します。次に、その定義の上で証明を書きます。そして、書いた証明が正しいかを、型検査によって確かめます。

証明の対象は 2 通りあります。それぞれ、証明を検査する目的も違います。

**1 つ目の対象は、一階述語論理や高階論理といった論理体系の中の定理です。**一階述語論理の推論規則を記述したファイルを用意したなら、その一階述語論理の上で「A かつ B ならば B かつ A」といった定理を証明します。

この場合に知りたいのは、その定理が、一階述語論理や高階論理といった論理体系の推論規則だけから導けるかどうかです。導けるなら証明は型検査を通り、導けないなら型検査は失敗します。たとえば直観主義論理の推論規則を記述したファイルの上で二重否定除去を証明しようとすると、型検査は失敗します。直観主義論理の推論規則からは導けないからです。

この場合の目的は、その定理を導くために、どの推論規則が必要かということであり、一階述語論理や高階論理といった論理体系そのものの性質を深く研究することです。

一方、古典論理の推論規則を記述したファイルの上では、二重否定除去の型検査を通ります。同じ定理を、一階述語論理、直観主義論理、古典論理と差し替えて試すことで、それぞれの論理体系の境界が分かります。

定理そのものを新しく得ることが目的ではありません。「A かつ B ならば B かつ A」が成り立つことは、はじめから分かっています。

2 つ目の対象は、一階述語論理や高階論理といった論理体系そのものについての性質です。「この型システムには型の安全性が成り立つ」「この体系のこの規則は、他の規則から導ける」といった定理です。一階述語論理の中で証明するのではなく、一階述語論理について証明します。Twelf の論文は、これをメタ理論と呼んでいます。

この場合に知りたいのは、記述した論理体系そのものが、望ましい性質を持つかどうかです。プログラミング言語の型システムを記述したなら、「型の付いたプログラムは実行時にエラーで止まらない」という性質を知りたい。論理体系を記述したなら、「矛盾が導けない」という性質を知りたい。こうした性質を、証明として書き、型検査で確かめます。

2 つ目の用途が、Edinburgh LF の特色です。一階述語論理や高階論理といった論理体系そのものを研究の対象にできます。複数の論理体系を同じ言語の上に記述すれば、体系どうしを比べることもできます。一階述語論理の推論規則が高階論理の推論規則から導けるか、といった問いを、同じ土俵の上で扱えます。

いずれの場合も、証明を書くのは Edinburgh LF の上です。Lean 4 や Rocq が出力した証明を持ち込んで検査する、という使い方ではありません。

ここで、Edinburgh LF と Dedukti の目的の違いを押さえておきます。

Dedukti の目的は、定理証明支援系が出力した証明を、別の証明検査器で再検証することです。だから翻訳器が必要になり、翻訳器の対象は Lean 4 や Rocq といった実在の定理証明支援系になります。

Edinburgh LF の目的は、そうではありません。
1987 年の論文が扱っているのは、論理体系そのものです。

一階述語論理や高階論理といった論理体系を、ひとつの言語の上に定義し、比較し、その性質を調べる。これが目的です。

当時、Lean 4 も Rocq も存在せず、他の定理証明支援系が出力した証明を再検証するという課題は、まだ立っていませんでした。

用途も、そこに沿っています。

Edinburgh LF の主な用途は、プログラミング言語や論理体系の仕様を記述し、その体系についての性質を証明することです。

「この型システムには型の安全性が成り立つ」といった性質を、Edinburgh LF の上で証明します。他の定理証明支援系から証明を受け取る用途ではありません。

Edinburgh LF は、いまも使われています。

実装は Twelf です。

Twelf は Pfenning と Schürmann が 1999 年の国際会議 CADE で報告した処理系で、Linux ディストリビューションのパッケージとして配布が続いています。ただし、Twelf 本体の版は 1.7.1 で止まっており、開発が活発とは言えません。

Dedukti は、Edinburgh LF の言語 λΠ計算に書き換え規則を足したものです。

言語の系譜としては Edinburgh LF に連なりますが、目的は違います。

出典

• R. Harper, F. Honsell, G. Plotkin, "A framework for defining logics", Journal of the ACM 40(1), 1993, pp. 143-184. https://dl.acm.org/doi/10.1145/138027.138060
• F. Pfenning, C. Schürmann, "System Description: Twelf — A Meta-Logical Framework for Deductive Systems", CADE 1999. https://www.cs.cmu.edu/~fp/papers/cade99.pdf

Isabelle との関係。
Logical Framework の考え方は、Dedukti だけのものではありません。

Isabelle は、Pure と呼ばれるメタ論理の上に、HOL や ZF といった論理体系を載せる作りになっています。

今回の記事で見た、符号化ファイルを差し替えれば扱う論理体系が変わる、という構造と同じ考え方が、広く使われている定理証明支援系の中にすでに入っています。

なお、Isabelleが、Isabelle pureと呼ばれる基盤の上に、複数の異なる論理公理体系を載せらえる構造については、本記事執筆者が過去に書いた以下の記事に詳述しています。

実績と限界。
Dedukti は 1998 年から続く研究です。それにもかかわらず、産業界での配備実績を、筆者は公開資料の範囲で確認できませんでした。

Deduktiは、何ができて、何ができていないのかを取り上げます。

なお、今回の初回記事では、翻訳が成立することを前提に話を進めましたが、実際には、翻訳がいつでも成立するわけではありません。

翻訳が成立するための条件は 5 つあります。この条件は、後続の記事で扱います。

📌 用語のミニ解説

本記事に出てきた用語をまとめました

定理証明支援系（proof assistant） ── 人間が数学の証明を書き、その証明が正しいかを機械が検査するためのソフトウェアです。Lean 4、Rocq（旧 Coq）、Isabelle、Agda、HOL Light などがあります。本記事では「定理証明器」「定理証明言語」も、ほぼ同じ意味で使っています。

証明項（proof term） ── 証明の全手順を、ひとつの式として書き表したものです。利用者が書くのは「まず帰納法を使え」といった指示ですが、定理証明支援系はその指示を実行した結果を、関数と関数適用だけからなる式に落とします。この式が証明項です。

型検査（type checking） ── ある式が、宣言された型に合っているかを確かめる処理です。証明項の場合、型が命題にあたるので、型検査を通ることが、証明が正しいことにあたります。

識別子（identifier） ── .dk ファイルの中で名前として使われるものです。imp や prop や enc.Pi がそうです。使う前に、imp : prop -> prop -> prop. のように型とともに宣言します。

書き換え規則（rewriting rule） ── 「左辺の式が現れたら、右辺の式に置き換えてよい」という指示です。[a, b] Prf (imp a b) --> Prf a -> Prf b. のように書きます。

符号化（encoding） ── ある論理体系や型理論を、識別子の宣言と書き換え規則の組に置き換える、固定的な置き換え規則のことです。

符号化ファイル ── 符号化を記述した .dk ファイルです。翻訳器に同梱されています。本記事で付けた呼び名で、Dedukti の公式な用語ではありません。

証明ファイル ── 翻訳された証明項が記述された .dk ファイルです。翻訳のたびに新しく作られます。こちらも本記事で付けた呼び名です。

翻訳器 ── ある定理証明支援系が出力した証明項を読み込み、.dk ファイルに書き直すプログラムです。lean2dk、CoqInE、hol2dk、isabelle_dedukti、Agda2Dedukti などがあります。

CIC（Calculus of Inductive Constructions） ── Rocq が立脚する型理論です。Lean 4 が立脚するのは、その変種です。宇宙の階層と帰納型を持ちます。

宇宙（universe） ── 「型の型」にあたるものです。型そのものを値として扱うために、階層を作ります。

λΠ計算 modulo rewriting ── Dedukti の言語です。依存型と書き換え規則を持ちます。詳しくは次回以降の記事で扱います。

Logical Framework ── 複数の論理体系の推論規則を記述するための言語のことです。詳しくは次回以降の記事で扱います。

実機検証について

本記事に掲載したコードと出力は、すべて筆者が実行して得たものです。
掲載にあたって、読みやすさのために改行を入れた箇所があります。内容は変えていません。

検証環境

項目	内容
OS	Ubuntu 24.04（コンテナ環境）
Dedukti	v2.7（GitHub の Deducteam/Dedukti をソースからビルド）
OCaml	4.14.1
dune	3.14
Lean 4	4.22.0-rc4
lean2dk	GitHub の Deducteam/lean2dk、コミット 471208f（2026 年 6 月 13 日）

検証できたこと

1. Lean 4 で 6 行の定義（MyTrue の宣言と、test : MyTrue → MyTrue の証明）を書き、Lean 4 が検証を完了しました。
2. Lean 4 の内部表現を出力し、証明項が Lean.Expr.forallE と Lean.Expr.lam で構成されていることを確認しました。
3. lean2dk を実行し、証明ファイル 2 本（fixtures_Mini.dk、AuxLvls.dk）が生成されることを確認しました。
4. lean2dk の符号化ファイルが dk/enc/ に 7 本あり、lean2dk の実行前と実行後で中身が同じであることを確認しました。
5. Dedukti v2.7 で、符号化ファイル 7 本と証明ファイル 2 本、計 9 本すべてを型検査し、すべて受理されることを確認しました。
6. 証明ファイルの最終行を => x0. から => MyTrue. に書き換えた誤った版を作り、Dedukti が拒否することを確認しました。エラーは型の不一致として報告されます。
7. CoqInE、hol2dk、isabelle_dedukti、Agda2Dedukti の各リポジトリを取得し、符号化ファイルの中身を読みました。本記事の 4 つの対応表は、この読解にもとづくものです。

検証できなかったこと・注意

• 検査 7 は、符号化ファイルを読んだだけです。CoqInE、hol2dk、isabelle_dedukti、Agda2Dedukti を実際に動かしてはいません。したがって Lean 4 以外の対応表は、実行結果ではありません。
• lean2dk の実行には --no-elim という選択肢を付けました。付けない場合、could not find constant というエラーで停止しました。この選択肢は、Lean4Less による前処理を省くものです。
• Lean 4 の組み込みの True を使うと同じエラーで停止したため、MyTrue という自作の命題を使いました。
• 本記事で扱ったのは、6 行の定義という最小の例です。研究の最前線で証明された定理を翻訳して検査したわけではありません。
• 産業界での配備実績は、筆者が調べた公開資料の範囲では確認できませんでした。

訂正一覧

公開後に訂正した箇所を、ここに追記していきます。現時点ではありません。

関連記事

本記事の内容に関係する、筆者の過去記事です。

• 依存型を使わないIsabelle/HOL とは何か ── AWS のクラウド基盤を検証した定理証明系は、なぜ証明を自動で探せるのか
• 論理はひとつではない ── 圏論論理学がつなぐ量子論理・トポス・圏論的量子力学
• 論理公理系の産業応用 全地図 ── 古典・直観主義・線形・様相・時相・記述・量子論理はどこで使われているのか
• 形式証明は「仕様が人間の意図を反映しているか」は保証しない ── Correctness と Appropriateness の境界
• AI Agent は社会規範に反していても、論理的に正しければ実行可能と判断してしまう ── 「何をしてよいか」を決める責任は、AIが賢くなるほど人間に集中する

出典一覧

Dedukti 本体

• Deducteam, Dedukti（GitHub リポジトリ）. https://github.com/Deducteam/Dedukti
• F. Blanqui et al., "Some Axioms for Mathematics", FSCD 2021.
• Inria, Deducteam 2024 Activity Report. https://radar.inria.fr/rapportsactivite/RA2024/deducteam/DEDUCTEAM-RA-2024.pdf

翻訳器

• Deducteam, lean2dk（GitHub リポジトリ）. https://github.com/Deducteam/lean2dk
• Deducteam, CoqInE（GitHub リポジトリ）. https://github.com/Deducteam/CoqInE
• Deducteam, hol2dk（GitHub リポジトリ）. https://github.com/Deducteam/hol2dk
• Deducteam, isabelle_dedukti（GitHub リポジトリ）. https://github.com/Deducteam/isabelle_dedukti
• Deducteam, Agda2Dedukti（GitHub リポジトリ）. https://github.com/Deducteam/Agda2Dedukti

Logical Framework

• R. Harper, F. Honsell, G. Plotkin, "A framework for defining logics", Journal of the ACM 40(1), 1993, pp. 143-184. https://dl.acm.org/doi/10.1145/138027.138060
• F. Pfenning, C. Schürmann, "System Description: Twelf — A Meta-Logical Framework for Deductive Systems", CADE 1999. https://www.cs.cmu.edu/~fp/papers/cade99.pdf

定理証明支援系

• Lean 4（GitHub リポジトリ）. https://github.com/leanprover/lean4

（２回目の記事に続く）