How is geometry defined using ZFC? I've been trying to get a rigorous understanding for the mathematical concepts I learned in high school. I've been reading about how the real numbers can be constructed from the axioms of ZFC, but I can't find any information on geometry.
I've read about axiomatic formulations of Euclidean geometry, such as Hilbert's, but they seem to introduce new primitive notions.
I've read definitions of Euclidean spaces as sets, but I don't see how it's isomorphic to the synthetic geometry taught in high school. I'd like to be able to know the answers to questions such as:


*

*How is the concept of "angle" defined? 


I thought ZFC was the foundation for most of modern mathematics? Doesn't this mean that it should be possible to describe basic high school geometry topics (circle geometry, cartesian geometry, etc) using ZFC?
My goal is to know that synthetic geometry is isomorphic to something analytically defined using ZFC, so I can know that any proofs in synthetic geometry will also hold in ZFC.
Sorry if this is impossible. I am very ignorant of how mathematics works.
 A: Basically, to develop "formally" a geomety you have two ways; call them analytic and synthetic respectively.
Analytic
This is our "good old" Analytic geometry :

a point in the space is a ordered triple of real numbers : $(x_1,x_2,x_3)$
a line is the totality of points $(x_1,x_2,x_3)$ such that $u_1x_1 + u_2x_2 + u_3x_3 = 0$,
  where at least one $u_j (j = 1,2,3)$ is different from zero
and so on ...

But real numbers are definable in set theory; thus - in principle - you can translate into set-theoretic notation the equation of the line.
Synthetic
See Edwin Moise, Elementary Geometry from an Advanced Standpoint (3rd ed - 1990), page 43 :

space will be regarded as a set $S$; the points of space will be the elements of this set. We will also have given a collection of subsets of $S$, called lines, and another collection of subsets of $S$, called planes. 
Thus the structure that we start with is a triplet : $<\mathcal S, \mathcal L, \Pi>$, where the elements of $\mathcal S, \mathcal L, \Pi$, and  are called points, lines and planes, respectively. 
Our postulates are going to be stated in terms of the sets $\mathcal S, \mathcal L$, and  $\Pi$. 

Here are the first two postulates :

I-0 : All lines and planes are sets of points. 
I-1 : Given any two different points, there is exactly one line containing them [we can "trivially" express the fact that the point $Q$ is contained into the line $l$ with the formula : $Q \in \mathcal S \land l \in \mathcal L \rightarrow Q \in l$ ].

We write $\overline{PQ}$ for the unique line containing $P$ and $Q$.
We define the relation of betweenness between (sic !) three points $P, Q, R$.
Then [see pages 64-65] : if $R,Q$ are two points, the segment between $R$ and $Q$ is the set whose points are $R$ and $Q$, together with all points between $R$ and $Q$.  
The ray $\overrightarrow {AB}$ is the set of all points $C$ of the line $\overline {AB}$ such that $A$ is not between $C$ and $B$. The point $A$ is called the end point of the ray $AB$. 
An angle is the union of two rays which have the same end point, but do not lie on the same line. If the angle is the union of $\overrightarrow {AB}$ and $\overrightarrow {AC}$, then these rays are called the sides of the angle; the [common] end point $A$ is called the vertex.
Finally, you can "close the circle" between this two approaches.
Assuming that we have defined the set $\mathbb N$ of natural numbers inside set theory [but I prefer to say that we have defined a model of the natural number system], and then the set $\mathbb R$ of real numbers, we can use $\mathbb R^3$ and call it : (three-dimensional) space.
Comment
What have we gained so far ? I think nothing more and nothing less than what we already have with Descartes' discovery of analytic geometry : an "embedding" of the euclidean geometry into the "cartesian plane".
Of course, the "basic" set-theoretic language gives us a powerful tool for expressing also geometrical "facts" : we can write $P \in l$ for : "the point $P$ is contained into line $l$", we can write $l_1 \cap l_2 \ne \emptyset$ for "two lines intersect each other", ...
But I think that speaking of "foundation for most of modern mathematics" can be mesleading.
A: 8 years have passed since the question was asked and no one has mentioned euclidean spaces...

*

*If you really want to, you can define functions in terms of sets and prove everything based on the ZFC axioms.


*Euclidean spaces can be used to formulate elementary geometry and can be defined in terms of sets and functions (see this book for more information):
An euclidean space is an affine space with a real and finite-dimensional vector space together with an inner product.
