David Udell comments on David Udell’s Shortform

[David Udell]

Now, whatever $T$ may assert, the fact that $T$ can be deduced from the axioms cannot prove that there is no contradiction in them, since, if there were a contradiction, $T$ could certainly be deduced from them!

This is the essence of the Gödel theorem, as it pertains to our problems. As noted by Fisher (1956), it shows us the intuitive reason why Gödel’s result is true. We do not suppose that any logician would accept Fisher’s simple argument as a proof of the full Gödel theorem; yet for most of us it is more convincing than Gödel’s long and complicated proof.

Now suppose that the axioms contain an inconsistency. Then the opposite of $T$ and therefore the contradiction $\neg T\wedge T$ can also be deduced from them:

$A\to \neg T$.

So, if there is an inconsistency, its existence can be proved by exhibiting any proposition $T$ and its opposite $\neg T$ that are both deducible from the axioms. However, in practice it may not be easy to find a $T$ for which one sees how to prove both $T$ and $\neg T$. Evidently, we could prove the consistency of a set of axioms if we could find a feasible procedure which is guaranteed to locate an inconsistency if one exists; so Gödel’s theorem seems to imply that no such procedure exists. Actually, it says only that no such procedure derivable from the axioms of the system being tested exists.

--E. T. Jaynes, Probability Theory (p. 46), logical symbolism converted to standard symbols

[JBlack]

The text is slightly in error. It is straightforward to construct a program that is guaranteed to locate an inconsistency if one exists: just have it generate all theorems and stop when it finds an inconsistency. The problem is that it doesn’t ever stop if there isn’t an inconsistency.

This is the difference between decidability and semi-decidability. All the systems covered by Gödel’s completeness and incompletness theorems are semi-decidable, but not all are decidable.