2
$\begingroup$

Is second order logic compact and/or decidable? Wikipedia says

Gödel's...compactness theorem, which hold[s] for first-order logic, carr[ies] over to second-order logic with Henkin semantics.

This is makes it sound like second-order logic is normally not compact. What about decidability? What are some good intuitions as to why, or counterexamples as to why not?

$\endgroup$
  • 5
    $\begingroup$ For incompactness, just observe that "the universe is finite" is expressible by a second-order sentence, e.g., by saying that every linear ordering of the universe has a greatest element. Now consider a set of sentences consisting of a second-order sentence saying "the universe is finite" and first-order sentences saying "there are at least two things", "there are at least three things", etc. Every finite subset is satisfiable, but the whole set is not satisfiable. $\endgroup$ – bof Apr 7 '18 at 3:56
  • 1
    $\begingroup$ I'm not sure (that's why I just comment and leave it to the logic experts to post a real answer) but I bet that, given a Turing machine $T,$ you can effectively construct a second-order sentence which is valid if and only if $T$ eventually halts on a blank input, and another second-order sentence which is valid if and only if $T$ runs forever on a blank input. Since the halting problem is undecidable, this would show that the second-order validities are not recursively enumerable. $\endgroup$ – bof Apr 7 '18 at 4:06
  • 2
    $\begingroup$ @bof Not an expert either, but I think that's a good sketch of a solution. And furthermore, first order logic suffices, so by the same token, first order logic is undecidable. $\endgroup$ – spaceisdarkgreen Apr 7 '18 at 4:34
  • 1
    $\begingroup$ Second order logic with full semantics is, of course, undecidable since it contains FOL. In fact, SOL with full semantics is not even semi-decidable since it is possible to express rich arithmetic in SOL without any additional symbols. $\endgroup$ – Daniil Kozhemiachenko Apr 7 '18 at 8:26
  • $\begingroup$ Answer available in every introductory exposition of SOL as well as Second-order and Higher-order Logic. $\endgroup$ – Mauro ALLEGRANZA Apr 7 '18 at 12:33

Your Answer

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

Browse other questions tagged or ask your own question.