In a way. Consider a Turing machine that enumerates all proofs in ZFC and halts iff it finds a proof of 0=1 (i.e. a contradiction). The statement that this Turi

In a way. Consider a Turing machine that enumerates all proofs in ZFC and halts iff it finds a proof of 0=1 (i.e. a contradiction). The statement that this Turing machine halts (like the statement that any given Turing machine halts) is what’s called a Sigma_1 statement, which lies at the bottom of the arithmetic hierarchy (right above bounded-quantifier statements). ZFC + ~Con(ZFC) is consistent but Sigma_1-unsound and therefore omega-inconsistent [1]. [1] https://en.wikipedia.org/wiki/Ω-consistent_theory https://en.wikipedia.org/wiki/Ω-consistent_theory