by Christoph Benzmüller, Manfred Kerber
Abstract:
We re-investigate a proof example presented by George Boolos which perspicuously illustrates Gödel's argument for the potentially drastic increase of proof-lengths in formal systems when carrying through the argument at too low a level. More concretely, restricting the order of the logic in which the proof is carried through to the order of the logic in which the problem is formulated in the first place can result in unmanageable long proofs, although there are short proofs in a logic of higher order. Our motivation in this paper is of practical nature and its aim is to sketch the implications of this example to current technology in automated theorem proving, to point to related questions about the foundational character of type theory (without explicit comprehension axioms) for mathematics, and to work out some challenging aspects with regard to the automation of this proof -- which, as we belief, nicely illustrates the discrepancy between the creativity and intuition required in mathematics and the limitations of state of the art theorem provers.
Reference:
A Lost Proof (Christoph Benzmüller, Manfred Kerber), In Proceedings of the IJCAR 2001 Workshop: Future Directions in Automated Reasoning, pp. 13-24, 2001. (Url (preprint): http://christoph-benzmueller.de/papers/W13.pdf)
Bibtex Entry:
@inproceedings{W13,
Abstract = {We re-investigate a proof example presented by
George Boolos which perspicuously illustrates
G\"odel's argument for the potentially drastic
increase of proof-lengths in formal systems when
carrying through the argument at too low a
level. More concretely, restricting the order of the
logic in which the proof is carried through to the
order of the logic in which the problem is
formulated in the first place can result in
unmanageable long proofs, although there are short
proofs in a logic of higher order. Our motivation in
this paper is of practical nature and its aim is to
sketch the implications of this example to current
technology in automated theorem proving, to point to
related questions about the foundational character
of type theory (without explicit comprehension
axioms) for mathematics, and to work out some
challenging aspects with regard to the automation of
this proof -- which, as we belief, nicely
illustrates the discrepancy between the creativity
and intuition required in mathematics and the
limitations of state of the art theorem provers.},
Address = {Siena, Italy},
Author = {Christoph Benzm{\"u}ller and Manfred Kerber},
Booktitle = {Proceedings of the IJCAR 2001 Workshop: Future
Directions in Automated Reasoning},
Pages = {13-24},
Title = {A Lost Proof},
Note = {Url (preprint):
\url{http://christoph-benzmueller.de/papers/W13.pdf}},
Year = 2001,
}