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