Most adequate logic system to formally prove Euler's identity (and what would the proof look like)?

Question

If we were given the task of proving Euler's identity using a formal logic system, which logic system out there would be the most convenient for such a task? And more or less what would the proof look like, assuming that we are not allowed to "cheat" (i.e. we cannot go the "easy route" of assuming Euler's identity as axiom because ... that's just boring).

Answer 1

The main hurdle to a complete formalization of this in the "usual" way would be formalizing the real numbers and the parts of real analysis that you would need and proving all the basic properties.

One approach to avoid this would be to use formal power series. These can be formalized as infinite sequences of, in this case, complex rationals, say. That is, simply functions $\mathbb N \to \mathbb Q[i]$. The function $a : \mathbb N \to \mathbb Q[i]$ would correspond to the formal power series $\sum_{n=0}^\infty a(n)x^n/n!$. The nice thing about this representation is that differentation is simply $Da(n) = a(n+1)$. You can then define the exponential function and $\sin$ and $\cos$ via "differential equations": $D\exp=\exp$ and $\exp(0)=1$ and $DD\sin=-\sin$, $D\sin(0)=1$, $\sin(0)=0$, $\cos=D\sin$. You'll, of course, need to formalize some of the basic arithmetic of formal power series, but this is much more straightforward than the reals. You'll also need to prove that those "differential equations" give unique solutions, but this isn't that hard. (Alternatively, you could just directly define the sequences.)

Given this, proving $\exp\circ\,iX = \cos + i\sin$ where $X(n)=\begin{cases}1,&\text{if }n=1\\0,&\text{if }n\neq 1\end{cases}$ is fairly straightforward. Just some simple equational reasoning for the most part. All of this would be relatively easy to formalize and do in something like Coq.

Proving $e^{i\pi}=-1$ will be trickier because you can't say $\pi$ in the approach I've suggested. However, you can pick some power series that evaluates to $\pi$ when evaluated at some (complex) rational. Call that power series $p$ and let's say $p$ evaluated at $1$ would be $\pi$. You could then make the composition $\exp\circ\, ip$. Then, the only bit of anything like real analysis you would need to do is prove that the resulting power series when evaluated at $1$ converges to $-1$. That is, given any positive rational $\epsilon$, you can find a natural $N_\epsilon$ such that $|{-1}-\sum_{n=0}^{N_\epsilon}(\exp\circ\, ip)(n)/n!| < \epsilon$. This will likely require some cleverness, though $p$ and $\exp\circ\, ip$ are likely to be fairly well-behaved. For example, it's likely you can arrange it so that you are working entirely with a rational sequence rather than a complex rational sequence, and it's likely you can get decent monoticinity properties. Ultimately, it will just be finding a bound for a sequence of (complex) rationals; nothing crazy should be needed. In particular, everything described is completely computable. If you did use Coq, for example, you'd actually be able to extract a program that when run would actually give you a natural number $N_\epsilon$ given a particular rational $\epsilon$, and then you could actually perform the summation up to the produced $N_\epsilon$ to verify that it is indeed within $\epsilon$ of $-1$.