>>250
課題１のFSに出てくる「図式」の定義は>>246のでいいの？
だとすると>>235であげられた「標数０の代数閉体の理論」はFS公理化可能ではないのでは？
「標数０」の部分は「穴」にどんな論理式を入れてもいいわけではないので。

>>260
その図式(*)も>>246の意味の図式にはなっていないよね？
"T ⊢ A" とコードの中にAを代入するのは「穴」に代入するのとは別のメカニズムが必要なので。