Interesting logic problems

Question

I've just began a course on logic and learned the following :

• De Morgan's laws

• Normal forms

• How to represent a logical formula (using or, and, not operators) using binary trees

• How to get the conjunctive normal form of a formula

It's obviously not much, but the subject interested me a lot and it was enough to study the 2-SAT and the 3-SAT problems. These two problems were very interesting to study.

I am wondering if there are other classical/interesting algorithms problem in logic (just as 2-SAT, 3-SAT) that can be studied with the little I know about logic?

Answer 1

Rather than going to talk about algorithms and more about SAT, this answer tries to show that there is more than just one kind of logic and that there are also different kinds of approaches.

I won't go into detail much but rather provide a list with some topics and keywords that should form a good basis to do some research:

---

Higher order logic

There are many ways of extending the propositional logic as you know it, for example (first order logic) with the quantifiers $\forall$ and $\exists$ quantifiers.

Keywords: First/second order logic (with equality), free/bound variables, Skolem normal form

---

Type theory

This is basically just another higher order logic, but it's a very rich topic and in my opinion deserves its own category since it plays a special role in CS.

Keywords: $\Pi$-/$\Sigma$-types, subtypes, quotient types, Curry-Howard correspondence, (un)typed $\lambda$-calculus, System F, Martin-Löf type theory, $\lambda$-cube

---

Proof systems

These can vary from classical logic as you know, but can be more abstract working with other syntactical objects than Boolean values or predicates. Generally they define some set $\mathcal{X}$ of objects (formulas/syntax), a truth-assigning function $t: \mathcal{X} \to \{\texttt{false},\texttt{true}\}$ (defines semantics), some notion of proofs and a way to (efficiently) check whether a proof is valid.

Keywords: Completeness & soundness, Gentzen/Hilbert style proofs, resolution calculus, Sequent calculus, Intuitionistic logic, Formal verification, temporal logic etc.

---

If this was not specific enough, here is one thing I found fascinating when I first learned about logic:

$$ \lnot \exists x . \forall y . \bigl ( F(x,y) \longleftrightarrow \lnot F(y,y) \bigr ) $$

The above formula is a tautology (ie. always true) for any domain $\mathcal{U}$ and predicate $F$. Now usually this is not very interesting, but

• define $\mathcal{U}$ as the set of all sets, $F(x,y) = y \in x$ and we get Russell's paradox, or
• define $\mathcal{U}$ some fixed enumeration of $\{0,1\}^\infty$, $F(x,y) = \text{$x$th bit of $y$}$ (now interpreting $\longleftrightarrow$ as equality on $\{0,1\}$) and we get Cantor's diagonalisation argument

which I find quite interesting.

Answer 2

Depending on how 2-SAT and 3-SAT were defined, you might have learned that they may be expressed as decision or search problems. For example, the decision version of 2-SAT is "Given the 2-SAT formula $\varphi$, is $\varphi$ satisfiable?" while the search version asks for a concrete variable assignment under which $\varphi$ is true.

You might have also learned that 2-SAT is efficiently solvable (i.e., there is an algorithm which solves it using a polynomial number of steps in the length of $\varphi$), whereas we do not know whether this is the case for 3-SAT. These observations are related to the open question $\textbf{P} \stackrel{?}= \textbf{NP}$.

Now, to address your question regarding interesting problems. There is a natural generalization of SAT as the counting problem #SAT, that is, "Given the formula $\varphi$, under how many different variable assignments is $\varphi$ true?" As far as we know, this problem is much harder than (3-)SAT since, if you are able to solve it efficiently, then you can also solve (3-)SAT efficiently (namely the formula is satisfiable if and only if it is true under at least one variable assignment).

Another generalization possible in the same sense is MajoritySAT: "Given the formula $\varphi$, is $\varphi$ true under the majority of (i.e., more than half the possible) variable assignments?" As it turns out, being able to solve this and being able to solve #SAT are in a certain sense equivalent: You can use one of the two problems to solve the other efficiently (by making an appropriate series of "questions"). In complexity-theoretic terms, the two problems are polynomial-time (i.e., efficiently) Turing reducible to one another. Solving MajoritySAT using #SAT is relatively straightforward (can you see why?); the other direction is more intricate and an important complexity-theoretic result.

Other generalizations of SAT are quantified Boolean formulas (QBFs), that is, formulas with quantifiers (i.e., "$\forall$" and "$\exists$"). And yet another problem is logical equivalence: "Given the formulas $\varphi_1$ and $\varphi_2$, are they equivalent (i.e., under the same assignment, $\varphi_1$ is true if and only if $\varphi_2$ is true)?" You might want to ponder about whether these are harder or easier to solve (in whatever sense) than the other problems I have previously mentioned.

I hope this qualifies as some suggestions of "interesting" problems. As you can see, one can address many topics in complexity theory (even if indirectly) while only referring to SAT and its generalizations.