Let $\phi$ be a ZFC formula and $\lceil \phi \rceil$ its syntactic representation.
We can build the following program:
- program BoundedCons( x )
- check if there exists a ZFC proof $\Gamma$ of length $|\Gamma| <= |x|$ of a contradiction (i.e. check for a string $\lceil ZFC \vdash ... \vdash \phi \land \neg \phi \rceil$ shorter than $|x|$)
- if we find it then Loop forever; otherwise Halt
If we define $\psi \equiv $"BoundedCons halts on all inputs"
ZFC cannot prove $\psi$, but
Can we say that $ZFC$ augmented with an axiom that $ZFC$ is consistent proves $\psi$ (i.e. $ZFC+Con(ZFC) \vdash \psi$) ?
Yes (assuming you define "length" properly) - $\psi$ is in fact equivalent to $Con(ZFC)$. More precisely, ZFC (or much, much less) proves $\psi\iff Con(ZFC))$; all we need to prove the equivalence is basic reasoning about Turing machines and proofs, and ZFC is more than enough to prove the required results.