>>480
>（＝特定されていない、「とある論理式Φ」のようなもの）

「のようなもの」じゃ形式化は出来ないだろ
それから形式化の仕事してるなら論理式なんて非専門用語は使わずに
命題なのか述語なのかはっきりさせないと
述語に量化記号使うなら二階述語論理になるし
大丈夫ですか

数学屋はたとえ公理の数を有限無限個にしても一階述語論理に閉じこもることを好むが
計算機科学屋はsystem Fとか昔から高階トポスに親しんでる人が多い
一階つまりエレメンタリートポスで充分なのかどうかはLean関係なく数学的な議論ができる
圏論的には量化をスライス圏における随伴関手として扱うのは当然知ってるだろうしそこまで難しくないだろ
そこをはっきりさせてくれないと形式化なんて無理
「のようなもの」なんて論外
まあIUT関連の論文ではよく出てくる言葉なんだけどw