帰納的述語に対して帰納法の原理を生成することはなぜ難しい？

[Seasawher]

inductive predicate に対して自動的に帰納法の原理を生成するのは難しいんですかね？
再帰関数に対してはできているわけですけど

[Seasawher]

たぶん難しくてできないのだろうなという気がする。なぜなのか、すぐにわからない。