I find in many references the fact that if $G$ is a connected planar graph, then for any embedding, $G^{**} \cong G$. However, all those references either say that this fact is trivial, or give the proof as an exercice.
I am ok that this is clear on a small graph, with a nice embedding, but how can we prove this property rigorously?
Work In progress.
Feel free to contribute filling up the arguments that are incomplete.
Before proving anything we need to make it precise what is it what we are trying to prove.
It is a theorem of Whitney that a graph is planar if and only if it has a combinatorial dual. Moreover, each combinatorial dual of a planar graph arises as a geometric dual of an embedding of the graph in the plane.
As you see above, this statement can mean different things. It could mean that $G$ is a connected plane graph and we are taking geometric dual a couple of times. It could also mean that $G$ is a planar graph and we are taking geometric dual a couple of times after fixing an embedding. Finally it could mean that we are taking combinatorial dual a couple of times of a connected planar graph.
Note: We also need to use the modern definition of connected in which the empty graph $0$ is not connected. Note that the dual of the empty graph is $K_1$ and the dual of $K_1$ is itself. So, $0^{**}=K_1\not\cong 0$. I am making the clarification because although it is becoming more widespread defining the empty graph as not connected, still not everyone does that.
I think this one is the simplest, assuming that we leave the topological results as known. Assume that $G$ is a plane graph and $G^*$ is its geometric dual. We assume $G^*$ to be a plane graph, which embedding satisfies the properties that we mentioned in the definition above. Let's do induction.
If $G=K_1$ we have that $G^*=K_1$, just another point of the plane, and therefore $G^{**}\cong G$. Then $G^{**}\cong G$.
We want to assume that the theorem is true for all graphs that have smaller number of vertices or edges than $G$. The following two lemmas allow use to construct the isomorphism by removing vertices of $G$ of degree $1$ or edges that are not cut edges. Then we just extend or modify the isomorphism that we have from the inductive assumption on the smaller graph. The lemmas below are quite intuitive, but they make use of Jordan's curve theorem. So, the main annoying thing to write down the arguments is to make it as explicit as possible the point in which this big theorem is used.
Lemma 1: Assume $G$ is connected plane graph with an edge $e$ that is not a cut edge of $G$. Assume that $(G\setminus e)^{**}\cong G\setminus e$. Then $G^{**}\cong G$.
Proof: Since $e$ is not a cut edge, the two faces2 of $G$ incident with $e$ are different. Call those faces $f_1$ and $f_2$. Deleting $e$ from $G$ fuses $f_1$ and $f_2$ into a single face $f$. Faces of $G$ that are adjacent to $f_1$ or $f_2$ become adjacent to $f$ in $G\setminus e$. In the dual, the vertices $f_1^*$ and $f_2^*$ of $G^*$ get replaced by a single vertex $f^*$ of $(G\setminus e)^*$. Any vertex of $G^*$ that is adjacent to $f_1^*$ or $f_2^*$ is adjacent to $(G\setminus e)^*$. Therefore, the function sending $f^*$ to the identification of $f_1^*$ and $f_2^*$ in $G^*/e^*$ and that is the identity on all other vertices is an isomorphism. ... $\square$
Lemma 2: Assume that $G$ is a plane graph that has a vertex $v$ of degree $1$ and that $(G\setminus v)^{**}\cong G\setminus v$. Then $G^{**}\cong G$.
Proof: Since $v$ has degree $1$, then it is adjacent to only one face $f$ of $G$. If $e$ is the edge of $G$ incident on $v$ and $f^*$ is the vertex in $G^*$ that is in $f$, then there is a loop $e^*$ incident on $f^*$ that contains in its interior $v$ and no other vertex of $G$. Here we are implicitly using Jordan's curve theorem. By assumption $(G\setminus v)^{**}\cong G\setminus v$. By jordan's curve theorem the interior of $e^*$ is a face $v^*$ of $G^*$ and this face is adjacent to exactly another face. Therefore, extending the isomorphism of $(G\setminus v)^{**}$ and $G\setminus v$ by sending $v$ to $v^*$ and $v^*$ to $v$ give us an isomorphism of $G^{**}$ and $G$. ... $\square$
To complete the induction observe that we can apply Lemma 1, if the graph has some non cut-edge. If $G$ has no non cut-edges, then it must be a tree. So, we can apply Lemma 2, as long as $G$ has more than one vertex. If it is a tree and has one vertex, then it is $K_1$, which is the base case.
For this we use Whitney's theorem. If $G$ is a connected planar graph and $G^*$ a combinatorial dual, then there is an embedding of $G$ and $G^{*}$ such that $G^*$ is the geometric dual of $G$. From the proof above it follows that $G$ is a geometric dual of $G^*$ and therefore a combinatorial dual of $G^*$. Now assume that $G^{**}$ is a combinatorial dual of $G^*$. Consider an embedding of $G^*$ and $G^{**}$ such that $G^{**}$ is a geometric dual of $G^*$. Using Jordan-Shoenflies theorem we can extend ... [This one seems harder. I don't have a complete plan yet. We probably need to extend the new embedding of $G^{*}$ (in which $G^{**}$ is a geometric dual) to embed also $G$ and show that it is also a geometric dual of $G^{*}$ in this embedding.]
You can probably locate a copy of Bondy and Murty's book Graph Theory with its Applications. While they don't prove it either, they give the following intuition:
Let $G$ be a (connected) plane graph and $G^*$ its dual. There is a natural embedding of $G^*$ in the plane that corresponds to $G$, namely that each vertex $f^*$ in $G^*$ is placed in the corresponding face $f$ of $G$, and each edge $e^*$ is drawn such that it only crosses the corresponding edge $e$ in $G$ and it crosses it exactly once.
