スケマティック変数の名前を変更する

Question

定理のスケマティック変数の名前を変更する方法はありますか？ たとえば、?Pと?Qの名前をimpI:(?P ⟹ ?Q) ⟹ ?P ⟶ ?Qから?uと?vに変更することはできますか？

Answer 1

定理の自由変数は、たとえばfor節を使用してローカルに固定された正しい名前の変数でインスタンス化できます。一般化されると、それらは正しい名前のスケマティック変数になります。だから、impI[where ?P=u and ?Q=v for u v]は仕事をするべきです。