High school geometry proofs and first order logic?

I am a student of logic who recently came across two column geometry proofs which seem to be the bane of many a high-school student. My main question though, is that is there any way of doing these proofs entirely in the language of first order logic and thereby using the methods of natural deduction? Saying "If two angles are complementary, then they amount to 90 degrees" as a justification is way, way too wordy for me and it seems like it could be broken down into the cold, precise and unambiguous deductions of formal logic (it should be a premise translatable into formal logic, which then can be used to derive other statements using the 19+ rules of inference). Thanks guys!

• If you really just want to know if it can be done, the answer is yes. – Git Gud Oct 23 '14 at 10:18
• I think the only problematic part is find a first-order formalization of high school geometry, since Hilbert's axioms contains second-order axiom. (But this problem can be easily avoided, or we can use Tarski axioms.) – Hanul Jeon Oct 23 '14 at 10:45
• High school geometry is probably essential for developing a spatial sense. If you ever try to truly formalize geometry as taught in high school or even a "manageable" subset of it, you will soon discover the myriad details grossed over in textbooks. And that's not necessarily a bad thing. IMHO, formal logic and set theory (suitably simplified) would be a better way to introduce high school students to mathematical proofs. Of course, care must be taken in selecting relatively simple examples and exercises. – Dan Christensen Oct 23 '14 at 16:58
• Larry Wos and some others have done some work on Euclidean geometry in an automated context automatedreasoning.net/docs_and_pdfs/… aarinc.org/Newsletters/107-2014-06.html Here's another source argo.matf.bg.ac.rs/events/2009/fatpa2009/slides/… You can probably find some more. – Doug Spoonwood Oct 23 '14 at 21:24

If I understand you correctly, you are seeking for formal systems of first order logic in which to formalize statements of Euclidean geometry?

There seem to be several ways to do this.

• Firstly, you might formalize statements of Euclidean geometry inside a FOL set theory like ZFC, taking ${\mathbb R}^2$ as the domain of discourse, and prove them there (ultimately building on your set theoretic axioms only).

• Alternatively, you could try to factor this set theoretic approach in two steps:

• Firstly, setting up a system of first order logic particularly made for the formalization of Euclidean geometry, and translating your statement into a formula of that theory, and ...

• ... secondly modelling the theory you chose by the plane ${\mathbb R}^2$ inside your ambient set theory.

This way, a formal proof of your translation in the chosen FOL system for Euclidean geometry will in particular yield a proof of the translation into set theory by the soundness of interpretation.

From the top of my head, I know two FOL formal systems for Euclidean geometry:

Natural deduction is a formal proof calculus, thus we can apply it to any formal theory.

Here is an article on the Goedel's lost letters blog, which deals with elementary identities, which cannot be proven using "high school mathematics", for how "high school mathematics" is defined

Especially see the HSI section.

A formalization of geometry based on some first order axioms can be done. An example of such an axiom system is the system of Tarski. In fact, we have done it. You can find the computer checked proofs here: http://geocoq.github.io/GeoCoq/ If you assume only first order Dedekind cuts, then the models of Tarski's axioms are real closed fields.