論理におけるrecursion-capable

だんだん思い出した：指標＝インターフェイスの理論 - 檜山正幸のキマイラ飼育記 メモ編

• Lがrecursion-capable ⇔ Impl_Lがweakly trace-admissible

Lが、構造に対する制約・条件を記述する論理言語（命題言語／証明言語）を備えているとする。このとき、Lの指標は、セオリーと呼んでもいい。つまり、Imple_Lはセオリーとセオリー射の圏となる。

この状況で、Lがrecursion-capableとはどういうことか？ おそらく帰納的な証明が可能な論理体系ということになるだろう。論理まで考えたときのrecursion-capableはinduction-capableになるんだと思う。面白い問題だな、これは。