11
$\begingroup$

This question might be too elementary for MO, in which case I would gladly move it to math.stackexchange.com

Consider Tarski's axiomatization of Euclidean Geometry. It is stated in the wikipedia page linked and many other places that Tarski proved this first-order theory to be complete and consistent. My question concerns consistency: the proofs I have seen in model-theoretic literature reduce to the triviality that Euclidean geometry has a model in set theory (namely $\mathbb R^2$), so these proofs are actually proofs of the relative consistency of Euclidean Geometry with respect to set theory. But surely there must be a proof of the consistency of Tarski's axioms using only a considerably less powerful theory than set theory (whose consistency may itself be in doubt).

What (hopefully weak) meta-theory is needed to prove that Tarski's axioms are consistent?

For example, what about Tarski's original proof (that I can't track down on the internet)? Or perhaps more recent proofs? More philosophically, is there a proof of the consistency of these axioms that Hilbert would call finitist?

Improve this question
$\endgroup$
3
  • 3
    $\begingroup$ IIRC, Tarski's axioms for Euclidean geometry are equiconsistent with the real closed field axioms, via the usual constructions of defining numbers via the number line and by constructing the plane as pairs of numbers. $\endgroup$
    – user13113
    Commented Feb 5, 2017 at 15:34
  • 1
    $\begingroup$ @Hurkyi, Yes, I believe that. So my question is equivalent to the same question for real closed field. $\endgroup$
    – Joël
    Commented Feb 5, 2017 at 16:02
  • 2
    $\begingroup$ I finally found somewhere on the web a version of Tarski's original proofs (of completed, consistency, etc.). But I was disappointed: they are model-theoretical . In particular the proof of consistency is relative to set theory, and is just the fact that $\mathbb R^2$ is a model, a fact that can by the way without stretching too much be attributed to Descartes. $\endgroup$
    – Joël
    Commented Feb 5, 2017 at 16:04

1 Answer 1

Reset to default
16
$\begingroup$

In 1999, Harvey Friedman showed how to prove the consistency of Tarski's axioms for geometry in EFA. This is Elementary Function Arithmetic, otherwise known as $I\Delta_0(exp)$, a subtheory of PRA with functions bounded by towers of exponentials.

Improve this answer
$\endgroup$
2
  • 3
    $\begingroup$ In other words, the metatheory can be ridiculously weak, and certainly finitist. $\endgroup$
    – Timothy Chow
    Commented Feb 5, 2017 at 15:50
  • 2
    $\begingroup$ Thanks, great answer -- and thanks to Timothy Chow which answers in advance a question I was going to ask. So one can say Hilbert's program was carried out for first order Euclidean Geometry and the theory of real closed field, which is not much as compared as Set Theory, but better than nothing. Now I need to educate myself about EFA. $\endgroup$
    – Joël
    Commented Feb 5, 2017 at 16:02

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .