Euclid's Postulates: Geometry and Mathematics Explained

Can we see this as a formal system, perhaps a rewriting system, in which proofs are just derivations according to some rules...

Here [link] is a paper that talks about that:

2009-

*A Formal System for Euclid's Elements*- by Jeremy Avigad, Edward Dean, John Mumma.

*" ... we show that our proof system is sound and complete for a standard semantics*

of “ruler-and-compass constructions,” expressed in modern terms. Thus, our presentation

of E is accompanied by both philosophical and mathematical claims: on the one hand, we

claim that our formal system accurately models many of the key methodological features

that are characteristic of the proofs found in Books I through IV of the Elements; and, on

the other hand, we claim that it is sound and complete for the appropriate semantics. "

of “ruler-and-compass constructions,” expressed in modern terms. Thus, our presentation

of E is accompanied by both philosophical and mathematical claims: on the one hand, we

claim that our formal system accurately models many of the key methodological features

that are characteristic of the proofs found in Books I through IV of the Elements; and, on

the other hand, we claim that it is sound and complete for the appropriate semantics. "

An interesting question is: if you can draw a particular diagram (in Euclid's geometry), is that general enough to conclude that something has been proven? Or:

**can a single diagram make us sure that some geometrical property is true?**

*" ... in Euclid’s proofs the construction steps generally precede the deductive conclusions. Thus, the proofs generally split into two phases: in the construction (kataskeue) phase, one carries out the construction, introducing all the objects that will be needed to reach the desired conclusion; and then in the deduction (apodeixis) phase one infers metric and diagrammatic consequences. "*

## No comments:

## Post a Comment