8
$\begingroup$

Papadimitriou's "Computational Complexity" states that VALIDITY, the problem of deciding whether a first-order logic (without arithmetic) formula is valid, is recursively enumerable. This follows from the completeness and soundness theorems, which equate VALIDITY and THEOREMHOOD, the latter being the problem of finding a proof for a formula, which had previously been shown to be recursively enumerable.

However, I am not seeing why VALIDITY is not recursive as well, because given a formula $\phi$, one could run two Turing Machines for THEOREMHOOD, one on $\phi$ and the other on $\neg \phi$, concurrently. Since at least one of them is valid, it is always possible to decide whether $\phi$ is valid, or not valid. What am I missing?

Note: this question refers to first-order logic without arithmetic, so Gödel's Incompleteness Theorem does not have a bearing here.

Improve this question
$\endgroup$
1

2 Answers 2

Reset to default
5
$\begingroup$

However, I am not seeing why VALIDITY is not recursive as well, because given a formula $\phi$, one could run two Turing Machines for THEOREMHOOD, one on $\phi$ and the other on $\neg \phi$, concurrently. Since at least one of them is valid, it is always possible to decide whether $\phi$ is valid, or not valid. What am I missing?

This is wrong. A formula $\phi$ is valid iff it holds in all models.

It is not true that at least one of $\phi$ and $\lnot\phi$ must be valid: both might hold in some models, but not all of them.

Trivial example: take FOL with two constant symbols ${\sf a}, {\sf b}$, and the formula $\phi \equiv {\sf a}={\sf b}$. Then $\phi$ holds in some models (those which interpret $\sf a$ and $\sf b$ with the same point), but not all of them (a model can map them to distinct points). And indeed, FOL can not prove ${\sf a} = {\sf b}$ nor ${\sf a} \neq {\sf b}$.

Improve this answer
$\endgroup$
7
  • $\begingroup$ Thanks for figuring out what I was missing, this make sense. But then I guess the set of valid sentences (formulas with no free variables) is recursive then, since in that case either $\phi$ or $\neg \phi$ must be valid. $\endgroup$
    – user118967
    Commented Jul 22, 2016 at 19:51
  • 1
    $\begingroup$ Nope. $\forall x, y.\ x=y$ is true in models with only one element, and false in models with more than one. It is not valid, not is its negation. And no free variables. $\endgroup$
    – chi
    Commented Jul 22, 2016 at 20:02
  • $\begingroup$ Actually, thinking some more about it. If the set of valid sentences is recursive, then it seems I can show that the set of valid formulas is also recursive by doing the following: given a formula $\phi$ with constants $a_1,\dots,a_m$, decide whether sentence $\forall a_1,\dots,a_m \phi$ is valid. If it is, $\phi$ is valid; otherwise, $\phi$ is not valid. Either way, I can decide whether it is in the set of valid formulas. What am I missing now? $\endgroup$
    – user118967
    Commented Jul 22, 2016 at 20:03
  • 1
    $\begingroup$ Also consider $\forall x. \ p(x) \implies q(x)$ -- it holds only in models where predicates $p$ and $q$ are interpreted suitably. In FOL you do have predicates, constant symbols, and function symbols. Even without free variables, you can use predicates, etc. to write complex things which may or may not be true. $\endgroup$
    – chi
    Commented Jul 22, 2016 at 20:09
  • $\begingroup$ Of course, yes. This last point really makes it all clear. Thanks. $\endgroup$
    – user118967
    Commented Jul 22, 2016 at 20:11
1
$\begingroup$

A first-order sentence is valid if it is true in every possible model, i.e., if it is true for all choices of what the relation symbols, function symbols (if there are any) and constant symbols mean. A sentence is provable in some proof system if that proof system contains a proof of the sentence.

Note that provability and validity are two separate concepts, but your attempt to show that validity is recursive actually determines provability, not validity.

Validity and provability are tied together by two further notions:

  • a proof system is sound if everything it can prove is valid, i.e., it only lets you prove things that are actually true;
  • a proof system is complete if it can prove everything that is valid, i.e., it lets you prove all things that are true.

So your proposed method would be fine if you were using a sound and complete proof system: that would mean you could prove exactly all the valid sentences so deciding provability would be the same thing as deciding validity. Unfortunately, Gödel's famous incompleteness theorems say that there is no sound and complete proof system for first-order logic.

So, if your system is sound (it only proves true things) then it is incomplete (it doesn't prove all true things). In particular, there are some sentences $\varphi$ such that neither $\varphi$ nor $\neg\varphi$ has a proof in your system, which means that your Turing machine doesn't halt on input $\varphi$, so it doesn't actually decide any language. Alternatively, if your system is complete (it proves all true things), then it is unsound: it proves at least one false thing and, in fact, since false implies anything, it proves that every sentence is valid. In that case, the Turing machine that you thought was going to decide validity actually decides $\Sigma^*$.

Improve this answer
$\endgroup$
4
  • $\begingroup$ Your use of the incompleteness theorem refers to first-order logic with arithmetic, but my question refers to pure first-order logic, for which there is a sound and complete proof system, according to the book I am reading, and Gödel's Completeness Theorem. So I think my question remains unanswered at this point (I will clarify it). $\endgroup$
    – user118967
    Commented Jul 22, 2016 at 14:01
  • $\begingroup$ Either your proof system is powerful enough to prove statements about first-order arithmetic, in which case Goedel applies, or it isn't, in which case it obviously can't prove all true first-order statements, since it can't prove the ones about arithmetic. $\endgroup$
    – David Richerby
    Commented Jul 22, 2016 at 14:12
  • $\begingroup$ Right. But I am talking about first-order logic without arithmetic, while you are talking about FOL with arithmetic. For FOL without arithmetic, there is indeed a proof system that is sound and complete. The entirety of the question, including the definition of VALIDITY, is with reference to FOL without arithmetic, so in this scenario there is no need to prove statements about arithmetic to establish completeness. $\endgroup$
    – user118967
    Commented Jul 22, 2016 at 15:29
  • 1
    $\begingroup$ Godel's completeness theorem shows that there does exist a sound and complete deductive system for first order logic, such that a first-order sentence is a tautology if and only if it has a finite deduction. The incompleteness theorem shows that there can be sentences which are formally independent of the axioms of your theory: neither the sentence nor its negation is a tautology. As it pertains to arithmetic, the incompleteness theorem shows that the first-order PA axiom schema of induction can fail, unlike the "true" induction axiom (which is a second-order sentence). $\endgroup$
    – Mike Battaglia
    Commented Sep 22, 2017 at 4:55

Your Answer

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

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