4
$\begingroup$

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?

Improve this question
$\endgroup$
4
  • 3
    $\begingroup$ 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.) $\endgroup$
    – François G. Dorais
    Commented Aug 19, 2011 at 13:18
  • 2
    $\begingroup$ 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). $\endgroup$
    – Emil Jeřábek
    Commented Aug 19, 2011 at 13:24
  • 2
    $\begingroup$ 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. $\endgroup$
    – Carl Mummert
    Commented Aug 19, 2011 at 19:09
  • $\begingroup$ 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. $\endgroup$
    – abo
    Commented Apr 20, 2012 at 5:22

1 Answer 1

Reset to default
12
$\begingroup$

In principle, this doesn't have to be true, but I believe it is true in practice for all the formal proof systems that have been implemented. In particular, the length ratio is bounded. The ratio of formal proof length to informal proof length is often called the de Bruijn factor, since de Bruijn first raised this issue when working on the Automath system in the 1960's. It's actually surprisingly constant for a given system: not only are formal proof lengths no more than the de Bruijn factor longer than informal ones, they aren't much shorter than that either. However, the de Bruijn factor varies between different systems. Of course, formal proof systems with a low de Bruijn factor are especially attractive for practical use.

Hales wrote a very nice article on formal proofs (http://www.ams.org/notices/200811/tx081101370p.pdf) that has some additional information.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .