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


Consider [Tarski's axiomatization](https://en.wikipedia.org/wiki/Tarski's_axioms) 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*?



What is needed to prove the consistency of Tarski's Euclidean geometry?
In 1999, Harvey Friedman [showed](https://u.osu.edu/friedman.8/files/2014/01/ConsRCF85B15D.23.99-1zxwltk.pdf) 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.


