I understand that Godel's theorems apply to formal systems and it seems possible to treat Euclidean geometry as a formal system.
My question is more focused on this: let's take Goodstein's theorem as an example, which is defined from natural numbers but to prove it it is not enough to use natural numbers and we must use other tools outside the system (in my opinion this works as an example of the theorem de Gödel), my question is, is there something similar in Euclidean geometry?
(This is clear in some formal system that allows it, since I understand that Tarski proves that Euclidean geometry is complete (or am I wrong?))
Godel's theorem applies to "sufficiently powerful" formal systems, specifically "within which a certain amount of elementary arithmetic can be carried out"
There are formal systems where you can't do arithmetic, for example this one:
Symbols: M, ~ (not)
Complete list of syntactically valid expressions: M, ~M.
Axioms:
A1: M
Rules of inference:
(none)
It's clear this is complete and consistent: Every statement within the system is either proveable, or its negation is. (M is proveable, since it's an axiom, ~M's negation is proveable, there are no other statements to consider).
A more useful example would be propositional logic. Godel's theorem doesn't apply to propositional logic, and every theorem or its negation can be proven (eg, using truth tables).
Tarski wrote down a formalisation of Euclid's geometry and in 1951 proved the existence of an algorithm to prove or disprove propositions. This would not be possible to do if his formalisation of Euclidean geometry were able to express enough arithmetic to be subject to Godel's theorem.