Why are proofs so valuable, although we do not know that our axiom system is consistent? [closed]

Question

As a person who has been spending significant time to learn mathematics, I have to admit that I sometimes find the fact uncovered by Godel very upsetting: we never can know that our axiom system is consistent. The consistency of ZFC can only be proved in a larger system, whose consistency is unknown.

That means proofs are not like as I once used to believe: a certificate that a counterexample for a statement can not be found. For example, in spite of the proof of Wiles, it is conceivable that someday someone can come up with integers a,b and c and n>2 such that a^n + b^n = c^n, which would mean that our axiom system happened to be inconsistent.

I would like to learn about the reasons that, in spite of Godel's thoerem, mathematicians (or you) think that proofs are still very valuable. Why do they worry less and less each day about Godel's theorem (edit: or do they)?

I would also appreciate references written for non-experts addressing this question.

Answer 1

If you like, you can view proofs of a statement in some formal system (e.g. ZFC) as a certificate that a counterexample cannot be found without demonstrating the inconsistency of ZFC, which would be a major mathematical event, and probably one of far greater significance than whether one's given statement was true or false.

In practice, a given proof is not going to be closely tied to a single formal system such as ZFC, but will be robust enough that it can follow from any number of reasonable sets of axioms, including those much weaker than ZFC. Only one of these sets of axioms then needs to be consistent in order to guarantee that no counterexample would ever be found, and this is about as close to an ironclad guarantee as one can ever hope for.

But ultimately, mathematicians are not really after proofs, despite appearances; they are after understanding. This is discussed quite well in Thurston's article "On proof and progress in mathematics".

Answer 2

Gödel's theorems do not say that we can never know our axiom systems are consistent. Not at all. What they say is that we can never prove that certain systems are consistent within those systems themselves. This leaves open the possibility that we can prove their consistency in other axiom systems, or can convince ourselves of their consistency by methods that are not completely formal.

My recommended reference on the incompleteness theorems for a general reader is "Gödel's Theorem: An Incomplete Guide to its Use and Abuse" by Torkel Franzén. This book has the rare combination of being written to be broadly accessible while still being precise enough to be satisfying.

Answer 3

To address the issue of Fermat's Last Theorem: the reasoning behind Fermat's Last Theorem, while elaborate, in the end rests on basic intuition about the integers. (I'm not sure that it is actually proved in first order Peano arithmetic, since the proof as written certainly uses concepts outside of PA, but nevertheless, it is basically a result about numbers, proved using our fundamental notions about numbers.)

If the proof was correct, but the statement wrong (due to an inconsistency), there would be something fundamentally wrong in our conception of numbers. I don't think this would be like the crisis in set-theory: it would be much more fundamental. For example, if induction turns out to be inconsistent (and this is the kind of thing being speculated about here), this says that our basic intuition for the natural numbers, namely that non-empty subsets have least elements, is wrong. If that is true, then all mathematics goes out the window!

I think that most mathematicians (indeed, most humans who have been taught arithmetic) have a mental model of the natural numbers which says that you can always add 1 to get a new number, and that between any two natural numbers there are only finitely many more (so that any non-empty subset of the naturals has a least element). Given this, they know that PA is in fact consistent, even though PA doesn't prove this. They are proving it by exhibiting a (mental) model; they don't need formal arguments. (This falls under the class of "not completely formal" methods alluded to by Carl Mummert.)

Answer 4

We adopt axioms not because we can prove their consistency, but because we believe that they accurately describe something that we want to study. A proof from these axioms will have value in that it shows how the proposition (which may be surprising or complicated) follows from things that we already believe and are simple. If we someday prove an inconsistency using a given set of axioms, this shows that our possibly naïve intuition for reasonable axioms was incorrect. (e.g. Russel's paradox showing that unrestricted comprehension is a bad idea)

Answer 5

To answer the question posed:

A proof is valuable because it helps convince oneself and others of the validity of that result from the axioms [whether those axioms are consistent or not]. Mathematicians, I believe, are not worried that the axioms are inconsistent, but rather hopeful that they are consistent; or even more precisely, optimistic that if the axioms are inconsistent they can be modified [if necessary] to be consistent and still encompass most things proved. But even if they are inconsistent, we won't figure that out without lots and lots of proofs in the meantime.

To answer the philosophical question from a personal point of view:

From my point of view, I do mathematics because I love certainty and truth. I also enjoy discovery. Godel's theorems simply tell me that there are some things I will never be certain of or discover (inside a formal system). This may be disappointing, but at some level we all have to deal with uncertainty. For example, I could be deceiving myself that I'm typing this message. But I (and most others I know) are willing to accept a few things on faith; and if shown we are wrong, modify our beliefs accordingly.

Answer 6

To stray from mathematical logic to how other mathematicians might think about proofs...

I think many mathematicians go with Carl's "convince ourselves of their consistency by methods that are not completely formal." Many mathematicians use set theory simply as a language--probably similar sorts of mathematicians as do not concern themselves with categories too much, of which type there are still many. Mathematicians with a physics bent often enjoy "informal" arguments based on physical intuition, a mechanical construction, or the nonrigorous arguments of Archimedes or Appolonius or Cavalieri using a primitive version of infinitesimals to compute volumes, etc. The insight gained from less formal arguments, while less definitive, perhaps, probably outweighs the worries about set-theoretic and proof-theoretic issues for many mathematicians. (A graph theorist, for example, could be perfectly happy proving results for classes of graphs and graph properties for their whole career, knowing that the results are true for graphs the way one usually pictures them, without worrying about the consistency of ZFC).

Since your question is part mathematical logic and part psychology (whether people "worry"), may I suggest some of the literature on pedagogy for higher mathematics? Many people have thought a lot about how to treat the concept of proof and other issues in courses for various sorts of students in order to maximize the understanding and value gained. See, for example, David Henderson's work on "educational mathematics" at Cornell.

Answer 7

Most practically-useful mathematics does not need the strength of a theory such as ZFC. The reverse mathematics programme shows that many notable theorems can be stated in $RCA_0$, which is a finitistic system. Most other systems studied in revese mathematics (such as $WKL_0$, $ACA_0$ or $ATR_0$) are subsystems of second-order arithmetic, and also enjoy conservativity properties over $RCA_0$.

Answer 8

Not sure why Gödel's theorems are relevant here. It is indeed unknown whether ZFC is consistent. Somewhere at the undergraduate level students are lead to believe that a proof gives an absolute certainty. Later they learn that this is not quite true, big deal. Most working mathematicians believe in consistency of ZFC, and nobody yet proved them wrong. To date proofs have served us remarkably well.

Answer 9

Perhaps you should be upset if you've been led to believe as a generalisation that "...we never can know that our axiom system is consistent", and that "...proofs are not like as I once used to believe: a certificate that a counterexample for a statement can not be found".

These beliefs may be understandable (even if not justifiable) in the case of a set-theoretical language such as ZF, which can have no finitary interpretation.

They are misleading in the case of a first-order language such as PA which, in a digitally communicating universe, would be of more consequence than ZF.

Misleading, because they reflect the subjective belief that Aristotle's particularisation holds over the structure N of the natural numbers; which is the postulation that from an assertion such as:

'It is not the case that, for any given x, P(x) does not hold in N',

usually denoted symbolically by '~(Ax)~P(x)', we may always validly infer that:

'There exists an unspecified x such that P(x) holds in N',

usually denoted symbolically by '(Ex)P(x)'.

However, as Brouwer had noted in a seminal 1908 doctoral dissertation, the presumption that Aristotle's particularisation holds over infinite domains such as that of the natural numbers does not lie (as self-evident) within a common human intuition; and such a presumption has no logical basis in the objective decidability and computability of number-theoretic relations and functions over the domain of the natural numbers.

Now, although Kurt Goedel's arguments in his seminal 1931 on undecidable arithmetical propositions avoid assuming that Aristotle's particularisation holds over N, Goedel found it necessary to assume that the Peano Arithmetic he was considering was omega-consistent.

Omega-consistency: PA is omega-consistent if, and only if, there is no PA formula [F(x)] such that [~(Ax) F(x)] is PA-provable and also that, for any PA-numeral [n], [F(n)] is PA-provable.

However, it is easily seen that PA is omega-consistent if, and only if, Aristotle's particularisation holds over N.

(Although J. Barkley Rosser claimed in a 1936 paper to prove the existence of undecidable arithmetical propositions without the assumption of omega-consistency, his argument appears to implicitly presume that Aristotle's particularisation holds over N.)

The assumption of omega-consistency has a history.

David Hilbert was one who firmly believed that an arithmetical proof is, indeed, a certificate that a counterexample for a true arithmetical statement can not be found.

Thus, as part of his program for giving mathematical reasoning a finitary foundation, Hilbert proposed an omega-Rule as a finitary means of extending a Peano Arithmetic to a possible completion (i.e. to logically showing that, given any arithmetical proposition, either the proposition or its negation is formally provable from the axioms and rules of inference of the extended Arithmetic).

Hilbert also believed that the standard interpretation of PA is sound, which implies that Aristotle's particularisation holds over N.

In a contemporary context, Hilbert's omega-rule can thus be expressed as:

Hilbert's omega-Rule: If it is proved that a formula [F(x)] of the first-order Peano Arithmetic PA interprets under the standard interpretation of PA as an arithmetical relation F(x) that is true for any given natural number n, then the PA formula [(Ax) F(x)] can be admitted as an initial formula (axiom) in PA.

Goedel's 1931 paper on formally undecidable arithmetical propositions can, not unreasonably, be seen as the outcome of a presumed attempt to validate Hilbert's omega-rule by his assumption of omega-consistency.

However, Goedel discovered a PA formula [R(x)] such that if PA is assumed omega-consistent, then both [(Ax)R(x)] and [~(Ax)R(x)] are not PA-provable (Goedel's First Incompleteness Theorem).

Further, assuming that Aristotle's particularisation holds over N, Goedel defined a number-theoretic relation Wid(PA) which holds in N if, and only if, PA is consistent.

Goedel then discovered (his Second Incompleteness Theorem) that, if PA is assumed consistent, and we assume that some PA formula [W] expresses Wid(PA) in PA, then [(Ax)R(x)] is PA-provable if [W] is PA-provable.

Ergo, if PA is omega-consistent, then we cannot express the assertion 'PA is consistent' in PA by a PA-provable formula.

Now the points to note are that:

1. PA is omega-consistent if, and only if, Aristotle's particularisation holds over the domain N of the natural numbers.

2. If the standard interpretation of PA is logically sound, then Aristotle's particularisation holds over N.

3. Aristotle's particularisation over N can be expressed in contemporary terms as:

From an assertion such as:

'It is not the case that, for any given x, any witness Witness_N of N can decide that P(x) does not hold in N',

usually denoted symbolically by '~(Ax)~P(x)', we may always validly infer that:

'There exists an unspecified x such that any witness Witness_N of N can decide that P(x) holds in N',

usually denoted symbolically by '(Ex)P(x)'.

The validity of Brouwer's objection follows since Aristotle's particularisation does not hold over N if we take the witness Witness_N as a Turing machine, and P(x) is a Halting-type of number-theoretic relation.

It follows that if PA is not omega-consistent, then we cannot conclude from Goedel's Incompleteness Theorems that Goedel's [~(Ax)R(x)] is unprovable in PA.

The significance of the above is that issues involving number-theoretic functions and relations containing quantification over N lie naturally within the domains of:

(a) First-order Peano Arithmetic PA, which attempts to capture in a formal language the objective essence of how a human intelligence intuitively reasons about number-theoretic predicates, and;

(b) Computability Theory, which attempts to capture in a formal language the objective essence of how a human intelligence intuitively computes number-theoretic functions.

Now Goedel had also shown in Theorem VII of his 1931 paper that every recursive relation can be expressed arithmetically.

This suggests that if we can, conversely, define a finitary interpretation of first-order PA over N as sought by Hilbert, then any number-theoretic problem can be expressed - and addressed - formally in PA and its solution, if any, interpreted finitarily over N.

Now, if [A(x1, x2, ..., xn)] is an atomic formula of PA then, for any given sequence of numerals [b1, b2, ..., bn], the PA formula [A(b1, b2, ..., bn)] is an atomic formula of the form [c=d], where [c] and [d] are atomic PA formulas that denote PA numerals. Since [c] and [d] are recursively defined formulas in the language of PA, it follows from a standard result that, if PA is consistent, then [c=d] is algorithmically computable as either true or false in N.

In other words, if PA is consistent, then [A(x1, x2, ..., xn)] is algorithmically decidable over N in the sense that there is a Turing machine TM_A that, for any given sequence of numerals [b1, b2, ..., bn], will accept the natural number m if, and only if, m is the Goedel number of the PA formula [A(b1, b2, ..., bn)], and halt with output 0 if [A(b1, b2, ..., bn)] interprets as true in N; and halt with output 1 if [A(b1, b2, ..., bn)] interprets as false in N.

Moreover, since Tarski has shown that the satisfaction and truth of the compound formulas of PA (i.e., the formulas involving the logical connectives and the quantifiers) under an interpretation of PA is definable inductively in terms of only the satisfaction (non-satisfaction) of the atomic formulas of PA, it follows that the satisfaction and/or truth of the formulas of PA under the usual interpretation of the PA symbols is algorithmically decidable.

This is clearly a finitary interpretation of PA over N.

So, if Aristotle's particularisation does not hold over N, and the standard interpretation of PA is not logically sound, then - instead of considering Hilbert's omega-rule - the question that one ought to consider is whether the above is a sound algorithmic interpretation of PA such that:

Algorithmic omega-Rule: If it is proved that the PA formula [F(x)] interprets as an arithmetical relation F(x) that is algorithmically decidable as true for any given natural number n, then the PA formula [(Ax)F(x)] can be admitted as an initial formula (axiom) in PA.

This question is far more amenable to finitary reasoning, and I argue that it can be answered affirmatively. See:

http://alixcomsi.com/27_Resolving_PvNP_Update.pdf

If so, it would confirm that your faith in the classical notion of a proof is not misplaced, and an arithmetical proof is, indeed, a certificate that a counterexample for a true arithmetical statement can not be found.