Conversation

Notices

1. きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Thursday, 12-Aug-2021 11:22:25 JST きゅーけー

   順列の数がリストの長さの階乗になることの証明は、途中で心が折れそうになっても正しければ証明はできるのだということを学ぶ良い機会になった。

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Thursday, 12-Aug-2021 11:25:04 JST きゅーけー

     in reply to

     ACL2 は一階述語論理を使ってるのでゲーテルの完全性定理により恒真の定理は証明できるはずなのだ……。(それ必要な公理が欠けてたらどうなるんみたいな感じで、なんでそんなことがいえるのかについてはなんも分かってない)

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Thursday, 12-Aug-2021 11:26:26 JST きゅーけー

     in reply to

     ACL2 を今後も使っていくことを考えるとちゃんと一階述語論理についても学んだ方がよいのだろうか。