# Proof system with same complexity as “informal mathematics”?

The Completeness Theorem in first-order logic states that any mathematical validity is derivable from axioms. Hence, any informal mathematical proof (which is rigorous) can be translated into a formal proof in any reasonable proof system. However, this formal proof may be larger than the informal, natural-language proof.

Is there any proof system with the property that all known natural-language proofs have formal proofs with only a constant or polynomial blow-up in the proof length?

• I think you need to clarify what you mean by 'natural-language proof'. In my first interpretation, natural-language proofs are not necessarily first-order, so the answer is clearly 'no'. In my second interpretation, the only feature of natural-language proofs is the free use of definitional extensions of the first-order language. In that case, the answer should be 'yes' provided you include all the definitions and attached lemmas in the length of the natura-language proof. (Note, however, that parsimonious translation would require very heavy use of the cut rule.) – François G. Dorais Aug 19 '11 at 13:18
• Any of the usual proof systems (sequent calculus, Hilbert-style systems, natural deduction systems) have this property, as long as you allow definitions (that is, using the established terminology in proof complexity, the first order version of Extended Frege system does the job). – Emil Jeřábek Aug 19 '11 at 13:24
• To follow up on the remark by François G. Dorais, it is not even obvious to me that the usual natural-language proof system is globally consistent (although it's fine locally as long as we only look at proofs that can be formalized). Beyond the issue with higher-order logic, natural language reasoning also has an ability for paradoxical self-reference that is not present in formal reasoning. – Carl Mummert Aug 19 '11 at 19:09
• I think the last sentence of Carl's comment should end with "standard formal reasoning." It is possible to add self-reference to a formal system (e.g. by adding line numbers, and allowing reference to line numbers) and, if one chooses, furthermore making enough assumptions which allows one to duplicate the Liar's Paradox. Such a system would be inconsistent, but it would still be formal. – abo Apr 20 '12 at 5:22