論理式は、quantifierや変数記号や函数記号やらが一定の規則で
並んだものでしょ？∀x∀y x+y=y+xみたいに．
で、その中で、ある性質を持つような、自由変数を二つ持つ論理式に
Prov(x,y)と名前を付けてるだけでしょ？そういう風に書いてあるはず