1+1=と聞かれたら？

集合写真にて

突然ですが集合写真を撮る事になりました。一枚目はキリッとした表情でパシャリ。二枚目は朗らかな笑顔で撮ることになりました。

「それじゃあ撮ります～！　1+1=？」

これに皆さんなら何と応・えますか？

おそらく大半の人はこう答・えるでしょう。

「それはどの数学体系で？」

冗談です。こんな事を言ったら空気を読まない奴と思われてしまいます。普通の人は1+1と聞かれたら素直に以下のように答えるでしょう。

「ペアノの公理を使ってまずは自然数を定義しよう」

1+1という問いかけに答えるためには、まず自然数とは何かを考える必要があります。

小学校までは「物の個数」のような曖昧な物として教わりますが、このような教え方では万が一ヒトとは物事の捉え方が違う宇宙人と出会った時に通じないかもしれません。例えばこんな事を言われるかもしれません。

「リンゴが一個ある？　でもパラレルワールドではそこに倍の量2個のリンゴがあるよ？　他のパラレルワールドだとそこにみかんがあるよ？　もう一度聞くね、一個ってどういう事？」

この宇宙人はパラレルワールドも同時に観測しているみたいですね！　そんな彼らにとってはリンゴが一個と言われてもぴんと来ないようです。そこで、宇宙人にもきちんと伝わるように、厳密に自然数を定義したいです。

そこで考え出されたのが ペアノの公理 です。公理という名前の通り、これは証明せずに用いる事が出来る 前提条件 のようなものです。これによると自然数(ここでは0を含む)というものが以下のように定義されています。

1. まず自然数には $0$ という値がある
2. 全ての自然数にはその次の自然数が存在する
   これにより0の次に1、その次に2、その次に……というように、一種の数学的帰納法のように自然数を求める事が出来ます。ただしこれだけでは不十分で幾つかの追加項目があります。
   この次を求める操作を、以下では $succ(n)$ という関数とします
3. $0$ の前には自然数が無い
4. 異なる自然数の次の数が同じ物となる事は無い
   要するに「ループは許しませんよ、0から真っ直ぐ次へ次へと続いて行くよ」という意味です。
5. 0およびその次、その次、……を全部列挙したもの、それが自然数全てである
   5番目はホントはもう少し複雑ですが、ここでは簡略化しています。

「次に足し算を定義しよう（ついでに掛け算も）」

自然数とは何かを定義できたので、次は足し算と掛け算という関数を定義しましょう。

足し算の定義(数学バージョン)

ペアノの公理で定義された自然数について、足し算という演算子は以下のように定義されます。

$n+0=n$
$n+succ(m)=succ(n+m)$

です。

ちょっとよく分からないですね。ではこれをPythonコードにして実際に実行してみましょう！

Pythonで足し算を定義しよう

add(m, n) を以下のように定義し、例示のprint文を実行してみましょう！

def add(a, b):
    if b == '0':
        return a
    else:
        return 'succ(' + add(a, b[5:-1]) + ')'

# example usage
print(add('0', '0'))
print(add('succ(0)', '0'))
print(add('succ(0)', 'succ(0)'))

ちょっと難しいですね。例を1つずつ見ていきましょう。

まずは $0+0$ に相当するadd('0', '0')の挙動を。
これはb == '0'なのでreturn aとなり、戻り値は'0'です。

次に $1+0$ に相当するadd('succ(0)', '0')の挙動を。
これはb == '0'なのでreturn aとなり、戻り値は'succ(0)'です。

次に $1+1$ に相当するadd('succ(0)', 'succ(0)')の挙動を。
これはelseですね。ここでb[5:-1]は「bの前5文字と後1文字を消す」という意味なので
戻り値は'succ('+add(a, '0')+)です。
再帰的にadd関数呼び出され、結果的に戻り値はsucc(succ(0))となります。
「0の次の次」という意味――即ち2です。

このように、自然数の足し算は再帰関数によって定義されているのです。

掛け算の定義

ちなみに、掛け算という演算子は以下のように定義されます。

$n\times 0=0$
$n\times succ(m)=(n \times m) + n$

です。これをPythonコードにするとこうなります。

def mul(a, b):
    if b == '0':
        return '0'
    else:
        return mul(a, b[5:-1]) + '+' + a

# example usage
print(mul('succ(0)', '0'))
print(mul('succ(0)', 'succ(0)'))
print(mul('succ(0)', 'succ(succ(0))'))

出力結果は次のようになります

0
0+succ(0)
0+succ(0)+succ(0)

このように、掛け算とは再帰関数を使って連続した足し算に展開する操作なのです。

最後に1と2を定義しよう。

これは簡単です。以下のように定義可能です。
$1=succ(0)$
$2=succ(1)=succ(succ(0))$

「以上より1+1=2です」（満面の笑顔）

パシャ！！

最高の笑顔が撮れました。やはり「1+1=?」と尋ねると最高の笑顔が撮れるのですね。

もっと証明したい！　そうだ、Leanを使おう！

証明アシスタントLean

現在「コンピュータに証明を手伝って貰おう」という考え方が広まりつつあります。それにはLLMのような曖昧な物ではなく「確実に論理的な検証を行う特殊なシステム」が必要です。これを証明アシスタントと呼びます。

数ある証明アシスタントの中でも最も広く使われている物の1つが「Lean」です。この言語は普通のプログラミング言語としても使えますが、同時に証明アシスタントとしての機能も備えた優秀な原語です。

Leanのインストール

VSCodeのExtensions(拡張機能)からLean4を検索してダウンロードします。注意したいのはLean3などの旧バージョンも検索に引っかかる事です。ここでは最新バージョンであるLean4を使います。

Lean内で自然数を定義。

ひょっとしてシンタックスハイライト出来ていないかも？　取り敢えずコードは次のようになっています。

inductive N where
  | zero : N
  | succ : N → N
  deriving Repr

namespace N

-- Define addition (add function) and assign it

def add (m n : N) : N := match n with
| zero => m
| succ n' => succ (add m n')

instance : Add N where
  add := add

-- Define multiplication (mul function) and assign it

def mul (m n : N) : N := match n with
| zero => zero
| succ n' => mul m n' + m

instance : Mul N where
  mul := mul

end N

先ほどまで取り扱っていたペアノの公理をプログラミング言語っぽく書いた感じです。1つずつ解説していきます。

まずは自然数の定義から。

inductive N where
  | zero : N
  | succ : N → N
  deriving Repr

自然数とはzeroとsucc()関数からなる、という意味です。

「自然数Nについて述べます」と宣言

namespace N
-- 中略
end N

namespaceからendまでの間で自然数Nについての演算を述べます。

なお、-- から始まる行はコメントです。無視して大丈夫です。

足し算関数addの定義

def add (m n : N) : N := match n with
| zero => m
| succ n' => succ (add m n')

参考：数学的表記
$n+0=n$
$n+succ(m)=succ(n+m)$

数学的表記とよく似ていますね！　nとmが入れ替わっているのはただのミスです。（ごめんなさい）

プラス記号とadd関数を結びつける

instance : Add N where
  add := add

こう書くとa*bがadd a bに変換されるようになります。

掛け算も同様に

def mul (m n : N) : N := match n with
| zero => zero
| succ n' => mul m n' + m

instance : Mul N where
  mul := mul

参考：数学的表記
$n\times 0=0$
$n\times succ(m)=(n \times m) + n$

これにてLeanのセットアップは完了です。次回はLeanを使って色々な定理を証明していきたいと思います。

ではでは、しーゆー！