Godel's first incompleteness theorem states that any consistent formal system $F$ within which a certain amount of elementary arithmetic can be carried out is incomplete. I know we can prove Continuum Hypothesis to be independent of ZFC.
Now I wonder if there could be some statement in some formal system $F$ within which a certain amount of elementary arithmetic can be carried out such that the statement can neither be proved to be true nor false nor prove it's independent of the formal system.
We cannot prove $F$ to be consistent within $F$ itself. I thought if such a statement exists, maybe we can add the statement for $F$, maybe this new formal system can prove the statement to be independent? If not, it seems to be very sad that we will just never know something.
Logic is not my focus, and I'm not very familiar with it, just asking out of curiosity, so please forgive my ignorance.
Nonconstructively, such statements should exist, at least for “good” foundational theories. In particular, fix a recursive $\Sigma_1$-sound extension of arithmetic $T$ (in particular, ZFC is such an extension under relatively modest assumptions). Suppose that for all $\Sigma_1$ sentences $\phi$, either $T \vdash \phi$ or $T \vdash ((T \vdash \phi) \to T \vdash \bot)$. In other words, suppose that for all such $\phi$, either $T$ proves $\phi$ or $T$ proves that $\neg \phi$ is relatively consistent with $T$.
In this case, we have an algorithm for computing whether $\phi$ is true. For if $\phi$ is true, then $T$ proves it. If it were also the case that $T$ proves $((T \vdash \phi) \to T \vdash \bot)$, then we would have $T \vdash (T \vdash \bot)$, which contradicts that $T$ is $\Sigma_1$-sound. By contrast, if $\phi$ is false, then $T$ can’t prove $\phi$ by $\Sigma_1$-soundness. Thus, for all such $\phi$, exactly one of the following holds: (1) $T \vdash \phi$ and $\phi$ is true, and (2) $((T \vdash \phi) \to T \vdash \bot)$ and $\phi$ is false. By simply enumerating proofs until we figure out which holds, we can algorithmically decide the truth of $\phi$. However, the problem of determining the truth of a $\Sigma_1$-sentence is algorithmically equivalent to the Halting Problem and is thus undecidable.
I hypothesise this argument can be extended to work with any consistent extension of arithmetic and that it can be made constructive.