Do we have to define natural numbers in geometry?

Question

I have been thinking about the axiomatization of geometry, and I don't know one thing. Imagine you are defining triangles:

Definition [Triangle]: A triangle is a polygon with 3 sides.

In this case, is it required to define $3$ (and, by extension, $\mathbb{N}$)?

Edit: Maybe I should explain myself more clearly. What I am doing is the following: I have the definition of triangle, now what do I have to define previously so that the definition can be completely understood? In this case, it is clear that I must define what a polygon is and what is a side/vertex of a polygon. I'm wondering whether I have to define "3", but I am not complaining specifically with number 3, it just happens that it is the number I needed to use in this case.

Answer 1

In order to write down definitions and axioms (without which those definitions don't really make sense), you need a logic - that is, a formal language in which you can write these statements.

The standard example is first-order logic, although there are others. And Euclidean geometry is easily formulated in first-order logic.

Now, the natural numbers are implicit in first-order logic! Specifically, defining what a sentence is, and what a proof is, requires us to already understand what a natural number is. And there's really no way around this, and nothing special about first-order logic in this regard (indeed, other logics tend to require more mathematical background - e.g. second-order logic basically requires all of set theory!).

So in order to have a context in which your definitions and axioms can be expressed, and theorems can be proved, you need to already have the natural numbers "in the background".

---

To clarify: it's not that we have to define "$3$" in order to express "A triangle is a polygon with $3$ sides," it's that we already need to understand $\mathbb{N}$ in order to be able to formulate the language within which this definition is being expressed.

This point of view can be seen in more detailed fashion at the answers to this question.

Answer 2

Without attempting to rule on the question I would like to express my opinion that there are two first order logics. There is the naive logic we define using the english language an all that it entails (though I think numbers dont play a big role). There is a second formalized FOL defined within a theory such as ZFC or PA. Clearly, to prove theorems about FOL we need assumptions such as the axiom of choice and those are theorem about this formalized FOL.