The Dennes Room

Event Detail

Abstract: I present a quasi-formal account of the proof method in Euclid’s Elements, based on recent formalizations of Euclid’s diagrammatic arguments ([Avigad et al, 2010], , [Mumma, 2010]). The account is quasi-formal, rather than simply formal, in that it gives geometric content an irreduciable role in Euclid’s proofs. It is quasi-formal, rather than simply informal, in that this role is subject to formal constraints. Inferences which are based on geometric concepts occur within a precisely defined formal framework. I first motivate and explicate the account by contrasting it with Jody Azzouni’s view on the relation of informal proofs to formal proof systems. I then illustrate how the formal framework of the account constrains informal inferences by considering proposition 20 of book I of the Elements, which asserts the triangle inequality. Though arguably obvious from a geometric perspective, the proposition cannot be inferred directly within the framework. One must prove it as Euclid does.

J. Avigad, E. Dean, and J. Mumma. A formal system for euclid’s Elements. Review of Symbolic Logic, 2:700–768, 2009.

J. Mumma. Proofs, pictures, and euclid. Synthese, 175:255–287, 2010