今日の証明
Netを覗いて見ると。A→AのCoqでの証明例があり試してみた。
Coqは定理証明支援系の一つです。
Coq証明②で演繹定理を適用して、(intros.)
A → Aを
A ⇒ Aに置き換えている。Ａ⇒Ａは、「ＡはＡであると結論付ける」と読む。
Aをリンゴ(apple)とすれば”リンゴはリンゴ”で当たり前の事（公理）で証明できた。(exact H.) ←Isabell/Holのassumptionコマンド相当でしょうか？？
リンゴはミカンであると結論付ける事を、その筋の業界用語で「論理の飛躍が有る」と言います。
リンゴはニュートン、またはニュートンはリンゴと結論付けると論理の飛躍無しに感じる人もいるでしょうけど、誰もが納得する結論はA⇒A(公理)だけです。（推件計算の本参照してね）。
