Thus, there is a primitive recursive function $B_{ZFC}(x,y)$ which takes value $0$ if and only if the numeral $x$ is a Gödel code for a formal proof of the Gödel coded sentence $y$ from the axioms of ZFC. Taking $y$ to be the Gödel code for your favorite contradiction, say $0 = 1$. The consistency of ZFC can be expressed as $\forall x (B_{ZFC}(x,y) \neq 0)$. As Carl Mummert pointed out, this is a simple $\Pi^0_1$ statement in PRA. While we don't know whether it is true or false, it is a perfectly meaningful statement from the finitistic point of view.