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?

Improve this question
$\endgroup$
3
  • $\begingroup$ Removing excluded middle turns SAT from NP to PSPACE complete, but it's still expressible with Boolean Algebra, with one less rule. $\endgroup$
    – Joey Eremondi
    Feb 3, 2018 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$
    – Nicola Gigante
    Feb 4, 2018 at 2:59
  • $\begingroup$ Now cross-posted to mathoverflow.net/questions/292183/… . $\endgroup$
    – Emil Jeřábek
    Feb 5, 2018 at 8:53

1 Answer 1

Reset to default
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.

Improve this answer
$\endgroup$
4
  • $\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$
    – Nicola Gigante
    Feb 5, 2018 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, 2018 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$
    – Nicola Gigante
    Feb 5, 2018 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, 2018 at 7:33

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.