Finite set with unknown number of elements Does there exist anything like a finite set whose cardinality cannot be established by means of an algorithm or mathematical proof? I think ZFC should have no problem in accomodating such an object, but I can't figure out an example.

Certainly, we can fix a natural number $n>0$ and take the set $$\{x\mid x\leq n\text{ and }\mathsf{ZFC}\text{ is consistent}\}.$$
The set is provably finite. But since we cannot prove, or find algorithmically whether or not $\sf ZFC$ is consistent, we cannot decide whether or not the set is empty, or equals to $\{0,\ldots,n\}$.
The same idea can be applied using any unprovable statement. In fact this can be even simplified to the following case:
Let $\cal L$ be the first-order logic without any extralogical symbols (except equality, which I consider a logical symbol). We write the two statements:
$$\begin{align}
&\varphi_1 = \exists x\forall y(x=y)\\
&\varphi_2 = \exists x\exists y(x\neq y\land\forall z(x=z\lor y=z))
\end{align}$$
And let $\varphi=\varphi_1\lor\varphi_2$. Then if $M$ is a structure satisfying $\varphi$ either $M$ has one element, or it has two elements. But picking an arbitrary $M$ we cannot decide which one is true.
