The mechanization theorem of (ordinary) unordered geometry

Abstract

This is the principal chapter of the book. It aims to prove that if the associated number system of a certain geometry is a number field, i.e., multiplication is commutative, then the proving of theorems whose hypotheses and conclusions can be expressed as polynomial equality relations is mechanizable. This class of theorems will be called theorems of equality type. In fact, this class contains most of the important theorems in elementary geometries though it excludes theorems involving order relations and thus polynomial inequalities in the algebraic relations. However, the latter does not often occur except in high school Euclidean geometry. In modern geometries such as algebraic geometry, the associated number fields are usually the complex field and arbitrary fields of characteristic 0, so no order relation is involved. Therefore it is compatible with the current state of geometry to restrict mechanical proving to theorems that can be expressed by means of only equalities.