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 TL. The formulas are going to be expressions α∨β∨γ, where α,β,γ are (as usual) any generalized literals. The generalized literals are essentially linear equations over Z2, and for variables $x_1,\ldots...