Gödel's Completeness Theorem and satisfiability of a formula in first-order logic

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.

Just replace $\varphi$ with $\lnot \varphi$ in the quoted statement. So:

a formula $\lnot \varphi$ is satisfiable or $\lnot \varphi$ is refutable ($\vdash \lnot \lnot \varphi$).

The point is that $\lnot \lnot \varphi$ and $\varphi$ are logically equivalent in classical logic.

That said, it is difficult to decide which of the two cases happens for a particular formula $\varphi$. Indeed, this is equivalent to being able to decide whether or not a given first-order theory is consistent.