 As it is decidable (by the definition of formal systems) whether a given sequence of formulas constitutes a proof of a given sentence, according to the rules of the chosen formal system \(F\), the binary relation “\(x\) is (the Gödel number of) a proof of the formula (with the Gödel number) \(y\)” can be strongly represented in all systems containing Q, and thus in \(F\) in particular. Let us denote the formula which strongly represents this relation in \(F\) itself as \(\Prf_F (x, y)\).  The property of being provable in \(F\) can then be defined as \(\exists x\Prf_F (x, y)\). Let us abbreviate this formalized provability predicate as \(\Prov_F (x)\).  It follows that the latter is weakly representable (though, it turns out, not strongly):