2
$\begingroup$

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.

Improve this question
$\endgroup$

2 Answers 2

Reset to default
3
$\begingroup$

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).

Improve this answer
$\endgroup$
11
  • $\begingroup$ How do you actually get a certificate from this though? What would a certificate for M look like, and how could you represent it? $\endgroup$
    – Mike Battaglia
    Sep 22, 2017 at 15:46
  • $\begingroup$ @MikeBattaglia I've added some explanation of what a certificate might look like. The crucial keyword is "Herbrand model". Everything is undecidable though, obviously, so I'm not quite sure what you would want. $\endgroup$
    – cody
    Sep 22, 2017 at 18:05
  • $\begingroup$ I'm trying to figure out exactly where in the process decidability breaks down. Is it that a finite-length certificate is simply not guaranteed to exist, period? Or is it that a finite-length certificate is guaranteed to exist, but that it is not possible to verify that it actually is a counter-model to your sentence? (I believe you're saying #2 here, but I'm not sure.) $\endgroup$
    – Mike Battaglia
    Sep 22, 2017 at 18:12
  • $\begingroup$ Regarding the Herbrand structure, I guess this is in general an infinite-length construction, right? You can make it finite length only in some cases, such as if the universe can be represented via some recursive algorithm. $\endgroup$
    – Mike Battaglia
    Sep 22, 2017 at 18:53
  • $\begingroup$ The Herbrand universe is always "recursive", in the sense that it is countable and has a simple description (as a set of terms). But the equalities (or other relations) induced by the axioms need to be deduced from the axioms, and so are only enumerable and not recursive. $\endgroup$
    – cody
    Sep 23, 2017 at 2:09
0
$\begingroup$

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".

Improve this answer
$\endgroup$
9
  • $\begingroup$ You are saying that if the formula is not valid, its negation must be valid? I am very confused here, as I thought that wasn't true. $\endgroup$
    – Mike Battaglia
    Sep 22, 2017 at 4:44
  • $\begingroup$ What about sentences which hold only in some models, and for which the negation also holds only in some models? Consider some Diophantine equation which first-order PA is too weak to prove has no solution, and consider the sentence asserting that the equation has no solution. This sentence is not valid in first-order PA because nonstandard models exist in which it doesn't hold. But its negation is also not valid because the negation doesn't hold in the standard model. $\endgroup$
    – Mike Battaglia
    Sep 22, 2017 at 5:01
  • $\begingroup$ @D.W. If you allow constants $a,b$ in your language, $a=b$ is a formula $\phi$, which is not valid, but $\exists x,\neg\phi$ is just $\neg\phi$ and is not valid as well. I suspect you are implicitly assuming that there are no constants or function symbols in your language. $\endgroup$
    – cody
    Sep 22, 2017 at 14:09
  • $\begingroup$ @cody This assumption doesn't help, because it doesn't work for $\forall x, P(x)$ any better than for $a = b$. And without predicate symbols other than equality you have $\forall x \forall y, x = y$... $\endgroup$
    – Alexey Romanov
    Sep 22, 2017 at 15:02
  • $\begingroup$ @cody, In the formula $a = b$, the free variables are $a,b$. If $a = b$ is not valid, then $\exists a,b . \neg (a = b)$ is valid. If $\varphi$ is the formula $a=b$, then $\psi$ is the formula $\exists a,b . \neg (a = b)$. Take a look at my answer again? I think I handle that. $\endgroup$
    – D.W. ♦
    Sep 22, 2017 at 15:38

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.