なぜ部分関数が許されないのかの説明に補足をする

[Seasawher]

確かに、停止しない関数を許すと False が証明できるのだが、それ以前にカリーハワード同型対応から「帰納法は再帰」なので、無限再帰を許すというのは当然終わらない帰納法を許すことに繋がり、どう考えても不健全な証明に繋がる。