Will trilinear logic help with the completeness obstacle?

In the previous blogpost, we have seen that the poset-linear logic is not refutation complete for certain theories in it. This is a major obstacle in building a (possibly polynomial) algorithm that decides satisfiability problem by constructing the set of tautologies, as I explained there. Here I discuss my plan to fix this problem, which is to build a larger logic (I will call it trilinear), and try to show refutation completeness of all theories of poset-linear logic within trilinear logic. Despite trilinear logic being larger, it's only slightly so, and hopefully it will not present an obstacle for the step 3 of the grand strategy.

Trilinear Logic

So let's start with definition of the new trilinear deductive system $\mathcal{TL}$. The formulas are going to be expressions $\alpha\vee\beta\vee\gamma$, where $\alpha,\beta,\gamma$ are (as usual) any generalized literals. The generalized literals are essentially linear equations over $\mathbb{Z}_2$, and for variables $x_1,\ldots,x_n$, they form a vector space with the basis $$\{\bot, \neg x1, \ldots, \neg x_n\},$$ which corresponds to equations $$0=1, x_1=0, \ldots, x_n = 0$$ In that vector space, $\top$ is a zero vector and corresponds to an equation $0=0$.

We will classify formulas by degree, the count of generalized literals which are not $\bot$ in the formula. We will denote $\Omega_k$ all the formulas of degree less or equal than $k$. So the classification is as follows:

• $\Omega_0$ contains only $\bot \vee \bot \vee \bot$, a contradiction.
• $\Omega_1$ contains formulas $\alpha \vee \bot \vee \bot$; these correspond to linear equations.
• $\Omega_2$ contains formulas $\alpha \vee \beta \vee \bot$; these correspond to all formulas in poset-linear logic.
• $\Omega_3$ contains all possible formulas of trilinear logic.

The deduction rules of the trilinear logic will be as follows (for any generalized literals  $\alpha,\beta,\gamma,\delta$):

• Introduction (I): $$\vdash\ \neg \alpha \vee \alpha \vee \bot$$
• Permutation 1 (P1): $$\alpha \vee \beta \vee \gamma \ \vdash\ \beta \vee \alpha \vee \gamma$$
• Permutation 2 (P2): $$\alpha \vee \beta \vee \gamma \ \vdash\ \gamma \vee \beta \vee \alpha$$
• Linearity (L): $$\alpha \vee \beta \vee \gamma,\ \delta \vee \beta \vee \gamma \ \vdash\ \neg (\alpha \oplus \delta) \vee \beta \vee \gamma$$
• Transitivity (T): $$\delta \vee \alpha \vee \gamma,\ \neg \delta \vee \beta \vee \gamma \ \vdash\ \alpha \vee \beta \vee \gamma$$

As you can see, the rules are a straightforward extension of the rules of poset-linear logic, with the rule (P1) as renamed rule (C). The only really new rule is (P2). So for formulas in $\Omega_2$, all rules except (P2) work as their counterparts in poset-linear logic. This is what we want, because the plan is to convert any 2XSAT instance into a theory $\Gamma\subset\Omega_2$, and decide it within trilinear logic.

Important thing to note is that permutation rules (P1) and (P2) imply that any permutation of generalized literals within the formula yields an equivalent formula. This justifies above definition of a degree of the formula.

 

Also importantly, we can derive additional rule of simplification (S): $$\alpha \vee \beta \vee \bot \ \vdash\ \alpha \vee \beta \vee \gamma$$ This let's us specialize any formula, i.e. to replace $\bot$ with an arbitrary generalized literal $\gamma$. (I feel it should be called rule of complication rather than simplification, but the name comes from the traditional axiom of propositional logic $P \rightarrow (Q \rightarrow P)$, of which this is an analogue.)

Most of the logic definitions that were introduced for poset-linear logic (see the paper in the other blogpost) will hold for trilinear logic as well. Specifically, we denote $\overline{\Gamma}$ a deductive closure of theory $\Gamma$, set of all formulas that can be derived using rules (I), (P1), (P2), (L) and (T) starting from $\Gamma$.

Towards Completeness

Because of the 2XSAT reduction described in the previous blogpost, we can convert any 2XSAT instance into a theory $\Gamma\subset\Omega_2$. However, I will sketch the proof here again in a simplified way.

 

We can convert a 3-SAT instance directly to a theory in trilinear logic, just use traditional literals. But such theory is clearly not always in $\Omega_2$. However, it turns out, any theory $\Sigma$ in trilinear logic can be converted to a semantically-equivalent theory $\Gamma\subset\Omega_2$, by adding additional variables. We will use a propositional logic formula: $$\alpha\vee\beta\vee\gamma = (\alpha \vee \neg x \vee \bot) \wedge (\beta \vee (x \oplus \gamma) \vee \bot)$$

It can be verified that it is a suitable choice of $x$ that satisfies right hand side if and only if the left hand side is true. So for each formula $\alpha\vee\beta\vee\gamma \in \Sigma$, we create a fresh variable $x$, and put the two left hand side formulas $\alpha \vee \neg x \vee \bot,\ \beta \vee (x \oplus \gamma) \vee \bot$ in $\Gamma$. That ensures $\Gamma\subset\Omega_2$ and is semantically equivalent to $\Sigma$ on original variables.

First I would like to prove, for a theory $\Gamma\subset\Omega_2$, if a 2nd degree formula $\psi\vee\phi\vee\bot \in \overline{\Gamma}$, then there is a proof of $\psi\vee\phi\vee\bot$ such that every intermediate formula of the proof is also in $\Omega_2$. In other words, the rule (P2) is not required for the proof of 2nd degree sentences in 2nd degree theory. I don't have a full proof of this proposition, but it seems pretty plausible. (Correction: It is false, as the proof of (T) rule from (L) rule shows, below. However, I have a different plan here, which is quite involved and will be detailed later.)

With that, I can reformulate the deduction theorem as follows. Let $\Gamma\subset\Omega_2$ is a theory in trilinear logic, and theory $\Xi = \Gamma \cup \{\xi \vee \bot \vee \bot\}$, for a fixed generalized literal $\xi$. Consider theory $\Delta = \overline{\Xi} \setminus \overline{\Gamma}$, essentially sentences provable in $\Xi$ that require additional assumption $\xi \vee \bot \vee \bot$. Then for any 2nd degree sentence $\psi \vee \phi \vee \bot \in \Delta$, we can prove a sentence $\psi \vee \phi \vee \neg \xi \in \overline{\Gamma}$.

The proof of the deduction theorem should then be straightforward. We can use the fact that since $\Xi\subset\Omega_2$, then any sentence in $\overline{\Xi}$ and thus $\Delta$ has a proof which only needs 2nd degree formulas. We can then enrich axioms of $\Gamma$ with the additional literal $\neg\xi$ at the third slot of the formula, using the rule (S). The additional assumption of $\Xi$ then becomes $\xi \vee \bot \vee \neg\xi$, which is true by the (I) rule. With that, we can prove the $\psi \vee \phi \vee \neg \xi$ by retracing the proof of $\psi \vee \phi \vee \bot$ with the enriched axioms.

Once we have the deduction theorem in this form, we can specialize it to the original formulation where $\bot \vee \phi \vee \bot \in \Delta$ implies $\neg \xi \vee \phi \vee \bot \in \overline{\Gamma}$, and plug this in into the proof of refutation completeness, as described in the paper in the previous blogpost. So the conclusion would be that any theory $\Gamma\subset\Omega_2$ is refutation complete within trilinear logic. This means, if we generate $\overline{\Gamma}$, all the true sentences in it, and won't get a contradiction $\bot \vee \bot \vee \bot$, then $\Gamma$ is a satisfiable instance.

In conclusion, I am going to write the above up in a more formal paper, to see if it all fits together. Then my focus will be to actually produce an algorithm for solving SAT, by generating the $\overline{\Gamma}$ for any polynomial-sized theory $\Gamma\in\Omega_2$. This is the step 3 of the plan. Hopefully (if there is a polynomial algorithm), we will be able to hide the exponential size of $\overline{\Gamma}$ by working with triplets of vector spaces rather than individual formulas (basically, the hope is I can get by with a polynomial number of vector spaces in order to cover $\overline{\Gamma}$).

Odds and Ends

Here are some peculiarities regarding the trilinear logic, which are unrelated to the main goal of proving the refutation completeness of $\Omega_2$ theories.

First, I am a bit torn how to call rule (I). In poset-linear logic, I called it "identity", because it acts as such with respect to rule (T); it is an embodiment of an implication $\alpha\rightarrow\alpha$, while rule (T) is transitivity of implications. I don't want to call it "excluded middle", because that law has some philosophical consequences in the field of logic, and in finite logics such as ours, it seems to be a natural consequence of working with linear equations over $\mathbb{Z}_2$ field. Here I call it "introduction", because it's a kind of opposite of "annihilation", it allows an introduction of a new pair of opposite literals out of vacuum of "nothing".

Second, using rules (L) and (I), we can also derive a right skew rule (R): $$\alpha \vee \beta \vee \gamma\ \vdash\ \alpha \vee (\alpha \oplus \beta) \vee \gamma$$ That means we can add any generalized literal in a formula to another, and we will get an equivalent formula. In other words, the formula is not only closed to any permutation of the slots, but also, given a regular matrix $R\in\mathbb{Z}_2^{3\times 3}$, we can linearly (with respect to $\oplus$, this is a different linearity than in the (L) rule) transform the slots in any formula. Instead of formulas proper, we can consider classes of equivalence with respect to this transformation. The formulas in the class of equivalence than can also be assigned a degree, but it will be a dimension of the linear space (again with respect to $\oplus$) generated by the generalized literals in the formula (so for example $\alpha \vee \alpha \vee \alpha$ has degree of 1, and $\alpha \vee \beta \vee (\alpha\oplus\beta)$ has degree of 2).

Third, without using deduction rule (T), we can derive the following deduction rule: $$\delta \vee \alpha \vee \bot,\ \neg \delta \vee \beta \vee \bot \ \vdash\ \alpha \vee \beta \vee \bot$$ This is essentially (T) rule but on 2nd degree formulas only. We cannot derive full rule (T) because our logic has only three slots for generalized literals in a formula. If we extend our logic to "quadlinear", i.e. formulas $\alpha \vee \beta \vee \gamma \vee \delta$, and add an additional permutation axiom to use the fourth slot, then it is possible to derive (T) rule for 3rd degree formulas in that logic. So in some sense, rules (I) and (L) are more fundamental than rule (T).

Fourth, I suspect that members of $\Omega_k$ are symmetric tensors, and deduction-closed theories of degree $k$ are tensor algebras (which would make them quite amenable computationally), but I am not familiar with tensor algebra enough to be sure as of now.