Impossibility of proving a foundation to be consistent

Question

An argument came to my mind that seems really mind-blowing and I haven't found it anywhere. Here's how it goes:

We call a formal system F embodied in classical logic a foundation of mathematics when each and every statement of mathematics is translatable into its language and interpretable accordingly.

By Gödel's second incompleteness theorem, we know that any foundation of mathematics cannot prove its own consistency because it necessarily should include arithmetic.

If we came up with a mathematical proof of the consistency of F, then by definition of F we would be able to mimic that proof inside F, contradicting Gödel's second theorem, proving F to be inconsistent, so F is useless.

In other words, if F is consistent, not only are we not able to prove its own consistency inside F, we are not able to prove its consistency using tools beyond it.

Therefore, if a foundation F really is absolutely consistent, there is no way to know it is.

Is this a good argument?

I think the argument leaves out some other methods of proving the consistency of F, methods that are not at all mathematical. But knowing that F is itself a mathematical object, what else can we use to study it?

Answer 1

This kind of question is dicsussed and (for me) well answered into:

• Torkel Franzén, Gödel's theorem: An incomplete guide to its use and abuse (2005), Ch.5.3 Consistency Proofs, page 107-on:

it is a simple matter to prove $\mathsf {PA}$ consistent using only ordinary mathematics. [...] We say that a theory $T$ is arithmetically sound if every arithmetical theorem of $T$ is true. An arithmetically sound theory is consistent, since an inconsistent theory proves the false arithmetical statement $0=1$. [...] to prove that $\mathsf {PA}$ is arithmetically sound [...] we need to define "true arithmetical sentence," then we need to show that the axioms of $\mathsf {PA}$ are all true arithmetical sentences and that the rules of reasoning of $\mathsf {PA}$ lead from true premises to true conclusions. Inevitably, this involves some logical and mathematical formalities.

the proof that the axioms of $\mathsf {PA}$ are true and the rules of reasoning of $\mathsf {PA}$ lead from true statements to true statements uses just the same axioms and rules of reasoning as those embodied in $\mathsf {PA}$, plus a little bit of set theory or some mathematics at a comparable degree of abstraction. The proof is sometimes said to be carried out in $\mathsf {ZFC}$, but logically speaking this is enormous overkill. Only a very much weaker set theory is needed to carry out the proof, specifically a fragment of $\mathsf {ZFC}$ known as $\mathsf {ACA}$.

So what we have here is a mathematical proof, formalizable in the weak set theory $\mathsf {ACA}$ [...], using ordinary mathematical principles, that $\mathsf {PA}$ is consistent. A common objection to this description of what has been achieved is that the proof is really no proof of consistency, for $\mathsf {ACA}$ is logically stronger. So all we can say that the proof shows is the consistency assuming the consistency of $\mathsf {ACA}$. In other words, the proof shows that if $\mathsf {ACA}$ is consistent, then $\mathsf {PA}$ is consistent. This whole line of thought is predicated on the assumption that we have doubts about the consistency of $\mathsf {PA}$ and are trying to allay those doubts by means of a consistency proof. But when we regard the axioms and principles formalized in $\mathsf {PA}$ and $\mathsf {ACA}$ as straightforwardly part of our mathematical knowledge, the soundness proof for $\mathsf {PA}$ is not intended to allay any doubts at all. It is quite simply an essentially trivial proof of a basic result in logic.

There is, therefore, no basis in Gödel's theorem for the idea that a consistency proof is not a proof in exactly the same sense as any other mathematical proof is a proof. Every mathematical proof is based on certain basic axioms and rules of reasoning. A consistency proof such as the one sketched by no means yields a justification of the axioms and rules of reasoning formalized in $\mathsf {PA}$. It is just a proof of an arithmetical statement, a proof which establishes the statement as true in the same way and in the same sense of "establish" as do other proofs of arithmetical statements using those same axioms and rules of reasoning.

In a nutshell, every "absolute" foundational system F will be obviously open to some sort of "skeptical challenge": any conceivable system will be based on some assumptions, and it is always possible to ask for the justification of these assumptions.

Regarding an "absolute" consistency proof of $\mathsf {PA}$, the natural numbers sequence $\mathbb N$ is a model of it and is a "standard" result of logic that a theory having a model is consistent.

Answer 2

I'd say it's not really true that we can "never know" the system is consistent. For a first example, Gentzen gave a consistency proof for PA by using a principle which PA can't formalize but which many/most accept as true (transfinite induction up to the countable ordinal $\varepsilon_0$).

Of course, PA isn't a foundation for all, or even most, of mathematics, so it's not surprising that it would fail to capture some or many aspects of mathematical practice. ZFC is a better example. Is it impossible to really know it's consistent? Assuming ZFC is consistent, a proof of its consistency can't be formalized (mimicked) within ZFC, so the proof would have to rely on a new principle or axiom. One such axiom is the existence of an inaccessible cardinal: if $\kappa$ is such a cardinal then $V_{\kappa}$ is a (set) model of ZFC, so ZFC is consistent. However, one may ask how certain we are that inaccessibles exist — surely that's less certain than the consistency of ZFC. Even simpler possible axioms can be cited, but they beg the question: $\operatorname{Con}(ZFC)$, for example.

I have to conclude that the jury remains "out" on the answer to your question. "Certainty" concerning the consistency of a formal system that provides a foundation for mathematics would require some principle not captured or proven by the system, and in which the mathematical community would have great confidence. I'm not sure that such a principle has presented itself so far.