Self-verifying theory! But what can we learn from it?

Question

There is this seemingly surprising result that no consistent and sufficiently expressive theory can prove its own consistency. But what would be the actual benefit from knowing that a theory $T$ can do this? (e.g. Dan Willard's self-verifying theory) As I understand, we can encounter one of the following two scenarios:

1. $T$ is consistent and proves its own consistency.
2. $T$ is inconsistent, and because of this, also proves its own consistency.

The outcome is the same. So even if we can prove that $T$ proves its own consistency (do we need a meta theory here?), then we have no way to conclude whether $T$ is actually consistent or not, despite of the given proof. So what have we learned at all?

Is this more a tool to classify the expressive power of a theory than actually talking about its consistency? In the end it is easy to find a theory that proves its own consistency $-$ just take an inconsistent one. What distinguishes Dan Willard's self-verifying theory from such a trivial example? That it is not obviously inconsistent?

---

NOTE:

Feel free to make a note, whether this question might be better placed in another SE, like philosophy. I honestly do not know if it belongs here.

Answer 1

As I've always seen it, the Incompleteness Theorem isn't really about consistency so much as "totality". The idea is that the Holy Grail of mathematical foundations was to find a single system of axioms which (a) we believed to be true and (b) could prove everything in math. Godel's Incompleteness demonstrates that this goal is unattainable: there will always be a sentence that is true but unprovable from our axioms, unless we make the mistake of choosing inconsistent axioms. The fact that the sentence in question is "the axioms are consistent" isn't terribly important.

In fact, as I understand it, for some time many mathematicians considered Incompleteness unimportant - the philosophy was that sure, there are true sentences unprovable from (e.g.) ZFC, but they're just pathological things like Con(ZFC) that no one would really care about (for exactly the reasons you pointed out). It wasn't until the Continuum Hypothesis was shown to be independent of ZFC that people really understood that Incompleteness was a serious obstacle for foundational mathematics in general.

Now, of course, independence results have graduated from "obstacle" into "field of interest"; most people have given up on finding that Holy Grail, and instead started enjoying the Holy-Enough Grail that we have in ZFC. In fact, interest has sparked in going the other direction, to less powerful theories, like the Somewhat-Holy Grail of ZF (ZFC without the Axiom of Choice).

Answer 2

Inconsistent theories still generate correct proofs. Take for example naive set theory: Even though it turned out to be inconsistent, the work (for example) of Cantor wasn't erroneous and most results still hold in axiomatic set theory.

The same applies with arithmetics. If a proof of the consistency of arithmetics could exist within arithmetics, the proof may be such that we are convinced of its correctness. This is because an inconsistent theory proves everything via contradictions, so a proof of consistency might be produced in such a way, or from such a fragment of arithmetics, that we can feel relatively confident about its correctness. In the end we have some intuitions about numbers on which we can base the safety of such a proof.

This was (roughly) the idea of Hilbert: Produce a proof from finitistic methods (methods that we feel confident about their correctness) of the consistency of mathematical theories that can produce most parts of mathematics.