こんにちは．茨城大学大学院M1の福留です．
この記事は茨大 Advent Calendar 2020 19日目の記事で，現在は12/23です．大遅刻申し訳ない…
この記事では，情報工学科2年の専門科目で習った「数理論理学」という分野と，情報科学への応用について簡単に書こうと思います．
たとえば「明日雨が降るならば運動会は中止である」という言明や，「図書館は水戸にあり，かつ日立にもある」という言明は，「AならばB」「AかつB」という論理構造をしています．このような論理構造(命題)は，数学的な証明の上で基本となる構造です．
このような論理構造そのものを数学的に扱う分野が「数理論理学」ないし「数学基礎論」とよばれる分野です．数学の論理をさらに数学的に扱うことで，数学の証明そのものの"正しさ"を研究したいというのがこの分野のモチベーションです．
数学では通常，ある仮定を，認められた方法を用いて変形し，結論を導くことで証明を行います．たとえば
A: 今日が火曜日なら，私は働きに行く． B: 今日は火曜日だ． C: だから，私は働きに行く．
という言明について考えてみます．みなさんもお気づきの通り，これは三段論法を用いて導出できます．もうちょっと分解すると，
P:今日は火曜日である Q:私は働きに行く A:P⇒Q B:P C:Q
と書くことができます．さて，Cの導出過程を，上が仮定，下が結論の図で表すならば
P⇒Q P —————— (三段論法) Q
とかけます．このような証明の流れを表す図を証明木といいます．2つの仮定「P⇒Q」と「P」，そして三段論法という認められたルールを用いて「Q」を導いていると解釈できますね．証明図を下からたどると，命題Qを示すには，命題P⇒Qと，命題Pを示せばよいという構造を表しているとも解釈できます．
数理論理学では，証明をこのような記号を用いた証明木によってモデル化し，証明そのものの性質を調べます[1]．
さて，ここからはプログラミング言語における関数の型に視点を移します．以下の関数を用意します．