現在２０２１年４月１９日７時３７分である。
麻友「早起きね」
私「今日は、通院なんだ」
- 作者:安井 邦夫
- 発売日: 2021/03/31
- メディア: 単行本
若菜「月曜日は、『フーリエの冒険』のはずですけど」
私「昨日、あと少しで、時間切れになったから、纏めをする。許してくれ」
結弦「どう纏めるの？」
『ＮＪについての書き直し（その２）』で、
＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊
ところで、
が、 で、証明できることの証明は、それほど易しくないので、以下に証明しておこう。
まず、方針を示す。
(1)以下の つの論理式は、
の定理である(つまり、仮定のすべてが落ちている、演繹図の結論になっている)ことを、証明する。
(2)次に、そのことを仮定した上で、以下の論理式、
が、 の定理であることを、証明する。
(3)最後に、 の定理となった、
を用いて、
の定理
と、なるので、 の定理は、仮定がすべて落ちている演繹図の結論であるから、
が、証明されたことになる。
＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊＊
と、書いたね。そして、『ＮＪについての書き直し（その２）～（その５）』で、すべて証明した。だから、 の推論図、
は、 で、証明できることが、分かった。これにより、
は、
より弱い。つまり、
の定理は、
の定理であることが、分かった」
結弦「お父さんの証明は、完璧なんだけどさあ、論理の公理、 を使うところを、全部、
による、お父さんの
の証明で、上書きすれば、論理の公理なんて、持ち出さなくても、良かったんじゃない？
の、 と、
のところ」
私「あっ、そうか。そうだな。これは、一本取られた」
若菜「えっ、どういうこと？」
私「こういうことだろう。時間が無いので、演繹図の綺麗な整頓は、読む方に任せるけど」
結弦「 で、書いているときって、こんなメチャクチャなものを、ひとつひとつ微調整していくの？」
私「そもそも、エラーがあると、表示もされない。大変なんだぞう」
若菜「ひとつ、聞きたいのですが、この演繹図の横線に中に、一本だけちょっと太いものがありますね。 と、
のところ。あれは、『本当はもっとここに推論があるけど、十分分かるから、省略します』ということですか？」
私「良く分かったな。その通りだ」
麻友「 って、大変なのねえ」
私「このブログでは、プレビューで、確かめられるから、楽だけど、昔は、１回１回、コンパイルしないと、見られなかったんだぞ。本当に大変だった」
麻友「ちょっと気になるのは、 が、２箇所で、仮定除去されているでしょ。５番と６番って、同じ
を、区別できるのかしら？」
私「それは、この演繹図を、手で実際書いてみると、分かるんだ。５番目が、仮定除去された後に、６番目が現れるんだ。だから、混乱しない」
麻友「ああ、数字は、最初から付いているのではないのね」
私「そうだよ」
若菜「そろそろ、病院に行かなければ」
私「そうだな。行ってくるよ。今回は、ほとんど、問題なしだな。ポートに行けてることだけが、報告すべき事だな」
麻友「良かったわね。行ってらっしゃい」
私「バイバイ」
現在２０２１年４月１９日１０時１６分である。
