Comment by bmacho

Let S be a statement. S is called semidecidible (also: Turing recognizable, most commonly "recursively enumerable", abbreviated as "r.e.", but I hate that one) if there is a Turing machine that halts if and only if S is true.

With this definition, we can say that "ZFC is inconsistent" is semidecidible: you run a program that searches for a contradiction.

The question BB(748) =/= 1000 is similarly semidecidable. You can run a program that will rule out 1000 if it is not BB(748).

So they are in the same "category", at least regarding their undecidability.

Also, if you turn "ZFC is consistent" into a number: {1 if ZFC is consistent; 0 if ZFC is inconsistent}, you will see, that BB(748) is not very much different, both are defined (well, equivalently) using the halting of Turing machines, or, the result of an infinite search.