What logic can be used express Hilbert's axiomatization of Euclidian geometry?

Question

Can the first order logic be used to express Hilbert axioms for Euclidean geometry as well as all theorems that follow from them? If it is not the case, what logic can be used? Does it have a name? In what way is it more expressive than the first order logic?

Answer 1

The first four groups of Hilbert Axioms can be expressed in first order logic, the occurrences of sets are inessential in the first four groups. An example of a formalization is given in GeoCoq.

The fifth group consists of Continuity axioms:

Axiom of Archimedes:

If AB and CD are any segments then there exists a number n such that n segments CD constructed contiguously from A, along the ray from A through B, will pass beyond the point B.

Axiom of line completeness:

An extension (An extended line from a line that already exists, usually used in geometry) of a set of points on a line with its order and congruence relations that would preserve the relations existing among the original elements as well as the fundamental properties of line order and congruence that follows from Axioms I-III and from V-1 is impossible.

Both axioms of group V require second order logic, where one can quantify over predicates.

The line completeness axiom contains a quantification over the models of I-III and from V-1, so to express it one needs to says "forall predicates incidence, betweeness, congruence, which verify ..."

These two axioms (line completeness and axiom of Archimedes) can also be replaced equivalently by Dedekind cut axiom.

Tarski studied a variant of the Dedekind cut axiom which can be expressed in first order logic using an axiom schema:

Let φ(''x'') and ψ(''y'') be first-order formulae containing no free instances of either ''a'' or ''b''. Let there also be no free instances of ''x'' in ψ(''y'') or of ''y'' in φ(''x''). Then all instances of the following schema are axioms: : $\exists a \,\forall x\, \forall y\,[(\phi(x) \land \psi(y)) \rightarrow Baxy] \rightarrow \exists b\, \forall x\, \forall y\,[(\phi(x) \land \psi(y)) \rightarrow Bxby].$

In fact, most of Hilbert's theorems about geometric figures can be developed in FOF. In the proof of Pascal's theorems, he may use second order logic when it makes use of congruence classes of segment or angles. But this use is inessential because the statement is first-order.

Hilbert needs these second order axioms only to characterize the models of its axioms as cartesian planes over the reals.

Using Tarski's first order variant of Dedekind's cut, the models are the cartesian planes over a real closed field.

If one only wants to prove theorems within ruler and compass geometry, the first order axioms of line/circle or circle/circle continuity are enough.