Lingua Universalisを求めて

御言葉を証する科学の探求

私が主の御為に, そして私の隣人の為に是非とも成し遂げたいと願っていることはいくつかありますが, その中でも特に, 科学を正すということをしたいと切に願っています. 正すというのはつまり, 御言葉を正しく証できるようなものへと昇華させるということです. そんなことができるのかと言えば, 出来るはずです. というより, できない方がおかしいのです. 実際, 現代科学をもってしても未解決の問題は山のようにあり, それらはなぜ未解決であるのかと言えば, 科学の側が, 自分たちの古い価値観や先入観に縛られたまま世界を観察し続けた結果, 考慮すべき要素を考慮せず, 考慮せずとも良い要素を考慮して理論を構築しているからなのです.

観察とは本質的に損失を伴う(Observation is inherently lossy.)とは, システム論と呼ばれる学問で言われることですが, この教訓は自然科学全体に当てはまります. すなわち, 現代科学が神様の存在を証できず, 聖書を証できず, 御言葉を証できず, 神様が遣わされた方を証できないのは,

• 現代科学を構築する人々が真に見るべきものを見ておらず, 代わりに見なくても良いものばかりを見続け,
• 更には, 彼らが世界の有様を記述するために用いる言語が, この世界の真の姿を書き表すには不適切なものである

からなのです. 私が認識するこれらの問題について, 前者は既に解決策があると私たちは知っています. 神様が今, この複雑で混乱極まるこの社会を生きる私たちに述べ伝えてくださる新しい福音, RAPTブログ有料記事 でRAPTさんが述べ伝えてくださる御言葉に従うならば, 我々はどこを見て, 何をすべきか全て分かるようになります. 無神論者は神を無視するが故に, 本質的にこの世界を正しく捉え得ないですが, 我々は正しい道を知らされています.

では, 後者についてはどうかと言えば, ここが, 私が主の栄光の為に, そしてRAPTさんに従い神様を愛する神の民である方々の為に成し遂げてたいと願っていることなのです. すなわち, 自然科学を正すために, この世界の有様を造られた通りに記述する言葉を, 私は見出したいのです.

随分と大きくでたと思われてしまうでしょうが, 私はこの事について1年以上主に祈り求めており, 今では私が何をすべきかということが大体分かっています. 一言で言ってしまえば, 解放系の数理, あらゆるエージェント, あらゆる事物が"相互作用"する有様を厳密に記述する為の新しい数学を見出せば良いのです. これについて詳しく説明させてください.

論理, 計算, 圏: 3人の証人

旧約聖書にはこのような記述があります.

いかなる犯罪であれ, およそ人の犯す罪について, 一人の証人によって立証されることはない. 二人ないし三人の証人によって, その事は立証されなければならない.

申命記 19:15

20世紀の論理学と計算機科学の大きな発展により, 地球上に暮らす人類が今現在計算の数学的モデルとして知っている型付ラムダ計算と, 直観主義論理と呼ばれる論理体系と, デカルト閉圏と呼ばれる数学的構造の間に, カリー=ハワード同型対応と呼ばれる同型対応があることが, 1970年代後半に見出されました.

これらの数学的構造の間の同型対応とはつまり, 型付ラムダ計算と, 直観主義論理と, デカルト閉圏という3つの異なる数学的構造が, ある一つの同じ数学的構造を異なる言葉で表現しているという意味だと言えます. この同型対応によって, 計算機上で数学を厳密に行えるようになったり, また圏論という抽象的な学問の計算機科学, つまり応用数学への有効性が積極的に研究されるようになりました. 私もまた, CoqやIdrisと呼ばれるプログラミング言語を用いて, この同型対応を利用したプログラミングを沢山したことがあります.

それでは, このカリーハワード同型対応がどのような数学的構造を言い表しているのかと言えば, 言わば, “閉鎖系の数理"であると, 私は考えています. ここで, 閉鎖系というのは熱力学での専門用語を指すのではなく, 単に, 外界と相互作用をしないという意味だと考えていただきたいです. 外界と相互作用しないというのは, データの流れが一方向であるということです. もっと言えば, “閉鎖系の数理"とは, 一度入力が与えられたら, その入力に対する計算結果があらかじめ決定論的に分かるような計算の仕組みについての数学ということです. これをどうして"閉鎖系の数理"と呼びたいのか, そしてそれが何を意味しているのかについては, 次回以降続けて書いていきたいと思います.