Undecidability in ZFC of statements concerning logical validity For every first-order sentence (in some vocabulary) $\varphi$ let us denote by $\varphi^+$ to the sentence (in the vocabulary of ZFC) expressing "$\varphi$ is logically valid (i.e., $\varphi$ is true in all first-order structures)".
My question concerns whether it is possible or not that there is some first-order sentence $\varphi$ such that $\varphi^+$ is undecidable in ZFC (i.e., $\text{ ZFC } \not \vdash \varphi^+$ and $\text{ ZFC } \not \vdash \neg \: \varphi^+$).
 A: Here is a concrete example of a $\phi$ such that neither $\phi^+$ or $\lnot (\phi^+)$ is provable in ZFC. 
Let $\psi$ be the conjunction of the finite number of axioms of Goedel–Bernays set theory (NBG). Note that ZFC does not prove the consistency of NBG or the inconsistency of NBG. This follows from a conservation theorem that a sentence in the language of ZFC is provable in NBG if and only if ZFC proves that sentence; in particular NBG proves the sentence that says "0=1" if and only if ZFC proves that sentence. This conservation theorem is itself formalizable in ZFC, so ZFC proves that Con(NBG) and Con(ZFC) are equivalent. 
Let $\phi$ be $\lnot \psi$. Thus $\phi$ is true in every structure if and only if $\psi$ is false in every structure, and this is also provable in ZFC.  Also, ZFC is able to formalize the completeness theorem, so ZFC proves "$\psi$ is false in every structure if and only if $\psi$ is inconsistent". 
Now, if ZFC proves $\phi$ is logically valid, then ZFC proves "NBG is inconsistent", which is impossible because NBG is consistent and ZFC is $\omega$-consistent. On the other hand, if ZFC proves $\phi$ is not logically valid, then ZFC proves there is a model of $\psi$, which is a model of NBG; this cannot be proved in ZFC because ZFC doesn't prove "NBG is consistent".  This last step again uses the fact that the completeness theorem can be formalized in ZFC. 
As with Levon Haykazyan's answer, I had to assume here that ZFC is ω-consistent to know that ZFC doesn't prove "NBG is inconsistent". Even if ZFC is only consistent, it can't prove "NBG is consistent", because (as above) ZFC can prove that Con(NBG) implies Con(ZFC), and the second incompleteness theorem requires just simple consistency to conclude that ZFC can't prove Con(ZFC). 
A: The answer is yes. If for every $\varphi$, we have either $\rm ZFC \vdash \varphi^+$ or $\rm ZFC \vdash \lnot \varphi^+$, then we can have an algorithm for deciding whether $\varphi$ is logically valid or not. The algorithm will lookup for either a proof of $\varphi^+$ or $\lnot \varphi^+$ and will halt by the assumption. However, such an algorithm cannot exist by Church's theorem.
All this holds, provided ZFC is consistent and $\varphi^+$ can effectively be obtained from $\varphi$ (which I believe it can).
