## User login## Navigation |
## A Formal System For Euclid's ElementsA Formal System For Euclid's Elements, Jeremy Avigad, Edward Dean, and John Mumma. Review of Symbolic Logic, Vol. 2, No. 4, 2009.
Diagrammatic languages are a perennial favorite discussion topic here, and Euclid's proofs constitute one of the oldest diagrammatic languages around. And yet for hundreds of years (at least since Leibniz) people have argued about whether or not the diagrams are really part of a But was this necessary, or just a contingent fact of the logical machinery available to them? Avigad and his coauthors show the former point of view also works, and that you can do it with very basic proof theory (there's little here unfamiliar to anyone who has read Pierce's book). Yet it sheds a lot of light on how the diagrams in the Elements work, in part because of their very careful analysis of how to read the diagrams -- that is, what conclusion a diagram really licenses you to draw, and which ones are accidents of the specific figure on the page. How they consider these issues is a good model for anyone designing their own visual programming languages. |
## Browse archives## Active forum topics- Code Completion for Generic Programming
- managing closed worlds of symbols via alpha-renaming in loosely coupled concurrent apps
- Why do we need modules at all?
- CFP: International Conference on Live Coding
- Impact of static type systems on productivity of actual programmers: first experiment I've seen documented.
## New forum topics |

## Recent comments

8 min 20 sec ago

3 hours 25 min ago

1 day 1 hour ago

1 day 2 hours ago

1 day 6 hours ago

1 day 7 hours ago

1 day 7 hours ago

1 day 11 hours ago

1 day 17 hours ago

2 days 3 hours ago