How to prove that the dual of the dual of a connected planar graph $G$ is isomorphic to $G$?
Work In progress.
Feel free to contribute filling up the arguments that are incomplete.

Definitions:
Before proving anything we need to make it precise what is it what we are trying to prove.

Planar graph: A graph that can be embedded in $\mathbb{R}^2$.(1)
Plane graph: A planar graph together with a particular embedding $G\hookrightarrow\mathbb{R}^2$. I will call a plane graph just by the name $G$ of the graph itself. We call faces of a plane graph to the connected components of the complement $\mathbb{R}^2\setminus G$. We can also assume the plane graph embedded in the two dimensional sphere $S^2$. That way we don't need to distinguish one of the faces which will be unbounded in the plane.
Polygon: A simple closed path in a graph without a proper closed subpath.
Cut-set: A minimal set of edges of a graph that, if removed, would increase the number of connected components of the graph.
Combinatorial dual: A graph $G^*$ is said to be a combinatorial dual (sometimes also called algebraic dual) of another graph $G$ if there is a bijection between their edges such that the polygons of one of them correspond to the cut-sets of the other, and vice versa. A graph can have no combinatorial duals, or it can have multiple non-isomorphic combinatorial duals.
Geometric dual: A geometric dual $G^*$ of a plane graph $G$ is a graph obtained by placing a vertex on each face of $G$. There is going to be an edge of $G^*$ for each triple $(f_1,f_2,e)$ where $f_1,f_2$ are faces of $G$ such that their closures contain the edge $e$ of $G$. The edge corresponding to this triple will be embedded in such a ways that it connects the vertices of $G^*$ inside $f_1$ and $f_2$. It will be contained in $f_1\cup f_2\cup e$ and intersects $e$ only at one point that it is not a vertex of $G$. For this definition to make sense a couple of results from topology are needed. In particular, two results that are quite intuitive, but very hard to prove. These are Jordan curve theorem and Jordan-Shoenflies theorem. Using these results it can also be proven that the geometric duals of a plane graph are isomorphic. So, we can talk about the geometric dual of a plane graph.

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.

$G^{**}=G$
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.

Geometric double dual.
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.

Combinatorial double dual
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.]
Footnotes:

The topology on the graph is that of a CW-complex.
There are at most two faces incident on an edge. This follows from Jordan-Shoenflies theorem.