Comment by tromp

That entirely depends on how you want to interpret a finite binary string as an enumeration of logic proofs?!