Proving that a sentence in first-order logic is not valid By the completeness of FOL, one can show that a sentence $S$ in FOL is valid, i.e. that it holds true in every model, by exhibiting a proof of $S$. Such a proof string is a certificate of the validity of $S$.

To show that $S$ is not valid, one can either exhibit a counterexample model in which $S$ doesn't hold, or find a proof that such a model exists, either of which would serve as a certificate.

However, do I understand correctly that while a "certificate of validity" will always exist, that "certificates of invalidity" do not exist in the general case?

In other words, that there can exist $S$ which are not tautologies, and for which a counterexample model exists, but for which one cannot actually construct a counterexample, or a proof of its existence?

This is not a question about the ability of FOL to formalize arithmetic (which Godel proved is impossible), but simply whether or not, in a very foundational sense, it is possible to prove counterexamples exist to FOL sentences in general.
The completeness theorem states, in an equivalent form:


  If a formula $S$ is not valid, then there exists some model $\cal M$ such that $$ {\cal M}\not\models S$$
  or, equivalently
  $${\cal M}\models\neg S $$


This is simply the contraposative of the completeness theorem, as stated on e.g. wikipedia.

This shows that there is always a "certificate of invalidity" as you ask. This is still true if you ask for $\cal M$ to be countable.

However, obviously there is no procedure to compute $\cal M$, by a straightforward argument involving undecidability of Robinson's arithmetic.



Edit: To answer the question of how one might represent such a counter-model:

Unpacking the proof of the completeness theorem shows that such a certificate can be represented by a Herbrand structure, which are the syntactic terms of the language, possibly augmented with constants and function symbols, and recursively enumerable interpretations for the predicate symbols.

In general however, the interpretation of a formula cannot be decided by such a recursive enumeration (but it can be semi-decided).