<p>The example you gave extends as follows:</p>

<ul>
<li>SAT for arbitrary lattices (meaning, is a given formula satisfiable in some lattice) is polynomial-time decidable</li>
<li>SAT for modular lattices is Turing undecidable:
<em>Freese, Ralph</em>, <a href="http://dx.doi.org/10.2307/1998318" rel="nofollow noreferrer"><strong>Free modular lattices</strong></a>, Trans. Am. Math. Soc. 261, 81-91 (1980). <a href="https://zbmath.org/?q=an:0437.06006" rel="nofollow noreferrer">ZBL0437.06006</a>.</li>
<li>SAT for Boolean algebras is NP-complete</li>
</ul>

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

CC BY-SA 3.0
2018-02-05T06:55:45.613Z
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).
Nicola Gigante
CC BY-SA 3.0
2018-02-05T07:12:48.327Z
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)
Bjørn Kjos-Hanssen
CC BY-SA 3.0
2018-02-05T07:25:25.030Z
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?
Nicola Gigante
CC BY-SA 3.0
2018-02-05T07:33:27.733Z
Easiest probably to just Google/Bing it and then go to the Wikipedia link that comes up
Bjørn Kjos-Hanssen
CC BY-SA 3.0
2018-02-05T06:21:44.963Z
2018-02-05T06:21:44.963Z
Bjørn Kjos-Hanssen
<p>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.</p>

<p>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?</p>

<p>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?</p>

CC BY-SA 3.0
2018-02-03T22:11:16.120Z
Removing excluded middle turns SAT from NP to PSPACE complete, but it's still expressible with Boolean Algebra, with one less rule.
Joey Eremondi
CC BY-SA 3.0
2018-02-04T02:59:25.347Z
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?
Nicola Gigante
CC BY-SA 3.0
2018-02-05T08:53:56.520Z
Now cross-posted to https://mathoverflow.net/questions/292183/connections-between-algebraic-semantics-and-computational-complexity-of-a-logic .
Emil Jeřábek
<cc.complexity-theory><lo.logic><algebra>
Connection between algebraic logic and computational complexity of logics?
Nicola Gigante
# Connection between algebraic logic and computational complexity of logics?

(Asked by: username_0 on 2018-02-03)

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?

**Tags:** cc.complexity-theory, lo.logic, algebra
> **Comments:**
> **username_1**: Removing excluded middle turns SAT from NP to PSPACE complete, but it's still expressible with Boolean Algebra, with one less rule.  
> **username_0**: 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?  
> **username_2**: Now cross-posted to https://mathoverflow.net/questions/292183/connections-between-algebraic-semantics-and-computational-complexity-of-a-logic .  

---

## 1 answers

### Answer by username_3 on 2018-02-05. Score: 4 | Accepted answer

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**](http://dx.doi.org/10.2307/1998318), Trans. Am. Math. Soc. 261, 81-91 (1980). [ZBL0437.06006](https://zbmath.org/?q=an:0437.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.

> **Comments:**
> **username_0**: 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).  
> **username_3**: 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)  
> **username_0**: 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?  
> **username_3**: Easiest probably to just Google/Bing it and then go to the Wikipedia link that comes up  

---

