As everybody knows, there are thousands and thousands of theorems in mathematics having a proof that is accepted without any doubt because it follows impeccable and rigorous mathematical reasoning.
I would like to know which the limits are (if any) when thinking about preparing a formal deduction for some mathematical proof:
- Is every existing theorem proof (made by mathematicians up to the moment) formalizable inside one of the most important axiomatic systems (PA, ZF, ZFC, ...)?
- Is there any theorem with an accepted mathematical proof that escapes all efforts so far to formalize it?
- Is there any evidence that humans use some kind of mathematical reasoning that is impossible to formalize?
- I know that some proofs are not accepted by some mathematicians (e.g. intuitionists). Currently I am interested in normal logic, not the intuitionistic and other special logics.
I am not referring to open problems of mathematics, but to theorems for which a proof already exist and is accepted generally by mathematicians. There are two examples that interest me greatly:
Fermat Last Theorem, a very simple arithmetic sentence that has an extremely difficult and long proof. As far as I know, it is an open question whether it is provable inside PA or not, but this doesn't worry me at the moment. I just would like to know if the existing proof can be formalized in one of the most important axiomatic systems (ZF, ZFC, ...).
Gödel's G sentence. In the introduction to "On Formally Undecidable Propositions Of Principia Mathematica And Related Systems", Gödel states that this sentence is true in the context of the Principia Mathematica (which I take as equivalent to being true in the standard model of natural numbers). He says that the sentence has been effectively proven using meta-mathematical arguments. These arguments are, of course, outside PA. The question is: is it possible to formalize those sophisticated meta-mathematical arguments in one of the most important axiomatic systems (ZF, ZFC, ...)?
I know also that you can reach the same conclusion (theorem sentence) following different "paths" from the axioms in a formal proof (i.e. there are many different formal proofs for the same theorem). Where I am curious the most is about "replicating" the mathematical proof formally as best as possible, so that the mathematical proof serves as a sketch for the formal deduction. I would like to know if every step in a mathematical proof can have the corresponding piece in the formal deduction.
ADDITIONAL NOTES (April 9th):
At this moment I am not curious about the philosophical aspect regarding the limit of human reasoning, just wondering about existing theorems produced so far by mathematicians. The history has provided a vast amount of mathematical knowledge already. If there is no evidence that the reasoning techniques used so far by mathematicians for proving theorems are beyond the usual formal systems (say ZFC), then that could be a good reason to think that no human will ever produce such a proof.
So I would like to know if there is practical evidence based on the study of existing theorem proofs. It has been said that the “proof of Fermat's Last Theorem […] is a long way off from being formalized in a system like ZFC”. I would like to know if the reason is one of the following:
- Impassable points (there are theorems on the way up that logicians are unable to formalize so far). In the process of formalizing all theorems on which Wiles proof is based (or even Wiles theorems themselves), there is (perhaps) some theorem that, as much as logicians try, they don’t find the way of translating it into a formal deduction because it uses a kind of mathematical reasoning that can’t be formalized (because ZFC falls short or because logicians don’t find the formal “path” in ZFC for going from certain point of the proof to the following one). Has this ever happened?
- It is just a matter of patience and mechanical work (until all the theorems on which Wiles proof is based are formalized, which will happen eventually because formalizing theorems is just tedious mechanical work and people is working on this). Is this the case? Is the process of producing a formal deduction from a mathematical proof a straightforward process (although tedious). Can this “translation” process be guided directly by the deductions used in the mathematical proof or (on the contrary) does it put logicians into constant challenge for producing the formal proof?
- Lack of interest?
In short, I would like to know if the formalization process is just mechanical work (guided by the mathematical proof) or if some parts require lots of investigation, and even put logicians at dead ends.
ADDITIONAL NOTES (April 12th):
For expressing my doubts clearer, let's take some existing theorem TH and suppose that all the theorems and theories on which this theorem is built (let’s call these "external theorems") are already formalized in the default formal system (ZFC + FOL). If my very basic (amateur) knowledge about axiomatic systems is good enough, the formal deduction for TH will be built directly on the (already existing) formal deductions for the external theorems. Then what is left for formalizing TH is formalizing the arguments in the theorem itself. Let's also suppose that the natural-language mathematical proof for TH has no gaps and it is correct (by extensive peer review).
With those suppositions, I would like to know what kind of difficulties one can face when formalizing the proof:
Has it ever happened (with some existing theorem) that logicians have reviewed the mathematical proof, have found it intuitively correct (as in every peer review) and they are unable to translate it into a formal proof as much as they try? (without having to rewrite completely the argument, of course).
Is the translation quite straightforward or, on the contrary, logicians have to spend days and days of investigation trying to find the way of translating an argument into specific ZFC axioms and FOL inference rules?
I guess that formalization nowadays is a sufficiently mature field and has already provided good experience on the kind of difficulties one can face. Sorry for my insistence. I am not a mathematician, just an amateur of foundations of mathematics, and perhaps I am asking too obvious a question. I have had this curiosity for years and I would like to know.