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.
 A: 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.
A: Let me add what happens in intuitionistic set theory. It's a bit tangential, but you might be interested.
In intuitionistic set theories such as IZF and CZF there are three alternative definitions of "finiteness" that are distinct in these theories but turn out to be equivalent when you add excluded middle.
First note that as in ZF, the natural numbers are implemented in such a way that $n = \{0,\ldots,n-1\}$, so the natural number $n$ is also a set of size $n$.
Let $X$ be a set.
$X$ is finite if there is a natural number $n$ and a bijection $f : n \rightarrow X$.
$X$ is finitely enumerable if there is a natural number $n$ and a surjection $f : n \rightarrow X$.
$X$ is subfinite if it is a subset of a finitely enumerable set.
One can show for intuitionistic set theories that every finite set has a fixed cardinality and moreover one can find the cardinality computably from a proof that a set is finite. You can also find computably an "upper bound" for finitely enumerable sets and subfinite sets.
However, there are examples of finitely enumerable and subfinite sets that have "unknown" cardinality. In fact Asaf's example for ZFC also works as an example of a subfinite set in intuitionistic set theory.
