High school geometry proofs and first order logic?

Question

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!

Answer 1

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

Answer 2

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:

• Tarski's system

• Avigad-Dean-Mumma's system

Answer 3

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

see, http://rjlipton.wordpress.com/2014/07/10/high-school-theorems/

Especially see the HSI section.

Answer 4

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.