２０１９年８月２８日 （前提の日）
前回に続き、証明論系シークエントに関する話題を。
私の行間埋め作業は正しく実行されるのですが。
猿の方も、似たような真似をしてきました。
それが、論理推論におけるcutの逆操作としての
「内挿（interpolation）」
これが、どのレベルで正しいのか？
今回は、この本質がテーマです。
前回は超ＬＫの提唱が目的でしたが。
今回は、従来の古いＬＫにも適用できる話になります。
以下、判り易さを重視して、ＬＫ限定で議論していきます。
「推論の形式化（自動化）とは何か？
何であるべきか？」
非常に重要なテーマです。
証明やＡＩにおける最重要課題と言える。
その秘密が、愈々、今回、明らかになるというシナリオ。
というわけで、以下は、論理猿の知力限界を探る展開になります。