とある統計の本に「銀行の支店が多い駅前は、蕎麦屋も多い」
という話題があり、駅前に銀行支店を多く誘致するため、「駅前に蕎麦屋を誘致する」という結論を下す。さらに牧草地とバッタの例も記載されており、刈った牧草地にバッタを放つ結論を下して草が生えるのを待つ、話もあったように覚えている。
もちろん、こんな結論はだめと記載されていて、 この手の政策がままあるので注意するよう記載があった気がする。コロナ禍の政策も。。勇気のある人は検証してね！
このとある統計の本は、20年程度前に書かれた物で30年程度前の事と思われるが、今でも駅前の銀行支店数と蕎麦屋数の回帰分析をすると高い確度で、「銀行の支店が多い駅前は、蕎麦屋も多い」と結論できる思われる。
＊＊だれか試してね！。。俺はやらない
その筋の業界では、「試してね」を「検証する」と言う。
検証して見るをもう少し細かく分けると、
- 帰納的検証
- 演繹的検証
に別れ、冒頭から書いてある事柄の「試してね！」を「帰納的検証」と言う。
⇒いくつかの駅前に行き、銀行支店数・蕎麦屋数を調べ上げ、統計処理をして「銀行の支店が多い駅前は、蕎麦屋も多い」はやはり正しいと結論付けるのが帰納的検証例の一つである。
帰納的検証に対抗するためだけではないが、演繹的検証と言うものがある。
俗な言いかたでは、屁理屈をこねると言う。
上記に記したとある統計の本にも、民家が多い⇒駅の乗降客が多い⇒。。。
という屁理屈が有ったが詳細は忘れた。
浮世草子 の「風が吹けば桶屋が儲かる」でおなじみの屁理屈も演繹的なものだ。
江戸の時代に戻って帰納的に検証して見たら面白いと思うかな。
＊＊不完全性定理を少しでもかじった事のある人から突っ込みがきそうですが
雰囲気は出ていると思います。
＊＊世に言うゲーデルの不完全性定理は、上記の完全性がいつも成り立たない？あたりの事柄です。ゲーデルの不完全性定理が成り立つ成り立たない付近を理解できたら計算機科学研究者に成れるそうですが。。私は、経営・流通研究者なのそこまでは勉強しません。⇒気が向いたら勉強してみるよ。。
長い前振りであったが、一般的な技術書の書式に従った。
想定する読者層以外でも買ってもらえる長い前振りを冒頭に置き、途中からは自説を記載する。。。
今日の証明は
A →A
AならばAと読む。
上記の証明をして何が面白いと思われるでしょうが、A→Aが正しいことは重要です。
証明を行うにあたって支援ソフトなるものがあり証明支援系と呼ばれる。
下記の画像はIsabell/holと言う証明系です。
A⇒Aは推件計算では、公理と呼ばれ無条件で正しいとされている。
A→Aの”→”は含意演算子でA同士の論理演算です。このA→AをA⇒Aに置き換えてよいという規則があり、その操作はapply(rule impI)になる。
A⇒Aは公理なので無条件で正しくて、めでたくA→Aが正しいことが証明された。
** Isabell/holを立ち上げると、ソフトの動作チェックのために
theorem "P →P"
apply(auto)
が出てきて、下段のウインドウに No subgoales!と出れば動作OKとになる。
apply(auto)は自動証明コマンドなので、手動で証明してみた。
