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.
['https://cs.stackexchange.com/questions/81507', 'https://cs.stackexchange.com', 'https://cs.stackexchange.com/users/10594/']
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](https://en.wikipedia.org/wiki/G%C3%B6del%27s_completeness_theorem#G.C3.B6del.27s_original_formulation).

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](https://en.wikipedia.org/wiki/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).
Let $\varphi(x)$ be a formula in first-order logic with free variables $x$. If $\varphi(x)$ is not valid, then $\exists x. \neg \varphi(x)$ is valid. Let $\psi$ denote the formula $\exists x. \neg \varphi(x)$. As you stated, if $\psi$ is valid, then there exists a finite proof of $\psi$.

Thus, if $\varphi(x)$ is not valid, then there exists a finite proof that it is not valid: namely, the proof of $\psi$ constitutes such a proof.

Moreover, if $\varphi(x)$ is not valid, then there exists a value of $x$ (say $x\_0$) such that $\varphi(x\_0)$ is false, and in that case there exists a finite proof that $\varphi(x\_0)$ is false (namely, the proof of validity of $\neg \varphi(x\_0)$).

So, the answer to your question is "no; a certificate of invalidity always exists".