3
$\begingroup$

I'm learning a bit about algebraic logic and I was wondering how knowing the algebraic semantics of a given logic might help the study of the logic itself from a computational point of view.

In particular, is there any example of a complexity (or decidability) result for the satisfiability problem for some logics that was obtained by reasoning about its algebraic semantics?

For example, the semantics of propositional logic can be given in terms of boolean algebras. Is there any connection between them and the fact that SAT is decidable and $NP$-complete?

$\endgroup$
  • $\begingroup$ Removing excluded middle turns SAT from NP to PSPACE complete, but it's still expressible with Boolean Algebra, with one less rule. $\endgroup$ – jmite Feb 3 '18 at 22:11
  • 1
    $\begingroup$ As I said, I’m learning those things, so I thought you need Heyting algebras to give semantics to intuitionistic logic. What am I missing? $\endgroup$ – gigabytes Feb 4 '18 at 2:59
  • $\begingroup$ Now cross-posted to mathoverflow.net/questions/292183/… . $\endgroup$ – Emil Jeřábek Feb 5 '18 at 8:53
4
$\begingroup$

The example you gave extends as follows:

  • SAT for arbitrary lattices (meaning, is a given formula satisfiable in some lattice) is polynomial-time decidable
  • SAT for modular lattices is Turing undecidable: Freese, Ralph, Free modular lattices, Trans. Am. Math. Soc. 261, 81-91 (1980). ZBL0437.06006.
  • SAT for Boolean algebras is NP-complete

So while modular lattices are in between Boolean algebras and arbitrary lattices, they are the most complicated.

$\endgroup$
  • $\begingroup$ Thanks. Any reference about the first result of the list? Anyway, can the NP-completeness result be connected to properties of boolean algebras themselves? Like "this logic is NP-complete because its algebraic semantics is XYZ" (I know this would be too broad to be an actual theorem, but you get the point). $\endgroup$ – gigabytes Feb 5 '18 at 6:55
  • 1
    $\begingroup$ Well, the fact that it's in NP has to do with how the free Boolean algebra on finitely many generators is always finite (whereas that's not true for free modular lattices) $\endgroup$ – Bjørn Kjos-Hanssen Feb 5 '18 at 7:12
  • $\begingroup$ That was the kind of comments I was looking for. But I lack the background to fully understand yours. Do you have any reference to this kind of topics? $\endgroup$ – gigabytes Feb 5 '18 at 7:25
  • $\begingroup$ Easiest probably to just Google/Bing it and then go to the Wikipedia link that comes up $\endgroup$ – Bjørn Kjos-Hanssen Feb 5 '18 at 7:33

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

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