メタな意味で（つまり日本語の「ならば」、のただの略記として）⇒使って
ただの論理記号の意味で→使ってたんじゃないの？
逆になってるような

あれ、書いてなかったかな
>>95と同じで、命題変数AにもBにも命題変数や、¬（命題変数）の形の命題論理式
（つまり所謂literal）を入れれば、当然証明出来ない
従って「ＡがＨｐで証明可能⇔ＢがＨｐで証明可能」
は、どっちも証明不可能だから成り立つ

「Ａ⇔ＢがＨｐで証明可能」は、たとえばAが命題変数、Bが¬Aのとき、明らかに成り立たないから証明も出来ない

述語論理のときは>>75とか>>79みたいにそれ自身も、その否定も証明できない
閉論理式なら何でも良い（例えば集合論ZFCなら、連続体仮説とかね）