Gödel's original proof of the Completeness Theorem for first-order logic proves it in the equivalent form :
a formula $\varphi$ is satisfiable or $\varphi$ is refutable (i.e.$\vdash \lnot \varphi$).
Assuming classical logic, someone can exhibit an example of first-order formula $\varphi$ for which we are not able to decide if it is provable (i.e.$\vdash \varphi$) or if there is a counterexample (i.e.$\lnot \varphi$ is satisfiable) ? In other words, a formula $\varphi$ for which we are not able to decide if it is valid or not ?
Added March 1st
Following Carl's answer, an example of a sentence like the above can be costructed in the following way; ref to Elliott Mendelson, Introduction to Mathematical Logic (4th ed – 1997), Ch.4: Axiomatic Set Theory [page 225-on] :
(i) let $\mathcal N$ the formula obtained by the conjunction of the following axioms for $\mathsf {NBG}$ : Axiom T, Axiom D, Axiom N, Axioms B1-B7, Axiom U, Axiom P, Axiom S, Axiom I, Axiom AC, Axiom Reg (no axiom shemas), after having "unwinded" all the set-theoretic definitions (like : $\emptyset$ and $\subseteq$) and after having replaced in the above formulas all occurences of $\in$ with a binary predicate symbol $R$;
(ii) let $RH$ the formula expressing in the language of $\mathsf {NBG}$ the Riemann Hypothesis, subject to the same "translation".
Then :
$\mathcal N \land \lnot RH$
is an example of formula for which we do not know if it is satisfiable or if it is refutable.
Best Answer
Decidability - which means computability in this question - is always about a set of formulas. It does not make much sense to look for a single formula the satisfiability of which is not decidable.
This is because, if the formula is satisfiable, then the program that always outputs "Yes" will be correct, and if the formula is not satisfiable, the program that always output "No" will be correct. So, in a somewhat trivial way, the satisfiability of each individual formula is decidable. But this is so trivial that we don't view it as interesting.
What is true is that, when we consider sufficiently rich languages of first-order logic, there is no single program that, given an arbitrary formula, will decide whether that formula is satisfiable or not. The key point is that this is a problem involving an infinite set of formulas; the same program would have to decide correctly whether each of them is satisfiable.
It is still the case, of course, that there are individual statements of first-order logic such that we do not know whether those statements are satisfiable or not. For example, let $C$ be any unsolved conjecture, expressed in the language of set theory. Let $A$ be the conjunction of the finite set of axioms for NBG set theory (which is stronger than ZFC set theory). Then we will not know whether the formula $A \land \lnot C$ is satisfiable or not. We could take $C$ to be the Riemann hypothesis or any other unsolved problem that can be formalized in set theory.
The key point is that there are foundationally strong theories that have finite axiom systems, so we can code the entire axiom system as a single formula. That is also the key fact behind the proof that first-order logic is not decidable when the language is sufficiently rich.