以下の内容はhttps://lpha-z.hatenablog.com/entry/2025/08/10/231500より取得しました。

Lean 4 で巨大数の大きさを証明してみる

最近VRChatにこういうワールドができたらしくて、見てきました。

巨大数については、「巨大数論」が「まだ書きかけ版」（2013年に出た「初版」の前のバージョン。おそらく2009年ごろの版）だった頃に少し勉強したことがありました。 なので、その範囲が紹介されている上記ワールドは少しなつかしさがありました。 最近はどんどんすごいものが出ているようで、ついていけていません。

上記ワールドでは、ふぃっしゅ数バージョン1の大きさが紹介されています。 今回は、Lean 4という定理証明支援系を使って、その大きさを評価してみたいと思います。 具体的には、ふぃっしゅ数バージョン1 | 巨大数研究 Wiki | Fandomに書かれている次の言明をLean 4で形式的に証明してみます。

SS変換の1回目はS変換4回なので、S変換2回程度の A(2,3,3) に相当する A(1,0,1,1) よりは大きく、

巨大数の議論はたいてい、あまり形式的ではなく*1、また実際に計算して確認することも事実上不可能です。 また、「とんでもなく大きい」「～と比べものにならないほど急速に増大する」などの記述が乱舞しますが、具体的にどのくらい大きいのかわかりづらいです。 定理証明支援系を用いることで、この問題を解決し、巨大数が実際に“大きい”ことの証明ができたと確信することができるようになります。

準備

import Mathlib.Tactic

2変数アッカーマン関数

定義

アッカーマン関数は、次で定義される関数です。

A(m,n) =\begin{cases} n + 1 \;\;\mathrm{if}\;\; m = 0 \\ A(m-1,1) \;\;\mathrm{if}\;\; n = 0 \\ A(m-1,A(m,n-1)) \;\;\mathrm{otherwise} \end{cases}

この関数は、原始再帰の操作を対角化する関数になっています。 以降で引数を増やす一般化を施したアッカーマン関数が登場するので、2変数アッカーマン関数と呼ぶことにします。

def Ackermann2 : Nat -> Nat -> Nat
| 0, n => n + 1
| Nat.succ m, 0 => Ackermann2 m 1
| Nat.succ m, Nat.succ n => Ackermann2 m $ Ackermann2 (m+1) n

Lean 4は関数型言語なので、関数適用は引数を並べるだけです。 Nat.succ mは、要するにm+1のことです。 $はHaskellで出てくるのと同じ関数適用演算子で、そこから末尾までを括弧でくくるのと同じ効果を持ちます。 =や:=をも越えて末尾までくくろうとするのでかなり不便です……。

計算例1

計算例を紹介しましょう。 A(3, 3) = 61です。

example : Ackermann2 3 3 = 61 := by simp [Ackermann2]

simpは、ある程度かんたんな計算を自動で進めることで証明を作ってくれる、タクティックと呼ばれる半自動証明方法です。 simpはデフォルトでは特定の簡略化しか行いませんが、角括弧の中に等式を入れることで、それを用いた簡略化も行ってくれます。

第一引数の固定

もう少し大きな値を返す例を計算してみたいですが、再帰深度制限にかかってしまうので、定義をそのまま展開して計算することはできません。 アッカーマン関数の第一引数を固定すると、乗算・冪乗・テトレーション……など（に近い関数）になることが示せるので、まずはそちらを証明しましょう。

0の場合

まず、 A(0, n) = n + 1です（定義より明らか）。

lemma Ackermann2_0_eq_lemma n : Ackermann2 0 n = n + 1 := by simp [Ackermann2]

1の場合

次に、 A(1, n) = n + 2であることを帰納法で簡単に示すことができます。

lemma Ackermann2_1_eq_lemma n : Ackermann2 1 n = n + 2 := by
  induction n with
  | zero => simp [Ackermann2]
  | succ n ihn => simpa [Ackermann2] using ihn

Lean4 では、帰納法はinductionと書きます。 simpa [X] using hは、Xという等式（定理または仮定）を用いて証明したい命題を書き換え、仮定hと一致させることにより証明を行うタクティックです。 ここでihnは帰納法の仮定、つまり命題が入っている変数です。 induction hypothesisなのでihみたいな変数名を使うことが慣例ですが、任意の名前を付けることができます。 今後ネストされた再帰が出てくるので、どの変数の帰納法の仮定なのかを明示した命名を使うことにします。

ところで、nが二回出てきていて、「n = succ n！？」と思ってしまうかもしれないですが、最初のnは破棄されています。 普通の高校数学で習うような数学的帰納法ではkを導入したりして紛れがないように書きますが、「∀n. φ(n)を証明するには、φ(0)と∀n. φ(n)→φ(n+1)の二つを証明すればいい」ということが数学的帰納法の本質で、両者に出てくるnはそれぞれ異なる∀n.で導入された別の変数なので、見た目上同じ名前がついていても問題ありません。

2の場合

さらに、 A(2, n) = 2n + 3であることも、上で示した A(1, n) = n + 2であることを使えば、帰納法で簡単に示すことができます。

lemma Ackermann2_2_eq_lemma n : Ackermann2 2 n = 2 * n + 3 := by
  induction n with
  | zero => simp [Ackermann2]
  | succ n ihn => simp [Ackermann2.eq_3]; simpa [ihn] using Ackermann2_1_eq_lemma (2*n+3)

ここで、Ackermann2.eq_3は自動生成された等式定理で、Ackermann2関数の3番目の定義に基づく等式定理です。

3の場合

同様に、 A(3, n) = 2^{n+3} - 3であることも、 A(2, n) = 2n + 3であることを使えば、帰納法で示すことができます。 ただし、冪乗はタクティックで自動的に証明できる範囲を超えてしまっているので、手動で多少のヒントを与える必要があります。 なお、Natの引き算は部分的引き算*2 x \mathbin{\dot-} y = \max \{0, x - y\}になっていて面倒なので、少し変形した命題を証明することにします。

lemma Ackermann2_3_eq_lemma n : (Ackermann2 3 n) + 3 = 2 ^ (n+3) := by
  induction n with
  | zero => simp [Ackermann2]
  | succ n ihn => rw [show 2 ^ (n+1+3) = 2 * 2 ^ (n+3) by group, ← ihn]
                  rw [Ackermann2.eq_3, Ackermann2_2_eq_lemma]
                  group

ここで、rwは等式を用いて証明すべき命題を書き換えるタクティックです（rewrite）。 rwタクティックに渡す等式はshow 等式定理 by タクティックのようにその場で作ることも可能です。 ← ihnとしているのは、等式定理を逆方向に適用することを意味します。 ここで、x = yとあった時に証明したい命題のxをyで置き換えるのが“順方向”、yをxで置き換えるのが“逆方向”です。 groupタクティックは、群に関する簡単な命題を証明するタクティックで、ここでは可換性を適用して式を整理して証明しています。

4の場合

最後は、 A(4, n) = {}^{n+3}2 - 3であることを、 A(3, n) = 2^{n+3} - 3であることを使って、帰納法で示します。 なお、左肩に書くのはテトレーションの記法です。 同様に、引き算がなくなるよう変形した命題を証明します。

def Tetration : Nat -> Nat -> Nat
| _, 0 => 1
| m, Nat.succ n => m ^ (Tetration m n)

lemma Ackermann2_4_eq_lemma n : (Ackermann2 4 n) + 3 = Tetration 2 (n+3) := by
  induction n with
  | zero => simp [Ackermann2, Tetration]
  | succ n ihn => rw [show Tetration 2 (n+1+3) = 2 ^ Tetration 2 (n+3) by simp [Tetration]]
                  rw [← ihn]
                  rw [Ackermann2.eq_3]
                  rw [Ackermann2_3_eq_lemma]

rwタクティックで終了している点が先ほどと異なります。 これは、rwタクティックには、証明すべき命題を書き換えた結果自明な形になればそれを以って証明とするオプショナルな機能がついていることによります。

計算例2

これを使うと、 A(4,1) = 65533であることを示せます。

example : Ackermann2 4 1 = 65533 := Nat.add_right_cancel $ Ackermann2_4_eq_lemma 1

ここで、Nat.add_right_cancelは標準ライブラリにある定理で、前提条件h「n + m = k + m」を満たすとき、n = kであるという、標準ライブラリにある定理です。 定理は一種の関数として表現されているため、前提条件を関数適用のように与えることができます。 ここでは、hとしてAckermann2_4_eq_lemma 1を与えています。 これは、(Ackermann2 4 1) + 3 = Tetration 2 (1+3)という定理ですね。

ちなみに、標準ライブラリにある定理をすべて覚える必要はなく、apply?タクティックなどで検索することができます。

計算例3

さらに、 A(4,4) = {}^72 - 3であることも示せます。 ただし、Nat.add_right_cancelを直に使おうとすると {}^72が3より大きいかを実際に計算しようとして指数の制限（指数が256を超えるものはできないらしい）にかかるため、ひと工夫が必要です。

example : Ackermann2 4 4 = (Tetration 2 7) - 3 := by
  have : Ackermann2 4 4 + 3 = (Tetration 2 7) := Ackermann2_4_eq_lemma 4
  omega

haveは補題を用意するタクティックです。

ここで、omegaタクティックは、自然数の線形計画問題を決定するタクティックです。 おおよそ、加算・等式・不等式からなる命題を証明できると思えばよいでしょう。 全自動で証明してくれるわけではなく、適切な中間補題を用意することが必要になることがあります。 中間補題自体もomegaタクティックで証明できたりするので、適切なものをこちらから指定するのが大事（何を中間補題としてとるのが適切かを考えるのが腕の見せ所）ということです。

おそらく、omegaタクティックは冪乗の詳細に立ち入らない（ {}^72を記号的に扱う）ため、巨大数の展開の沼にはまることなく、証明の探索に成功したのだと思います。 Ackermann2 4 4 + 3 = (Tetration 2 7)が成り立っている時、右辺を具体的に計算せずともそれが3以上であることがわかり、その事実から証明可能です。

全域性の証明について

アッカーマン関数は、原始再帰関数でない関数（二重再帰関数）として有名です。 その全域性（停止性）は、 \mathrm{I\Sigma_1}では示せませんが、 \mathrm{I\Sigma_2}であれば示せます。 \mathrm{I\Sigma_2}は、順序数 \omega^\omegaまでの超限帰納法です。 実際には、 \omega^2までの超限帰納法が、アッカーマン関数の全域性の証明に必要十分です。

3変数アッカーマン関数

3変数アッカーマン関数と言うと、普通はアッカーマンが提案したオリジナルの関数を言います。 この関数は、追加の引数を取ることでより繊細*3な計算が可能な関数で、例えば \phi(a,b,3) = ^{b+1}\!\!aなどが表現できます（2変数アッカーマン関数は底が2のものしか計算できませんでした）。

一方で、巨大数の文脈では、「原始再帰の操作を対角化する操作」を対角化するよう設計された、2変数アッカーマン関数よりも真に増大度の大きい関数を指します。 この関数は、次のように定義されます（多変数アッカーマン関数 | 巨大数研究 Wiki | Fandom）。

A(c,b,a) =\begin{cases} a + 1 \;\;\mathrm{if}\;\; c = b = 0 \\ A(c-1,a,a) \;\;\mathrm{if}\;\; b = 0 \\ A(c,b-1,1) \;\;\mathrm{if}\;\; a = 0 \\ A(c,b-1,A(c,b,a-1)) \;\;\mathrm{otherwise} \end{cases}

追加された A(c, 0, a) = A(c-1,a,a)が重要な部分で、これにより「原始再帰の操作を対角化する操作」を対角化することができます。

def Ackermann3 : Nat -> Nat -> Nat -> Nat
| 0, 0, a => a + 1
| Nat.succ b, 0, a => Ackermann3 b a a
| x, Nat.succ b, 0 => Ackermann3 x b 1
| x, Nat.succ b, Nat.succ a => Ackermann3 x b $ Ackermann3 x (b+1) a

基本的には左側の引数が大きい方が大きな数を返しますが、0付近では異なることに注意します。

example : Ackermann3 0 0 1 = 2 := by simp [Ackermann3]
example : Ackermann3 0 1 0 = 2 := by simp [Ackermann3]
example : Ackermann3 1 0 0 = 1 := by simp [Ackermann3]

最も左の引数が0の時、2変数アッカーマン関数と同等になることは、定義から明らかです。 これを示すためには、2変数アッカーマン関数の再帰構造と同様の二重帰納法が必要です。

theorem Ackermann3zero_eq_Ackermann2 : Ackermann3 0 x y = Ackermann2 x y := by
  induction x generalizing y with
  | zero => simp [Ackermann3, Ackermann2]
  | succ x ihx =>
      induction y with
      | zero => rw [Ackermann3.eq_3, Ackermann2.eq_2]; exact ihx
      | succ y ihy => rw [Ackermann3.eq_4, Ackermann2.eq_3]; simpa [ihy] using ihx

ここで、induction x generalizing yは、yを先に固定した命題をxに関する帰納法で証明したあとにyが自由変数であることを以って全称命題を証明するするのではなく、yに関する全称命題自体をxに関する帰納法で証明することを意味します。 つまり、二重帰納法をする場合に必要です。

exactタクティックは、証明したい命題が、仮定や定理そのものになっている時に、証明を終わらせるタクティックです。

rw [Ackermann3.eq_3]などとしていますが、定義の順番を入れ替えることに耐性がなくなるのが不満です。 rw [Ackermann3.eq_def]; split <;> try contradiction; expose_names; rw [show m = x by omega]みたいに書けばその問題はなくなりますが、やたらに長くなってしまいます。

GPT-5に聞いたら、「@[simp] を付けて名前依存を下げるといいよ！」とか言ってきました。 「巨大数の計算の最初の方はどんな感じかな？」と試したいとき、simpを使った瞬間にAckermann3 2 3 3とかを具体的に展開しきろうとしてしまって大変なことになりそうです。 全称命題を証明するときは気にする必要がなく、具体的な計算の場合はsimp onlyを使って@[simp]のついた等式定理を使った変形はしない、とすれば大丈夫そうでしょうか。 そもそも、@[simp]をつけるのではなく、simp [Ackermann3]（あるいは、simpの自動的な変形が気に入らない時はsimp only [Ackermann3]）を使えばいいのかもしれませんが、計算が進行しない場合がたまにあったりして、その違いがいまだによくわかっていません。

4変数アッカーマン関数

同様の考え方で、さらに引数を追加することができます（多変数アッカーマン関数 | 巨大数研究 Wiki | Fandom）。

A(d,c,b,a) =\begin{cases} a + 1 \;\;\mathrm{if}\;\; d = c = b = 0 \\ A(d-1,a,0,a) \;\;\mathrm{if}\;\; c = b = 0 \\ A(d,c-1,a,a) \;\;\mathrm{if}\;\; b = 0 \\ A(d,c,b-1,1) \;\;\mathrm{if}\;\; a = 0 \\ A(d,c,b-1,A(d,c,b,a-1)) \;\;\mathrm{otherwise} \end{cases}

同様に、追加された A(d, 0, 0, a) = A(d-1,a,0,a)が重要な部分で、これにより『「原始再帰の操作を対角化する操作」を対角化する操作』を対角化することができます。

def Ackermann4 : Nat -> Nat -> Nat -> Nat -> Nat
| 0, 0, 0, a => a + 1
| Nat.succ b, 0, 0, a => Ackermann4 b a 0 a
| x, Nat.succ b, 0, a => Ackermann4 x b a a
| x, y, Nat.succ b, 0 => Ackermann4 x y b 1
| x, y, Nat.succ b, Nat.succ a => Ackermann4 x y b $ Ackermann4 x y (b+1) a

最も左の引数が0の時、3変数アッカーマン関数と同等になることは、定義から明らかです。 3変数アッカーマン関数の再帰構造と同様の三重帰納法を使えば示すことができます。

theorem Ackermann4zero_eq_Ackermann3 : Ackermann4 0 x y z = Ackermann3 x y z := by
  induction x generalizing y z with
  | zero =>
      induction y generalizing z with
      | zero => simp [Ackermann4, Ackermann3]
      | succ y ihy =>
          induction z with
          | zero => rw [Ackermann4.eq_4, Ackermann3.eq_3]; exact ihy
          | succ z ihz => rw [Ackermann4.eq_5, Ackermann3.eq_4]; simpa [ihz] using ihy
  | succ x ihx =>
      induction y generalizing z with
      | zero => rw [Ackermann4.eq_3, Ackermann3.eq_2]; exact ihx
      | succ y ihy =>
          induction z with
          | zero => rw [Ackermann4.eq_4, Ackermann3.eq_3]; exact ihy
          | succ z ihz => rw [Ackermann4.eq_5, Ackermann3.eq_4]; simpa [ihz] using ihy

計算例

いくつか例を計算してみましょう。 まず、 A(1,0,1,0) = 3です。

lemma example1 : Ackermann4 1 0 1 0 = 3 := by simp [Ackermann4]

次に、 A(1,0,1,1) = A(2,3,3)です。 右辺はグラハム数を超えるような巨大数なので*4、これを具体的に計算することはできません。

lemma example2 : Ackermann4 1 0 1 1 = Ackermann3 2 3 3 := by
  rw [Ackermann4, example1, Ackermann4, Ackermann4zero_eq_Ackermann3, Ackermann3]

ふぃっしゅ数バージョン1の定義

定義は巨大数論 第二版の91ページやふぃっしゅ数バージョン1 | 巨大数研究 Wiki | Fandomを参照するなどしてください。 それを書き下したものが以下になります。

def B_func (f : Nat -> Nat) : Nat -> Nat -> Nat
| 0, n => f n
| Nat.succ m, 0 => B_func f m 1
| Nat.succ m, Nat.succ n => B_func f m $ B_func f m.succ n
termination_by
  m n => (m, n)
decreasing_by
  · tauto -- (m+1,0) > (m,1)
  · omega -- (m+1,n+1) > (m+1,n)
  · tauto -- (m+1,n+1) > (m,Big)

def NFPair := Prod Nat (Nat->Nat)

def S_transform (mf : NFPair) : NFPair :=
  let (m, f) := mf
  let g x := B_func f x x
  (g m, g)

def Tr := NFPair -> NFPair

def Repeat {T : Type} (f : T -> T) : Nat -> (T -> T)
| 0 => id
| Nat.succ m => fun p => Repeat f m $ f p

def SS_transform (mfS : Prod NFPair Tr) : Prod NFPair Tr :=
  let (mf, S) := mfS
  let (m, f) := mf
  let fm : Nat := f m
  (Repeat S fm mf, Repeat S fm)

def F1 := (Repeat SS_transform 63 ((3, fun x => x + 1), S_transform)).fst.fst

ここに現れるB関数は、アッカーマン関数とほぼ同じですが、基底ケースが与えられた関数fの適用になっています。 つまり、アッカーマン関数は後者関数を繰り返し適用するものですが、B関数は与えられた関数fを繰り返し適用するものになっています。

S変換は、自然数と関数のペアから自然数と関数のペアへの写像です。 B関数を通すことで、与えられた関数を所与としたときの原始再帰の操作を対角化しています。

SS変換は、自然数と関数と変換のトリプレットから自然数と関数と変換のトリプレットへの写像です。 S変換を繰り返し適用することで、『「原始再帰の操作を対角化する操作」を対角化する操作』を対角化しています。

どうでもいいですが、初めて多相関数を使いました（Repeat関数）。

B関数の停止性

B関数は停止性が明らかでないため、その証明（以下に再掲）が付随しています。

termination_by
  m n => (m, n)
decreasing_by
  · tauto -- (m+1,0) > (m,1)
  · omega -- (m+1,n+1) > (m+1,n)
  · tauto -- (m+1,n+1) > (m,Big)

引数mとnについて、ペア(m, n)の辞書的順序において真に小さい方向にのみ再帰を行うことを以って停止性を証明しています。 \omega^2の整礎性に基づいて証明していると言い換えてもいいでしょう。 \omega^2までの超限帰納法とも言います。

よく考えると、ペアの辞書的順序（ \omega^2の形）どころか、自然数の通常の順序（ \omegaの形）に対してですら、「真に小さい方向にのみ再帰を行っているから、停止する」というのは結構すごい事実です。 一回の関数呼び出しが複数の再帰呼び出しを含む場合、例えば二分木状の呼び出し構造となり、再帰回数の合計は膨大になるからです。 実際、いわゆる愚直フィボナッチ関数がそれになっています。

すべての場合分けにおいて真に小さい方向にのみ再帰を行っているかは、自動的には判断されないようです。 tautoタクティックは、命題論理レベルで示せることを証明するタクティックです。 しかしなぜか、第一要素が減ったなら、ペアの順序でも減っている、ということを示せるようです。 さらに不思議なことに、第二要素が減る場合はtautoタクティックでは証明できませんでした（omegaタクティックは便利で、ペアに関する証明なども作ってくれます）。

というか、Ackermann2関数とかも停止性が明らかではなさそうですが、なんで付けなくても怒られなかったんでしょうか……？

→GPT-5に聞いたところどうやら、Ackermann2関数などはLean 4処理系的には「この再帰は辞書式順序で見れば減っているから停止する」と判断できるようです。 処理系はなかなか賢いですね。一方でB_funcの方は、引数fが増えているため、このパターンを外れて自動では推論できなかったようです。

B関数の性質の証明

基本関数を f_0（ x \mapsto x+1）とした（Ackermannタイプの*5）S変換は、実は3変数アッカーマン関数の系列を生成します。 このことを示すため、まずはB関数の性質を証明していきます。

B関数の正値性

B関数に与える関数fが、厳密膨張的である（ \forall x. x \lt f(x)）とき、残りの二つの引数がいかなる数であっても、B関数は正の数を返します。

lemma B_func_positive (f : Nat -> Nat) (hf1 : ∀x, x < f x)
  : ∀m n, 0 < B_func f m n := by
  intro m n
  induction m generalizing n with
  | zero => rw [B_func.eq_1]; exact Nat.zero_lt_of_lt (hf1 n)
  | succ m ihm =>
      match n with
      | 0 => rw [B_func.eq_2]; exact ihm 1
      | n+1 => rw [B_func.eq_3]; exact ihm $ B_func f m.succ n

ここで、Nat.zero_lt_of_ltは、a < bならば0 < bであるという、標準ライブラリにある定理です。

B関数は厳密膨張的・左引数優位・狭義単調増加

B関数に与える関数fが、厳密膨張的かつ狭義単調増加（ \forall x. \forall y. x \lt y → f(x) \lt f(y)）であるとき、次の三つの性質が成り立ちます。

  1. 任意のmに対し、B_func f m : Nat -> Natは、厳密膨張的（nよりもB_func f m nの方が大きい）
  2. 任意のmとnに対し、B_func f (m+1) nはB_func f m (n+1)以上である（右の引数を増やすよりも左の引数を大きくする方がより早く増大する）
  3. 任意のmに対し、B_func f m : Nat -> Natは、狭義単調増加（nより大きいxに対し、B_func f m nよりもB_func f m xの方が大きい）

これらの性質は二重帰納法で示すことになりますが、性質1を示すためには性質2を補題として使いたく、性質2を示すためには性質3を補題として使いたく、性質3を示すためには性質2を補題として使いたいため、すべての命題を連結した上で示すことにします（性質2と性質3だけ連結して証明してもよかったですね）。

lemma B_func_monotonic_lemma1
  (f : Nat -> Nat) (hf1 : ∀x, x < f x) (hf2 : ∀x y, x < y → f x < f y)
  : ∀ m n, (n < B_func f m n)
           ∧ (B_func f m (n+1) ≤ B_func f (m+1) n)
           ∧ (∀ x, n < x → B_func f m n < B_func f m x) := by
  have hf3 x y : x ≤ y → f x ≤ f y := by
    by_cases h : x = y
    · exact fun a => Nat.le_of_eq (congrArg f h)
    · intro
      exact Nat.le_of_succ_le (hf2 x y (show x < y from by omega))

  intro m n
  induction m generalizing n with
  | zero =>
      induction n with
      | zero =>
          refine ⟨?_, ?_, ?_⟩
          · rw [B_func.eq_1]; exact hf1 0
          · rw [B_func.eq_1, B_func.eq_2, B_func.eq_1]
          · intro x
            rw [B_func.eq_1, B_func.eq_1]
            exact hf2 0 x
        | succ n ihn =>
            have ihn2 := ihn.right.left; clear ihn
            refine ⟨?_, ?_, ?_⟩
            · rw [B_func.eq_1]; exact hf1 (n+1)
            · rw [B_func.eq_1, B_func.eq_3]
              calc
                f (n+1+1)
                  = B_func f 0 (n+1+1)            := Eq.symm $ B_func.eq_1 f (n+1+1)
                _ ≤ B_func f 0 (B_func f 0 (n+1)) := by rw [B_func.eq_1, B_func.eq_1, B_func.eq_1]
                                                        exact hf3 (n+1+1) (f (n+1)) (hf1 (n+1))
                _ ≤ B_func f 0 (B_func f 1 n)     := by rw [B_func.eq_1]
                                                        nth_rewrite 2 [B_func.eq_1]
                                                        exact hf3 (B_func f 0 (n+1)) (B_func f 1 n) ihn2
            · intro x
              rw [B_func.eq_1, B_func.eq_1]
              exact hf2 (n + 1) x
    | succ m ihm =>
        have ihm1 n := (ihm n).left
        have ihm2 n := (ihm n).right.left
        have ihm3 n := (ihm n).right.right
        clear ihm

        induction n with
        | zero =>
          refine ⟨?_, ?_, ?_⟩
          · rw [B_func.eq_2]
            exact B_func_positive f hf1 m 1
          · rw [B_func.eq_2]
          · intro x hx
            calc
              B_func f (m+1) 0 = B_func f m 1     := B_func.eq_2 f m
              _                < B_func f m (x+1) := ihm3 1 (x+1) (show 1 < x+1 by bound)
              _                ≤ B_func f (m+1) x := ihm2 x
        | succ n ihn =>
          have ihn2 := ihn.right.left
          have ihn3 := ihn.right.right
          clear ihn

          refine ⟨?_, ?_, ?_⟩
          · calc
              n+1 < n+2 := by simp
              _   < B_func f m (n+2)     := ihm1 (n+2)
              _   ≤ B_func f (m+1) (n+1) := ihm2 (n+1)
          · refine Nat.le_of_succ_le $ Nat.succ_le_of_lt ?_ -- a<b を示すことで a≤b を証明
            calc
              B_func f (m+1) (n+1+1)
                = B_func f m (B_func f (m+1) (n+1))   := B_func.eq_3 f m (n+1)
              _ < B_func f m ((B_func f (m+1+1) n)+1) := ihm3 (B_func f (m+1) (n+1)) ((B_func f (m+1+1) n)+1)
                                                           $ Order.lt_add_one_iff.mpr ihn2
              _ ≤ B_func f (m+1) (B_func f (m+1+1) n) := ihm2 (B_func f (m+1+1) n)
              _ = B_func f (m+1+1) (n+1)              := Eq.symm $ B_func.eq_3 f (m+1) n
          · intro x hx
            match x with
            | 0 => contradiction
            | t+1 =>
                rw [B_func.eq_3, B_func.eq_3]
                exact ihm3 (B_func f (m + 1) n) (B_func f (m + 1) t) $ ihn3 t (show n < t by omega)

かなり長くなりました。 二重帰納法の後にrefineで分解した後にcalcしていてインデントが深く、このブログの幅に収まらなくなっています。

新登場したタクティックは次の通りです。

  • by_cases：場合分けにより証明する
  • intro：証明したい命題が∀x, PやQ → Rで始まっている時、それを仮定側に移動する
    • ∀x < y, Pの時は、intro x hxなどとすることでxを仮定側に移動しつつ（仮定として役立つわけではなさそう？）、x < yも仮定側に移動してhxで参照できるようになる
  • refine：定理や補題を?_付きで使用することで、本来の命題の証明のために欠けている補題の証明に置き換える
    • refine ⟨?_, ?_, ?_⟩は要するに、P ∧ Q ∧ Rを証明するときに分解するということ
  • calc：等式や不等式（推移律が成り立つもの）の証明をするために、証明をつなぎ合わせる
  • nth_rewrite：与えた等式補題が使えるn番目を書き換える
    • rwだと1番目が書き換わるけれど、そこじゃないところを書き換えたいときに
  • bound：簡単な有界性や大小関係を示せるタクティック
    • omegaが不要なほど自明な時に使ってすごいことをしていないことを明示。simpではうまくいかない時に使っている。大小関係を示すときはlinarithタクティックもあるけれど今回の記事では出番がなかった
  • clear：邪魔な仮定を消す（証明力は下がる。これはもう使わないということを明示できる）
    • 特にihn1 := ihn.leftを使わないことを明示している
  • match：場合分けにより証明する
    • casesでいいのだけれど、変数名をつけるために使っている。cases'なら変数名はつけられるのだけれど、Lean 4では非推奨らしいので
  • contradiction：仮定が矛盾していることを指摘し、爆発律により証明する

ここまでは、Lean 4の初心者向けに標準ライブラリの定理を説明してきましたが、新しいものが多数出てきたので、いちいち説明をすることはやめます。 calcで具体的に書いてある数式変形は、常識的に見ればいずれも“自明”であり理解可能であると思われるからです。

Eq.symm $ 等式定理だけは説明したほうがいいでしょうか。 これは、等式定理の左右を入れ替えることを意味します。

ちなみに、定理をどの引数で使用するかはすべて明示してありますが、実際には_などと書いておけば自動で推論してくれます。

B関数の二引数狭義単調増加性1

B関数に与える関数fが、厳密膨張的かつ狭義単調増加であるとき、次の性質が成り立ちます。

  • 任意のm・n・x・yに対し、m < xとn < yが成り立つとき、B_func f m nよりもB_func f x yの方が大きい（引数がそれぞれ大きいなら、大きい）

証明の方針は、xに対する帰納法で、その中では先ほど示した最右引数に対する性質を利用するというものです。 帰納法のステップでm < x+1に対して示すとき、m < xが成り立てば帰納法の仮定が、m = xならば最右引数に対する性質が、それぞれ使えます。

lemma B_func_monotonic_lemma2
   (f : Nat -> Nat) (hf1 : ∀x, x < f x) (hf2 : ∀x y, x < y → f x < f y)
  : ∀ m n x y, m < x ∧ n < y → B_func f m n < B_func f x y := by
  have lB2 x y := (B_func_monotonic_lemma1 f hf1 hf2 x y).right.left
  have lB3 x y := (B_func_monotonic_lemma1 f hf1 hf2 x y).right.right

  intro m n x y
  induction x with
  | zero => tauto
  | succ x ihx =>
      intro hc
      by_cases h : m = x
      · calc
          B_func f m n = B_func f x n     := by rw [h]
          _            < B_func f x y     := lB3 x n y hc.right
          _            < B_func f x (y+1) := lB3 x y (y+1) (show y < y+1 by simp)
          _            ≤ B_func f (x+1) y := lB2 x y
      · have h : m < x ∧ n < y := ⟨by omega, hc.right⟩
        calc
          B_func f m n < B_func f x y     := ihx h
          _            < B_func f x (y+1) := lB3 x y (y+1) (show y < y+1 by simp)
          _            ≤ B_func f (x+1) y := lB2 x y

B_func f x y < B_func f x (y+1) ≤ B_func f (x+1) yの部分が重複していて微妙です。 くくりだすほどでもないので、コピペになっています。

B関数の二引数狭義単調増加性2

上記で示した定理は、両方の引数が真に大きくなければ使えないので、微妙に不便です。 左の引数が同じであっても、最右引数に対する狭義単調増加性により結局示せるので、それを含めた定理を証明しましょう。

  • 任意のm・n・x・yに対し、m ≤ xとn < yが成り立つとき、B_func f m nよりもB_func f x yの方が大きい（左引数が「以上」かつ右引数が大きいなら、大きい）
lemma B_func_monotonic_lemma2'
  (f : Nat -> Nat) (hf1 : ∀x, x < f x) (hf2 : ∀x y, x < y → f x < f y)
  : ∀ m n x y, m ≤ x ∧ n < y → B_func f m n < B_func f x y := by
  intro m n x y
  by_cases h1 : m = x
  · rw [h1]
    intro h2
    exact (B_func_monotonic_lemma1 f hf1 hf2 x n).right.right y h2.right
  · intro h2
    have h1 : m < x := by omega
    exact (B_func_monotonic_lemma2 f hf1 hf2 m n x y) ⟨h1, h2.right⟩

B関数に3変数アッカーマン関数を入れると3変数アッカーマン関数になる

定義から明らかに、B_func (fun x => x + 1) x y = Ackermann2 x yであることがわかります。

Lean 4での証明（整理する前のもの。クリックして展開）

lemma example3 : B_func (fun x => x + 1) x y = Ackermann2 x y := by
  induction x generalizing y with
  | zero =>
      rw [B_func.eq_def]
      split <;> try contradiction
      simp [Ackermann2]
  | succ x ihx =>
      induction y with
      | zero =>
          rw [B_func.eq_def]
          split <;> try contradiction
          expose_names
          rw [show m = x from by omega]
          simp [Ackermann2]
          exact ihx
      | succ y ihy =>
          rw [B_func.eq_def]
          split <;> try contradiction
          expose_names
          rw [show m = x from by omega, show n = y from by omega]
          simp [Ackermann2]
          rw [ihy]
          exact ihx

※整理する前のコードであるため、split <;> try contradictionを使っていて長い。

△展開ここまで

S変換すると3変数アッカーマン関数が出てきます。

lemma example4 : B_func (fun x => x + 1) x x = Ackermann3 1 0 x := by
  calc
    B_func (fun x => x + 1) x x = Ackermann2 x x := example3
    _                           = Ackermann3 0 x x := by simp [Ackermann3zero_eq_Ackermann2]
    _                           = Ackermann3 1 0 x := by rw [Ackermann3]

lemma example5 : (S_transform (3, fun x => x + 1)) = (61, fun x => Ackermann3 1 0 x) := by
  simp [S_transform]
  simp [B_func]
  simp_all [example4]

さらにS変換をすると3変数アッカーマン関数程度の増大度を持つ関数が得られることが知られています。 ただし、増大度が同じでも微妙に（※巨大数の文脈での意味。実際には“ものすごく”）値が異なることがあるため、よく確認する必要があります。 とりあえずB_func (fun x => Ackermann2 x x) x y = Ackermann3 1 x yくらいかな？と思って式変形を続けると、実際にこれが示せるため、正確に等式が成り立つようです。

Lean 4での証明（整理する前のもの。クリックして展開）

lemma example6 : B_func (fun x => Ackermann3 1 0 x) x y = Ackermann3 1 x y := by
  induction x generalizing y with
  | zero =>
      rw [B_func.eq_def]
  | succ x ihx =>
      induction y with
      | zero =>
          rw [B_func.eq_def]
          split <;> try contradiction
          expose_names
          rw [show m = x from by omega]
          rw [ihx]
          rw [Ackermann3]
      | succ y ihy =>
          rw [B_func.eq_def]
          split <;> try contradiction
          expose_names
          rw [show m = x from by omega, show n = y from by omega]
          rw [ihy]
          rw [ihx]
          simp [Ackermann3]

※整理する前のコードであるため、split <;> try contradictionを使っていて長い。

△展開ここまで

ここまでの実験結果を3変数アッカーマン関数を用いて書き換えると、以下のようになります。

  • B_func (fun x => Ackermann3 0 0 x) x y = Ackermann3 0 x y
  • B_func (fun x => Ackermann3 1 0 x) x y = Ackermann3 1 x y

ここから類推すると、任意のqについて、B_func (fun x => Ackermann3 q 0 x) x y = Ackermann3 q x yが成り立ってもよさそうです。 これは実際に証明できます。 というか、証明（タクティック列）はB_func (fun x => Ackermann3 1 0 x) x y = Ackermann3 1 x yの証明の時と完全に同じです。 この証明では、最左引数が1であることは一切使わなかったからです。

Lean 4での証明（整理する前のもの。クリックして展開）

lemma example12 : B_func (fun x => Ackermann3 q 0 x) x y = Ackermann3 q x y := by
  -- example6と同じ
  induction x generalizing y with
  | zero =>
      rw [B_func.eq_def]
  | succ x ihx =>
      induction y with
      | zero =>
          rw [B_func.eq_def]
          split <;> try contradiction
          expose_names
          rw [show m = x from by omega]
          rw [ihx]
          rw [Ackermann3]
      | succ y ihy =>
          rw [B_func.eq_def]
          split <;> try contradiction
          expose_names
          rw [show m = x from by omega, show n = y from by omega]
          rw [ihy]
          rw [ihx]
          simp [Ackermann3]

※整理する前のコードであるため、split <;> try contradictionを使っていて長い。

△展開ここまで

結局、以下のようにまとめることができました。

lemma B_func_Ackermann3_lemma1  : B_func (fun x => Ackermann3 q 0 x) x y = Ackermann3 q x y := by
  induction x generalizing y with
  | zero => rw [B_func.eq_1]
  | succ x ihx =>
      induction y with
      | zero => rw [B_func.eq_2, Ackermann3]; exact ihx
      | succ y ihy => rw [B_func.eq_3, Ackermann3]; simpa [ihy] using ihx

B関数で3変数アッカーマン関数の最左引数を1増やせる

B関数による対角化は、3変数アッカーマン関数の最左引数を1増やす効果があります。

lemma B_func_Ackermann3_eq_lemma2
  : B_func (fun x => Ackermann3 q 0 x) x x = Ackermann3 (q+1) 0 x := by
  rw [B_func_Ackermann3_lemma1, Ackermann3]

2変数アッカーマン関数の性質の証明

B関数に後者関数を与えたものが2変数アッカーマン関数

2変数アッカーマン関数くらいであれば性質を直に証明できますが、せっかくなのでB関数の性質を使って一気に片付けることにしましょう。 そのためにはまず、2変数アッカーマン関数がB関数を用いて書き表せることを示します。

lemma Ackermann2_eq_B_func : Ackermann2 x y = B_func (fun x => x + 1) x y := by
  induction x generalizing y with
  | zero => rw [B_func.eq_1]; simp [Ackermann2]
  | succ x ihx =>
      induction y with
      | zero => rw [B_func.eq_2, Ackermann2]; exact ihx
      | succ y ihy => rw [B_func.eq_3, Ackermann2]; simpa [ihy] using ihx

2変数アッカーマン関数は厳密膨張的・左引数優位・狭義単調増加

瞬殺です。

lemma Ackermann2_monotonic1 : ∀ x y, (y < Ackermann2 x y) ∧ (Ackermann2 x (y+1) ≤ Ackermann2 (x+1) y) ∧ (∀ z > y, Ackermann2 x y < Ackermann2 x z) := by
  intro x y
  repeat rw [Ackermann2_eq_B_func]
  obtain ⟨hB1, hB2, hB3⟩ := B_func_monotonic_lemma1 (fun x => x + 1) (by simp) (by simp) x y
  refine ⟨hB1, hB2, ?_⟩
  · intro z hz
    rw [Ackermann2_eq_B_func]
    exact hB3 z hz

∀で束縛された変数を含む書き換えはできないのか、いったん仮定側に追い出す必要があるようです。 そのため、hB3がそのままでは使えなくて、証明が長くなってしまっています。 obtainは、分解して取り出すタクティックです。

調べたら、rwタクティックではだめでも、simpタクティックだといけるようです（rw: 同値変形 - Lean by Example）。 実際、simpa [Ackermann2_eq_B_func] using hB3でうまくいきました（simpaはsimpと同様に動作します）。 つまり結局、exact ⟨hA1, hA2, by simpa [Ackermann3zero_eq_Ackermann2] using hA3⟩の一行で証明できたようですね。 そもそも、最初からsimpを使っておけばそれも不要で、以下のように証明できました。

example : ∀ x y, (y < Ackermann2 x y) ∧ (Ackermann2 x (y+1) ≤ Ackermann2 (x+1) y) ∧ (∀ z > y, Ackermann2 x y < Ackermann2 x z) := by
  intro x y
  simp [Ackermann2_eq_B_func]
  exact B_func_monotonic_lemma1 (fun x => x + 1) (by simp) (by simp) x y

横長になりますが次の方法もありますね。

example : ∀ x y, (y < Ackermann2 x y) ∧ (Ackermann2 x (y+1) ≤ Ackermann2 (x+1) y) ∧ (∀ z > y, Ackermann2 x y < Ackermann2 x z) := by
  intro x y
  simpa [Ackermann2_eq_B_func] using B_func_monotonic_lemma1 (fun x => x + 1) (by simp) (by simp) x y

3変数アッカーマン関数の性質の証明

3変数アッカーマン関数は厳密膨張的・左引数優位・狭義単調増加

B関数の性質を使うことで、三重帰納法などを使わなくても証明できます。

lemma Ackermann3_monotonic1 x y z :
      (z < Ackermann3 x y z)
    ∧ (Ackermann3 x y (z+1) ≤ Ackermann3 x (y+1) z)
    ∧ (∀ w > z, Ackermann3 x y z < Ackermann3 x y w) := by
  induction x generalizing y z with
  | zero =>
      repeat rw [Ackermann3zero_eq_Ackermann2]
      obtain ⟨hA1, hA2, hA3⟩ := Ackermann2_monotonic1 y z
      refine ⟨hA1, hA2, ?_⟩
      · intro w hw
        rw [Ackermann3zero_eq_Ackermann2]
        exact hA3 w hw
  | succ x ihx =>
      have ihx1 y z := (ihx y z).left
      have ihx3 y z := (ihx y z).right.right
      clear ihx

      have ihx4 y z w v : y ≤ w ∧ z < v → Ackermann3 x y z < Ackermann3 x w v := by
        repeat rw [← B_func_Ackermann3_lemma1]
        exact B_func_monotonic_lemma2' _ (ihx1 0) (ihx3 0) y z w v

      repeat rw [← B_func_Ackermann3_lemma1]

      set F := fun z => Ackermann3 (x+1) 0 z with hF
      have F_inc w : w < F w := by simpa [hF, Ackermann3] using ihx1 w w
      have F_monoto w v (h : w < v) : F w < F v := by
        simpa [hF, Ackermann3] using ihx4 w w v v ⟨show w ≤ v by omega, h⟩

      obtain ⟨hB1, hB2, hB3⟩ := B_func_monotonic_lemma1 F F_inc F_monoto y z
      refine ⟨hB1, hB2, ?_⟩
      · intro w hw
        rw [← B_func_Ackermann3_lemma1]
        exact hB3 w hw

実際のところ、最初はB関数の性質を使わずに直に証明していました。 B関数の性質を使った証明と見比べると、（split <;> try contradictionを使っていることを抜きにしても）非常に長いものになっていました。 これは、3変数アッカーマン関数という具体的な関数であるがゆえに、なまじ具体的に計算できてしまって、遠回りな変形を行ってしまっていたことが原因です。 逆接的ですが、抽象的なB関数の方が、証明に使える式変形が限られているため、却ってコンパクトな証明になったのです。 ただし、一か所だけは3変数アッカーマン関数の証明の方が短い部分があました。 先ほど示したB関数の性質の証明は、その技法を取り入れて、より簡潔なものにしたものです。

B関数の性質を使わない直証明（整理する前のもの。クリックして展開）

lemma Ackermann3_monotonic : ∀ x y z,
      (z < Ackermann3 x y z)
    ∧ (Ackermann3 x y (z+1) ≤ Ackermann3 x (y+1) z)
    ∧ (∀ w > z, Ackermann3 x y z < Ackermann3 x y w) := by

  intro x y z

  induction x generalizing y z with
  | zero =>
      refine ⟨?_, ?_, ?_⟩
      · rw [Ackermann3zero_eq_Ackermann2]
        exact (Ackermann2_monotonic y z).left
      · repeat rw [Ackermann3zero_eq_Ackermann2]
        exact (Ackermann2_monotonic y z).right.left
      · intro w hw
        repeat rw [Ackermann3zero_eq_Ackermann2]
        exact (Ackermann2_monotonic y z).right.right w hw
  | succ x ihx =>
      have ihx1 y z := (ihx y z).left
      have ihx2 y z := (ihx y z).right.left
      have ihx3 y z := (ihx y z).right.right
      clear ihx

      -- 累積帰納法バージョン
      have ihx2' y z : Ackermann3 x 0 (y+z) ≤ Ackermann3 x y z := by
        induction y generalizing z with
        | zero => simp
        | succ y ihy =>
            calc
               Ackermann3 x 0 (y+1+z) = Ackermann3 x 0 (y+z+1) := by group
               _                      ≤ Ackermann3 x y (z+1) := ihy (z+1)
               _                      ≤ Ackermann3 x (y+1) z := ihx2 y z
      have ihx4 y z w v : y ≤ w ∧ z < v → Ackermann3 x y z < Ackermann3 x w v := by
        induction w generalizing v with
        | zero =>
            intro h
            rw [show y = 0 from by bound]
            exact ihx3 0 z v h.right
        | succ w ihw =>
            intro h1
            by_cases h2 : y = w+1
            · rw [h2]
              exact ihx3 (w+1) z v h1.right
            · have h2 : y ≤ w := by omega
              calc
                Ackermann3 x y z < Ackermann3 x w (v+1) := ihw (v+1) ⟨h2, by omega⟩
                _                ≤ Ackermann3 x (w+1) v := ihx2 w v

      induction y generalizing z with
      | zero =>
          induction z with
          | zero =>
            refine ⟨?_, ?_, ?_⟩
            · simp [Ackermann3]
              exact ihx1 0 0
            · simp [Ackermann3]
            · intro w hw
              exact Ackermann3_is_increase_and_monotonic.right 0 w hw
          | succ z ihz =>
              have ihz' : (∀ y z w, z ≤ w → Ackermann3 x y z ≤ Ackermann3 x y w) := by
                intro y z w
                by_cases h : z = w
                · rw [h]; tauto
                · intro
                  exact Nat.le_of_succ_le $ ihx3 y z w (by omega)

              obtain ⟨ihz1, ihz2, ihz3⟩ := ihz
              refine ⟨?_, ?_, ?_⟩
              · calc
                  z+1 < Ackermann3 x z (z+1) := ihx1 z (z+1)
                  _   < Ackermann3 x z (Ackermann3 x z (z+1)) := ihx3 z (z+1) (Ackermann3 x z (z+1)) (ihx1 z (z+1))
                  _   ≤ Ackermann3 x z (Ackermann3 x (z+1) z) := ihz' z (Ackermann3 x z (z+1)) (Ackermann3 x (z+1) z) $ ihx2 z z
                  _   = Ackermann3 x (z+1) (z+1) := by simp [Ackermann3]
                  _   = Ackermann3 (x+1) 0 (z+1) := by simp [Ackermann3]
              · have : z+1+1 < Ackermann3 (x+1) 1 z := by
                  calc
                    z+1+1 < Ackermann3 x z (z+1+1) := ihx1 z (z+1+1)
                    _     ≤ Ackermann3 x (z+1) (z+1) := ihx2 z (z+1)
                    _     = Ackermann3 (x+1) 0 (z+1) := by simp [Ackermann3]
                    _     ≤ Ackermann3 (x+1) 1 z := ihz2
                have : Ackermann3 (x+1) 0 (z+1+1) < Ackermann3 (x+1) 1 (z+1) := by
                  calc
                    Ackermann3 (x+1) 0 (z+1+1) = Ackermann3 x (z+1+1) (z+1+1) := by simp [Ackermann3]
                    _                          < Ackermann3 x (Ackermann3 (x+1) 1 z) (Ackermann3 (x+1) 1 z) := ihx4 _ _ _ _ (by omega)
                    _                          = Ackermann3 (x+1) 0 (Ackermann3 (x+1) 1 z) := by simp [Ackermann3]
                    _                          = Ackermann3 (x+1) 1 (z+1) := by simp [Ackermann3]
                exact Nat.le_of_succ_le this
              · intro w hw
                exact Ackermann3_is_increase_and_monotonic.right (z+1) w hw
      | succ y ihy =>
          have ihy1 z := (ihy z).left
          have ihy2 z := (ihy z).right.left
          have ihy3 z := (ihy z).right.right
          clear ihy

          induction z with
          | zero =>
              refine ⟨?_, ?_, ?_⟩
              · simp [Ackermann3]
                calc
                  0 < 1 := by simp
                  _ < Ackermann3 (x+1) y 1 := ihy1 1
              · simp [Ackermann3]
              · intro w hw
                calc
                  Ackermann3 (x+1) (y+1) 0 = Ackermann3 (x+1) y 1 := by simp [Ackermann3]
                  _                        < Ackermann3 (x+1) y (w+1) := ihy3 1 (w+1) (by omega)
                  _                        ≤ Ackermann3 (x+1) (y+1) w := ihy2 w
          | succ z ihz =>
              obtain ⟨ihz1, ihz2, ihz3⟩ := ihz
              refine ⟨?_, ?_, ?_⟩
              · have : z+1 < Ackermann3 (x+1) (y+1) z := by
                  calc
                    z+1 < Ackermann3 (x+1) y (z+1) := ihy1 (z+1)
                    _   ≤ Ackermann3 (x+1) (y+1) z := ihy2 z

                calc
                  z+1 < Ackermann3 (x+1) y (z+1) := ihy1 (z+1)
                  _   < Ackermann3 (x+1) y (Ackermann3 (x+1) (y+1) z) := ihy3 (z+1) _ this
                  _   = Ackermann3 (x+1) (y+1) (z+1) := by simp [Ackermann3]
              · have h1 : Ackermann3 (x+1) (y+1) (z+1) < (Ackermann3 (x+1) (y+1+1) z) + 1 := by
                  calc
                    Ackermann3 (x+1) (y+1) (z+1) ≤ Ackermann3 (x+1) (y+1+1) z := ihz2
                    _                            < (Ackermann3 (x+1) (y+1+1) z) + 1 := by simp
                have h2 : Ackermann3 (x+1) (y+1+1) (z+1) = Ackermann3 (x+1) (y+1) (Ackermann3 (x+1) (y+1+1) z) := by rw [Ackermann3.eq_def]
                have h3 : Ackermann3 (x+1) (y+1) (z+1+1) < Ackermann3 (x+1) (y+1+1) (z+1) := by
                  calc
                    Ackermann3 (x+1) (y+1) (z+1+1) = Ackermann3 (x+1) y (Ackermann3 (x+1) (y+1) (z+1)) := by repeat rw [Ackermann3]
                    _                              < Ackermann3 (x+1) y ((Ackermann3 (x+1) (y+1+1) z) + 1) := ihy3 (Ackermann3 (x+1) (y+1) (z+1)) ((Ackermann3 (x+1) (y+1+1) z)+1) h1
                    _                              ≤ Ackermann3 (x+1) (y+1) (Ackermann3 (x+1) (y+1+1) z) := ihy2 (Ackermann3 (x+1) (y+1+1) z)
                    _                              = Ackermann3 (x+1) (y+1+1) (z+1) := Eq.symm h2
                exact Nat.le_of_succ_le h3
              · intro w
                intro hw
                simp [Ackermann3]
                nth_rewrite 3 [Ackermann3.eq_def]
                split <;> try contradiction
                expose_names; rw [show b = y from by omega]
                exact ihy3 (Ackermann3 (x+1) (y+1) z) (Ackermann3 (x+1) (y+1) a) (ihz3 a (by omega))

※整理する前のコードであるため、split <;> try contradictionを使っていて長い。遠回りでもある。

△展開ここまで

全域性の証明について

3変数アッカーマン関数は、巨大数論において、3重再帰関数であるとされています（83ページ目。多重再帰関数 | 巨大数研究 Wiki | Fandomも参考になる）。 また、上記の直証明では3重にネストした帰納法が使われています。 そのため、2変数アッカーマン関数の全域性が \mathrm{I\Sigma_2}を使わないと証明できなかったことから類推して、3変数アッカーマン関数の全域性は \mathrm{I\Sigma_3}を使わないと証明できないのかな？と思うかもしれませんが、これは誤りです。 3変数になるにあたって新しく増えた対角化も \mathrm{I\Sigma_2}で証明可能だからです。

Lean 4のような定義を導入する方式で証明していると混乱しますが、そもそも本来の \mathrm{I\Sigma_1}での原始再帰関数の全域性の証明は、以下のようなものです。

  1. \Delta_0定義可能なエンコーディングで関数の計算トレース（再帰呼び出しで引数がどのように変化したかの列）をエンコードする
  2. 計算トレースがあっていることも \Delta_0で確認する（再帰引数からわかる長さの上限があるため、有界全称量化で書ける）
  3. 関数の等式関係を示す \Delta_0論理式（例えば、 \mathrm{Exp}(a, b, x)と書いて a ^ b = xを意味するとする）を構成する
  4. 特定の入力に対して関数が停止することを意味する \Sigma_1論理式を構成する（上記の例なら \exists x. \mathrm{Exp}(a, b, x)）
  5. その \Sigma_1論理式に帰納法（ \mathrm{I\Sigma_1}）を適用して、全域性を意味する \Pi_2論理式を得る

\mathrm{I\Sigma_2}を使わないといけない全域性の証明の場合、2.の計算トレースがあっていることの確認が \Pi_1論理式になり、4.の特定の入力に対して関数が停止することを意味する論理式が \Sigma_2論理式になって、 \mathrm{I\Sigma_2}が必要になるようです。

ここに出てくる \mathrm{I\Sigma_1}の1だとか \mathrm{I\Sigma_2}の2とかは、Lean 4で書かれた証明のネスト数とは全く無関係です。 \mathrm{I\Sigma_2}が必要か否かは、1.～3.がうまい \Delta_0論理式で書けるか否かにかかっています。 \Delta_0論理式で書けるかは要するに有界量化で書けるか、つまり上限が指定できるかが重要であり、上限の有無にかかわらず帰納法が使えるLean 4で書かれた証明からすぐにそれを読み解くことはできません。

最左引数に対しても厳密膨張的

lemma Ackermann3_monotonic_3rd : ∀ x y z w, x < w → (y≠0 ∨ z≠0) → Ackermann3 x y z < Ackermann3 w y zを、wに対する帰納法で示すことができます。 帰納法のステップでは、lemma Ackermann3_monotonic_3rd_ih : ∀ x y z, (y≠0 ∨ z≠0) → Ackermann3 x y z < Ackermann3 (x+1) y zの証明が必要になります。

lemma Ackermann3_monotonic_3rdは少なくとも今回は使わなかったので、証明は畳んでおきます。

lemma Ackermann3_monotonic_3rdの証明（整理する前のもの。クリックして展開）

lemma Ackermann3_monotonic_3rd :
  ∀ x y z w, x < w → (y≠0 ∨ z≠0) → Ackermann3 x y z < Ackermann3 w y z := by
  intro x y z w
  induction w with
  | zero => tauto
  | succ w ihw =>
      intro
      by_cases h : w = x
      · rw [h]
        exact Ackermann3_monotonic_3rd_ih x y z
      · have h : x < w := by omega
        intro hc
        calc
          Ackermann3 x y z < Ackermann3 w y z := ihw h hc
          _                < Ackermann3 (w+1) y z := Ackermann3_monotonic_3rd_ih w y z hc

△展開ここまで 

lemma Ackermann3_monotonic_3rd_ih_ih
  (x y z : Nat)
  (ihy : ∀ (z : ℕ), y ≠ 0 ∨ z ≠ 0 → Ackermann3 x y z < Ackermann3 (x+1) y z)
  (ihz : y + 1 ≠ 0 ∨ z ≠ 0 → Ackermann3 x (y+1) z < Ackermann3 (x+1) (y+1) z)
  : Ackermann3 x (y+1) (z+1) < Ackermann3 (x+1) (y+1) (z+1) := by
  calc
    Ackermann3 x (y+1) (z+1)
      = Ackermann3 x y (Ackermann3 x (y+1) z)         := by simp [Ackermann3]
    _ < Ackermann3 x y (Ackermann3 (x+1) (y+1) z)     := (Ackermann3_monotonic1 x y (Ackermann3 x (y+1) z)).right.right
                                                           (Ackermann3 (x+1) (y+1) z) $ ihz (by simp)
    _ < Ackermann3 (x+1) y (Ackermann3 (x+1) (y+1) z) := ihy (Ackermann3 (x+1) (y+1) z) (by omega)
    _ = Ackermann3 (x+1) (y+1) (z+1)                  := by simp [Ackermann3]

lemma Ackermann3_monotonic_3rd_ih :
  ∀ x y z, (y ≠ 0 ∨ z ≠ 0) → Ackermann3 x y z < Ackermann3 (x+1) y z := by
  intro x y z hnz
  induction x generalizing y z with
  | zero =>
      induction y generalizing z with
      | zero =>
          match z with
          | 0 => contradiction
          | n+1 =>
              calc
                Ackermann3 0 0 (n+1)
                  = n+1+1                    := Ackermann3.eq_1 (n+1)
                _ < Ackermann3 0 n (n+1+1)   := (Ackermann3_monotonic1 0 n (n+1+1)).left
                _ ≤ Ackermann3 0 (n+1) (n+1) := (Ackermann3_monotonic1 0 n (n+1)).right.left
                _ = Ackermann3 1 0 (n+1)     := Eq.symm $ Ackermann3.eq_2 (n+1) 0
      | succ y ihy =>
          induction z with
          | zero => rw [Ackermann3.eq_3, Ackermann3.eq_3]; exact ihy 1 (by simp)
          | succ z ihz => exact Ackermann3_monotonic_3rd_ih_ih 0 y z ihy ihz
  | succ x ihx =>
      induction y generalizing z with
      | zero => rw [Ackermann3.eq_2, Ackermann3.eq_2]; exact ihx z z (by omega)
      | succ y ihy =>
          induction z with
          | zero => simp [Ackermann3.eq_3]; exact ihy 1 (by simp)
          | succ z ihz => exact Ackermann3_monotonic_3rd_ih_ih (x+1) y z ihy ihz

なんだか同じ証明が二回出てきたので、補題に切り出しました。 トップレベルにあることでインデントが減ってcalcが見やすくなって良いですね。 それでもはみ出していますが……。

本題：ふぃっしゅ数バージョン1のSS変換

ふぃっしゅ数バージョン1 | 巨大数研究 Wiki | Fandomに載っている、次の言明を証明します。

SS変換の1回目はS変換4回なので、S変換2回程度の A(2,3,3) に相当する A(1,0,1,1) よりは大きく、

S変換で3変数アッカーマン関数の最左引数が1増える

B関数を適用すると3変数アッカーマン関数の最左引数が1増えることを先ほど示しました。 したがって、S変換で得られる自然数と関数のペアにおいて、関数側がそうなることはすぐわかります。 自然数側は、それを適用したものなので、やはり同様に最左引数が1増えることになります。

lemma S_transform_Ackermann3_eq_lemma : (S_transform (m, fun x => Ackermann3 q 0 x)) = (Ackermann3 (q+1) 0 m, (fun x => Ackermann3 (q+1) 0 x)) := by
  simp [S_transform, B_func_Ackermann3_eq_lemma2]

ふぃっしゅ数バージョン1の1回目のSS変換結果

S変換を4回することになります。

lemma F1_first_iteration_eq_lemma : (Repeat S_transform 4 (3, fun x => x + 1)) = ((Ackermann3 4 0 $ Ackermann3 3 0 $ Ackermann3 2 0 $ Ackermann3 1 0 $ 3), (fun x => Ackermann3 4 0 x)) := by
  simp [Repeat]
  rw [show (fun x => x + 1) = (fun x => Ackermann3 0 0 x) by funext x; simp [Ackermann3]]
  rw [S_transform_Ackermann3_eq_lemma]
  rw [S_transform_Ackermann3_eq_lemma]
  rw [S_transform_Ackermann3_eq_lemma]
  rw [S_transform_Ackermann3_eq_lemma]

repeat rwとしてもよかったのですが、4回やるということを明示してみました。

funextタクティックは、関数と関数の等価性を、引数が同じであれば返り値も一致することを以って示す（ために適当な引数を仮定に導入する）タクティックです。 ここでは、後者関数を3変数アッカーマン関数を用いた表現に置き換えることで、ここまでに示した補題を適用できる形に変形しています。

また、simpが証明の最後以外に現れています。 simpは実際には、「証明を作ってくれる」タクティックではなく、「証明したい命題を簡略化」したうえで「それが自明な形になっていれば、それを以って証明とする」オプショナルな機能が付いたタクティックです（rwと同様）。

本題

次のように証明できます。

theorem F1_first_iteration : Ackermann4 1 0 1 1 < (SS_transform ((3, fun x => x + 1), S_transform)).fst.fst := by
  rw [SS_transform]
  rw [F1_first_iteration_eq_lemma]
  calc
    Ackermann4 1 0 1 1
      = Ackermann4 1 0 0 (Ackermann4 1 0 1 0) := Ackermann4.eq_5 1 0 0 0
    _ = Ackermann4 1 0 0 (Ackermann4 1 0 0 1) := by rw [Ackermann4.eq_4]
    _ = Ackermann4 1 0 0 (Ackermann4 0 1 0 1) := by rw [Ackermann4.eq_2 1]
    _ = Ackermann4 1 0 0 (Ackermann4 0 0 1 1) := by rw [Ackermann4.eq_3]
    _ = Ackermann4 1 0 0 (Ackermann4 0 0 0 (Ackermann4 0 0 1 0)) := by rw [Ackermann4.eq_5]
    _ = Ackermann4 1 0 0 (Ackermann4 0 0 0 (Ackermann4 0 0 0 1)) := by rw [Ackermann4.eq_4]
    _ = Ackermann4 1 0 0 (Ackermann4 0 0 0 2) := by rw [Ackermann4.eq_1, Ackermann4.eq_1]
    _ = Ackermann4 1 0 0 3 := by rw [Ackermann4.eq_1]
    _ = Ackermann4 0 3 0 3 := Ackermann4.eq_2 3 0
    _ = Ackermann3 3 0 3 := Ackermann4zero_eq_Ackermann3
    _ < Ackermann3 4 0 3 := Ackermann3_monotonic_3rd_ih 3 0 3 (by omega)
    _ < Ackermann3 4 0 (Ackermann3 3 0 3) := (Ackermann3_monotonic1 4 0 3).right.right _ $
                                              (Ackermann3_monotonic1 3 0 3).left
    _ < Ackermann3 4 0 (Ackermann3 3 0 (Ackermann3 2 0 3))
             := (Ackermann3_monotonic1 4 0 _).right.right _ $
                (Ackermann3_monotonic1 3 0 3).right.right _ $
                (Ackermann3_monotonic1 2 0 3).left
    _ < Ackermann3 4 0 (Ackermann3 3 0 (Ackermann3 2 0 (Ackermann3 1 0 3)))
             := (Ackermann3_monotonic1 4 0 _).right.right _ $
                (Ackermann3_monotonic1 3 0 _).right.right _ $
                (Ackermann3_monotonic1 2 0 3).right.right _ $
                (Ackermann3_monotonic1 1 0 3).left

最後の方の式変形は、3変数アッカーマン関数を適用すると大きくなるという定理をベースに書き換え、その外側が大きくなることについては3変数アッカーマン関数は最右引数が大きければ大きいという定理を再帰的に使うことで行っています。 関数呼び出しと同じ構造の証明が必要になるのはおもしろいですね。

まとめ

ふぃっしゅ数バージョン1は、SS変換を63回繰り返して得られる自然数です。 今回は、SS変換を1回だけして得られる自然数について、それが多変数アッカーマン関数A(1,0,1,1)=A(2,3,3)よりも大きいことを、Lean 4を用いて形式的に証明しました。

けっこう複雑な証明だったので、試行錯誤や便利なタクティックをいやでも覚えることとなりました。 実戦（？）を通じてLean 4の力がついてきた気がします。

*1:非数学的な帰納法がよく使われている印象があります。

*2:https://www.math.mi.i.nagoya-u.ac.jp/~kihara/pdf/teach/logic2017spring.pdfに載っていた名称です。GPT-5は切り捨て引き算がおすすめだというけれど、一回も見たことがないです。おそらく、truncated subtractionを直訳しているのだと思います。Google検索した時のAI概要は正しく理解していそうなものが出ますが……。

*3:巨大数同士の大小関係をよりタイトに評価できる的な意味で

*4:この記事では証明していませんが

*5:巨大数論 第二版 89ページ



以上の内容はhttps://lpha-z.hatenablog.com/entry/2025/08/10/231500より取得しました。
このページはhttp://font.textar.tv/のウェブフォントを使用してます
不具合報告/要望等はこちらへお願いします。
モバイルやる夫Viewer Ver0.14