Does predicate logic's semidecidability follow from the completeness of predicate logic itself (i.e., from Godel's completeness theorem)? From the fact that in predicate logic logical consequence entails derivability follows that every theorem in it has a proof. This is why you can successfully use "Godel numbering" in order to check for every sequence of formulas if it is a proof or not, and, if it is, "write down" the theorem it proves. Of course the decidability of the set of formulas of predicate logic is also a necessary condition. Am I correct?


Basically yes.

But your terminology is a bit wonky.

The theorems of a predicate logic formal system $S$ (in the usual usage) are the closed wffs (sentences) that are provable in your system $S$ from no premisses. Theoremhood in this sense is semidecidable, in the way you suggest. Enumerate all the strings of symbols, carve out those that are well-formed proofs of closed wffs from no premisses, and write down the final wffs -- that's all mechanical for a properly set-up formal system $S$, where we can decide what's a wff etc. And for this result, no appeal to completeness is needed.

The logical truths of a predicate logic formal system $S$ are the closed wffs which are true on all interpretations. Gödel's completeness theorem tells us that every logical truth is a theorem. The relatively trivial soundness result tells that every theorem is a logical truth. Hence, since we can effectively enumerate the theorems, we can effectively enumerate the logical truths, so the property of being a logical truth is semi-decidable, thanks to Gödel's result.

In sum, note that the claim "predicate logic is semidecidable" is not really clear, and is ambiguous between a claim about theoremhood and a claim about logical truth, only one of which depends on completeness.

  • $\begingroup$ "Since theoremhood is semi-decidable, so is the property of being a logical truth, thanks to Gödel's result". I would rather say the right direction is: since logical truths are semidecidable (i.e., effectively numerable) then, thanks to Godel's result, theorems also are. In order to say that logical truths are exactly theorems you need both completeness and soundness don't you? $\endgroup$ – Fishermansfriend Mar 17 '17 at 10:51
  • $\begingroup$ Well, yes, though soundness is kinda trivial. But I've edited to clarify $\endgroup$ – Peter Smith Mar 17 '17 at 10:54
  • $\begingroup$ Also, the worry that underlies the question I asked (the one at the top of the page) is the following: if someone asked me, as an exercise, to show that predicate logic's "semidecidability" follows from Godel's completeness theorem could I answer as I did at the top of the page (that was very rough, and I know that my terminology was not precise, but it was just in order to understand if I grasp how all this works). $\endgroup$ – Fishermansfriend Mar 17 '17 at 11:02
  • $\begingroup$ Not quite, for the reason you gave in your first comment -- effectively enumerating all (and only) the theorems isn't effectively enumerating all (and only) the logical truths if the theory isn't sound. $\endgroup$ – Peter Smith Mar 17 '17 at 11:12
  • 1
    $\begingroup$ Short answer: Formal systems of any real interest come with a formal semantics as well as a formal syntax -- systems of predicate logic are a case in point. $\endgroup$ – Peter Smith Apr 5 '17 at 20:03

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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