Is it possible to prove that some point belongs to Mandelbrot set? Is this an example of Gödel's theorem?

Question

Everybody knows about Mandelbrot set drawing computer programs. Program takes some point, builds sequence from it, and if found that sequence goes out of circle with 2 radius, then knows that this point does NOT belong to the set.

What about other points?

Sequences from them are infinite. Does this mean that we never can be 100% sure that these points belong to the set?

For example, if we take some point "A" (out of main cardioid)

can we ACTUALLY prove that this point belong to the set?

If not, then can this case be an example of Gödel's theorem, i.e. something true, but unprovable?

UPDATE

Thinking on this topic I thought that some points may be provable, like points inside main cardioid. Hence, there are possible provable theorems about other points too. There are probable numerous of them.

Hence, the incompleteness is escaping again: we can't be sure, that for some point "A" it will be never found a specific proof, that it belongs to the set. And if we have some point, for which the proof was not found for 1000 years, we still can't be sure that this point is unprovable...

Probably it is impossible to provide "problem domain" example of Gödel's theorem at all, because if it would be an example, it would be proven that it was unprovable :)

Answer 1

The Wikipedia article on the Mandelbrot set suggests that the answer to your question is not yet known. In the paragraph Further results, it says:

At present it is unknown whether the Mandelbrot set is computable in models of real computation based on computable analysis.

If the Mandelbrot set turned out not to be computable, then there would indeed be points in the set that could not be proven to be in the set, as you suspect. But that's a big "if".

Answer 2

The answer is mostly yes - there is an algorithm that will determine whether or not most complex numbers are in the Mandelbrot set or not. The algorithm definitely works for all points that lie in the basin of attraction of some attractive orbit and for all points that lie on the boundary of the Mandelbrot set, as proved in this paper. Whether there are any other points or not is equivalent to the hyperbolicity conjecture, which I think is generally assumed to be true.

For concreteness sake, let's consider how we might prove that a point like the one you've labeled $A$ in your diagram can be proved to be in the Mandelbrot set. Again, for concreteness sake, we'll suppose that the point is specifically $c=-0.2-0.75i$ which, as shown below, is right about where you're talking.

The proof that this point lies in the Mandelbrot set rests on two foundations. The first is the following theorem:
The basin of attraction of any attractive orbit under the iteration of a polynomial must contain a critical point of that polynomial.

Now, $f_c(z)=z^2+c$ has exactly one critical point, namely $z=0$, independent of $c$. Thus, if $f_c$ has an attractive orbit for some particular choice of $c$, then the orbit of zero must be bounded, as it must be attracted to the attractive orbit.

The second important issue is simply - exactly what do we mean by an attractive orbit. First, a fixed point $z_0$ (i.e. a point with $f(z_0)=z_0$ is called attractive if $|f'(z_0)|<1$. More generally, a periodic orbit with distinct points $z_1,z_2,\ldots,z_n$ yields $n$ fixed points of $F=f^n$. Thus, the orbit is attracting if those points are attractive fixed points of $F$.

Now, for your point $c=-0.2-0.75\,i$, it's a simple matter to compute that \begin{array}{ccc} 0.137914-0.0456595 i & -0.183064-0.762594 i & -0.748037-0.470792 i \end{array} forms an attractive orbit for your function.