How do we know whether certain mathematical theorems are circular?

Question

There are countless mathematical theorems and lemmata, some of which, obviously, depend on others.

My question is: how do we know that, say, Theorem $A_1$- which uses a result proved in Theorem $A_2$ which uses a result proved in ... which uses a result proved in Theorem $A_n$ which, in fact, relies on the fact that Theorem $A_1$ is true - doesn't make the proof of Theorem $A_1$ circular?

Essentially, what I'm saying is that, since there's no comprehensive list of all mathematical theorems, lemmata and corollaries (and what statements they rely on), how can we assume that no two theorems will be circular (not directly- but down a long chain of theorems)?

If I'm not articulating myself properly, please ask me to elaborate. Thanks

Answer 1

The shortest answer is this: because theorem $A$ can only be proven using theorem $B$ if theorem $B$ is already proven. This way, your circular chain can never happen, since $B$ can only be proven using already proven theorems, meaning $A$ cannot be used to prove neither $B$ nor any theorems used in the proof of $B$ (or any theorem used in the proof of a theorem used in the proof of a theorem used in the.... .... used in the proof of $B$)

Answer 2

If the result is sufficiently important, it will have been checked (with it's foundations) by several independent groups. I.e., in a graduate course (don't remember the topic, sorry) one assignment was to read and comment on a group of papers. That meant getting familiar with the results used as a starting point in each, and checking the whole framework. Sure enough, we found a corner case in which one theorem failed...

Important theorems get many independent proofs (see e.g. Aigner and Ziegler's "Proofs from THE BOOK" for some examples, or search for proofs of Pythagoras' theorem).

Answer 3

There is no guarantee, however as mentioned in the other answers, pivotal results come under close scrutiny which reduces the chance of any circularity. This reflects the fact that proofs are more of a social process than dry formal verification. Assumptions and theorem statements are often tweaked as as consequence.

Many results are based on an intuition, which can be misleading, but in general tends to be a reasonable guide.

Some proofs (the four-colour theorem) are computer based, which adds a whole new dimension to your question.

In general, the longer a result has been around and the more it has been 'used', the more likely it is not circular.

Answer 4

2022 Edit: Having just checked these links again, it seems the dependency graph feature mentioned below has been removed or relocated. It was an interesting feature, so if anyone knows about it, I'm happy to hear where it went!

---

You should take a look at the Stacks Project. There is a neat feature due to the way theorems and lemmas are organized that allows you took look at dependency graphs for all the results.

In other words, if you look at a certain theorem or lemma (for example here), you can look in the "dependency graphs" section in the lower right to look at every result which is used in the proof, and every result used to prove those results and so on (Here is a dependency graph for the example before).

These graphs would make it clear if there were a circular dependency, but they're also fun just to look at and explore. This is just for algebraic geometry though so I don't know if something like this exists for other parts of mathematics.

Answer 5

Circular proofs do exist, usually in the following situations:

• arguments (for correct theorems) in textbooks that use principles equivalent to the conclusion. This is done in the explanation of elementary material that was sorted out a century (or several centuries) ago, often when there is a geometric or intuitive component to the argument. The sorting process detected and corrected any circularity in the original proofs, but for instructional reasons or lack of space, the full story is not reflected in the books.

• proofs done in the less-rigorous olden times. Levels of precision varied, and arguments could appeal to informal arguments or intuitive principles. The most common logical problem that this would create was gaps in the proof where one or more steps were ill-defined, but there are also cases (such as the parallel postulate, or attempts to found real analysis) where a precisely stated principle was secretly equivalent to the thing being proved.

The mathematics literature does contain circular chains of citations, but it is rare (and easily noticed, for results that are read and used by others) for that to involve circles in the proofs. Papers with similar results published close to simultaneously often cite each other, but not for the proofs. The use of cycles of self-citations to cover for deficient proofs undoubtedly occurs sometimes but is a form of "pathological science" for which there are enough checks and balances to keep it from infecting the core.

Answer 6

I think the argument given by 5xum is the basic reason we trust most proofs. However, I know of several scenarios where circular proofs could possibly get into the literature.

One scenario is a mathematician writing a number of papers published in parallel. If the papers cite each other, there could be a circularity. A prominent mathematician (a Fields medalist) once told me of a case of an apparently circular argument in a series of papers by a famous mathematician. He believed it was actually a deliberate deception. Since I haven't personally verified this, I'm not going to name names. While this is possible, it is a rather rare circumstance.

Another scenario is theorem A is published. Later theorems B, C, ... are proven based on theorem A. Later, other proofs of theorem A are given possibly based on some of the theorems B, C, ... Such later proofs are circular and invalid, but at least the original proof is valid, so we may have invalid proofs but at least the theorems are all correct. Except ... what if the original proof of theorem A was erroneous and no one discovered the flaw? Or, even if the flaw in the original proof was discovered, but the later proofs are still accepted as valid. It may be very hard to sort out what is valid and invalid if there's a lot of intervening work.

Similar things can happen when textbooks are written that cite each other. I know of cases of erroneous statements given as "theorems" in well regarded and frequently cited texts. Often, such "theorems" are left as exercises or are claimed to be easy to prove.

So, ..., I generally trust the mathematical literature, but it's quite possible there are circular proofs out there. I also think there are many undiscovered errors in published proofs. Anyone who's done any computer programming knows that bugs are unavoidable and sometimes maddeningly difficult to find, even in seemingly simple and clear code. I have no doubt the same is true of math, except we don't have to pass our proofs through compilers and run them.

In the long run, I think the answer will be that some day we will run our proofs through compilers, in the form of automated proof verifiers. Gradually, we'll codify all of mathematics into machine verifiable systems that won't allow circular proofs.

Answer 7

Extending on @Josefs answer and your phrase "comprehensive list of all mathematical theorems": I asked about this sort of quest here: What is an efficient nesting of mathematical theorems?. In the last 2.5 years, I researched this a bit.

The biggest math library, starting from set theory axioms as initial "theorems" is Mizar. You find a page where they publish they theorems in pdf-format too, see here. The two languages Agda and Coq have a more active community and I know the first one has a library too. And there are more such projects, in particular in the Computer Science community. And there is, in fact, a subfield now, called Mathematical knowledge management which tried to forms tools to do that sort of thing in a less ad hoc fashion.

A year ago I started a similar project for myself, where I mostly sort sets by the inclusion relation, AxiomsOfChoice.org. (It has a graph rendered with the graphviz software, but now that there are over 200 entries it got completely messy. Anyone with serious interest in a coding challenge please write me!) I encountered the algebraic stacks project Joseph links too before I also know of some guys wiki on groups, which thousands of pages.

I also want to say that circular arguments are bad as far as the "math game" goes, but one should keep in mind that for many it's important to foster the things that work. I could point you to the logic project Reverse Mathematics, where people explore interdependencies by "starting at the good stuff".

I could post more links in that spirit, but my message is that people are thinking alot about this kind of stuff :)