A new linear inference of size 8 – The Proof Theory Blog

Linear inferences are propositional tautologies of the form $A\to B$ , where $A$ and $B$ are formulas with at most one occurrence of each propositional variable. These form a $\mathbf{coNP}$ -complete set, but surprisingly little is known about their structure, despite their importance in structural proof theory (and beyond). In this post I will cover some of the background on linear inferences, and present a new ‘independent’ linear inference on 8 variables, which I conjecture is minimal.

Switch, medial and relationships to linear logic

Classical examples of linear inferences are the switch and medial rules from deep inference.

$\begin{array}{rrcl}\mathsf s : & \quad a \wedge (b \vee c) & \to & (a\wedge b)\vee c\\\mathsf m : & \quad (a\wedge b)\vee (c\wedge d) &\to & (a\vee c)\wedge (b\vee d)\end{array}$

These inferences are fundamental in Linear Logic, since they govern the interaction between multiplicative conjunction $\otimes$ and disjunction $\parr$ (in the case of switch) and between the additive conjunction $\with$ and disjunction $\oplus$ (in the case of medial).

The set $\mathsf L$ of all linear inferences was observed to be $\mathbf{coNP}$ -complete by Lutz Strassburger in [1] so it is, in a sense, as rich as all of propositional logic. Interestingly, we also have the following well-known correspondence with linear logic:

Observation 1. $\mathsf L$ coincides with the multiplicative fragments of Blass‘ Game Semantics of linear logic [2] and Japaridze‘s Computability Logic.

Before going any further, I better explain elaborate on how we construct ‘proofs’ using linear inferences.

Composing inferences via rewriting

Construing $\{\mathsf s,\mathsf m\}$ as a rewriting system, modulo associativity and commutativity of $\vee$ and $\wedge$ , we can derive other linear inferences. For instance the following is a derivation, with redexes underlined:

$\begin{array}{rll}a \wedge \underline{b \wedge (c \vee d)} & \to_\mathsf s & \underline{a \wedge ((b \wedge c) \vee d)} \\& \to_\mathsf s & \underline{(a\wedge d) \vee (b \wedge c)} \\& \to_\mathsf m & (a\vee c) \wedge (b \wedge d)\end{array}$

However, notice that we could have also derived this inference using a simple application of the ‘mix’ rule:

$a \wedge b \to a \vee b$

This is not a priori derivable with the system $\{\mathsf s , \mathsf m \}$ above, unless we admit unit equations:

$a \vee \bot = a = a \wedge \top \qquad a\wedge \bot = \bot \qquad a \vee \top = \top$

Henceforth I will assume that all rewriting takes place modulo associativity, commutativity and the unit equations above.

Example 2. (Atomicity of contraction). Any non-atomic instance of $\mathsf c : A \vee A \to A$ may be simplified using the medial rule. When $A$ is a disjunction, it suffices to invoke associativity and commutativity of $\vee$ . The interesting case is when $A$ is a conjunction, for which we may apply the following reduction.

$\begin{array}{rcl}(A \wedge B) \vee (A \wedge B) & \to_{\mathsf m} & \underline{(A\vee A)} \wedge (B\vee B) \\& \to_\mathsf c & A \wedge \underline{(B\vee B)} \\& \to_\mathsf c & A \wedge B\end{array}$

Applying this reduction recursively means that we can simulate each $\mathsf c$ step using only atomic instances. This is a crucial feature of deep inference proof theory, giving rise to proof decompositions that are unavailable in the sequent calculus [3].

$\{\mathsf s,\mathsf m\}$ -independent linear inferences: the quest for minimality

Lutz Strassburger found in [1] a family of linear inferences based on the pigeonhole principle that were independent of switch and medial, even with units. The smallest one there consisted of 36 variables. I improved that in [4] to one on 10 variables:

(1) $\begin{equation*}\begin{array}{lc}& (a \vee (b \wedge b')) \wedge (c \vee d ) \wedge (c'\vee d') \wedge ((e\wedge e') \vee f) \\\to & (a \wedge ( c \vee e)) \vee (c' \wedge e') \vee (b' \wedge d') \vee ((b \vee d) \wedge f)\end{array}\end{equation*}$

Around the same time I had an undergraduate student, Alvin Šipraga, who wrote a program that searches for linear inferences, as well as checking validity and other related tasks [5]. Unfortunately we hit computational barriers even at 7 variables, but we were able to verify the following:

Proposition 3. Any linear inference on 6 variables or fewer is already derivable in ${\mathsf s, \mathsf m}$ (with units).

This raises a rather curious question: what is the smallest linear inference that is independent of switch and medial? By (1) and the proposition above we had narrowed the window to 7-10 variables.

8 years later, an 8-variable inference

Since 2012 a lot has happened. Axiomatising $\mathsf{L}$ via only linear inferences remained open until 2015, when Lutz and I showed the following result in [6] [7], resolving an open problem in Computability Logic and Blass’ game semantics from the early ’90s (see, e.g., [8] for more details):

Theorem 4. $\mathsf L$ cannot be axiomatised by a polynomial-time set of linear inferences, unless $\mathbf{coNP} = \mathbf{NP}$ .

Since then, I became more interested by the graph-theoretic aspects underlying the above result, working with students Cameron Calk and Tim Waring. Independently, Ross Horne has been developing similar ideas in the setting of linear logic, with Lutz Strassburger and Matteo Acclavio, and the whole area of ‘graph-based logics’ is now a rather active topic [9] [10] (albeit one beyond the scope of this post).

In the midst of all this recent activity, I re-examined my old arguments on linear inferences, rather trying to tackle a different question concerning ‘yanking’ in deep inference. In the course of all this, I stumbled upon a new linear inference on 8 variables:

(2) $\begin{equation*}\begin{array}{rl}& (a \vee (b \wedge b')) \wedge (c \vee d) \wedge ((e \wedge e') \vee f) \\\to & (a \wedge (c \vee e)) \vee (b'\wedge e') \vee ((b\vee d) \wedge f)\end{array}\end{equation*}$

One way to obtain this inference is by simply setting $d'=e'=\bar c'$ in (1). This takes care of soundness, but the fact that it is underivable requires a little work. A case analysis shows that there are only two applicable steps to the LHS, both switches, yielding one of the following two formulas:

$((a \wedge (c \vee d)) \vee (b \wedge b') ) \wedge ((e \wedge e') \vee f)\qquad \text{or} \qquad(a \vee (b \wedge b')) \wedge ((e \wedge e') \vee ((c \vee d ) \wedge f))$

Any other step applied to the LHS results in a formula that does not logically imply the RHS. In the same way, there remains no applicable switch or medial step from either of the formulas above. Thus (2) is indeed independent of switch and medial.

Only one question left…

Recall that Proposition 3 tells us that there is no $\{\mathsf s,\mathsf m\}$ -independent linear inference on 6 or fewer variables. Thus only one question remains which, despite its simplicity, remains unresolved:

Question 5. Is there a linear inference of size 7 not derivable in $\{\mathsf s, \mathsf m\}$ (with units), or is (2) above the/a smallest such inference?

My feeling is that this question is probably not so difficult to resolve, either through mathematical or computational techniques (or a mixture), but no one seems to have devoted the effort to answering it. I, for one, would very much welcome a resolution!

References

[1]

L. Straßburger, “Extension Without Cut,” Annals of Pure and Applied Logic, vol. 163, iss. 12, p. 1995–2007, 2012.
[Bibtex]

@article{Str08:extension,
Author = {Stra{\ss}burger, Lutz},
Date-Added = {2008-07-01 11:58:02 +0100},
Date-Modified = {2014-04-12 10:44:11 +0000},
Doi = {10.1016/j.apal.2012.07.004},
Journal = {Annals of {P}ure and {A}pplied {L}ogic},
Keywords = {deep inference},
Number = {12},
Pages = {1995--2007},
Title = {Extension Without Cut},
Url = {http://www.lix.polytechnique.fr/~lutz/papers/psppp.pdf},
Volume = {163},
Year = {2012},
}

[2]

A. Blass, “A Game Semantics for Linear Logic,” Ann. Pure Appl. Log., vol. 56, iss. 1-3, p. 183–220, 1992.
[Bibtex]

@article{Bla92:game-semantics,
author = {Andreas Blass},
title = {A Game Semantics for Linear Logic},
journal = {Ann. Pure Appl. Log.},
volume = {56},
number = {1-3},
pages = {183--220},
year = {1992},
url = {https://doi.org/10.1016/0168-0072(92)90073-9},
doi = {10.1016/0168-0072(92)90073-9}
}

[3]

K. Brünnler, “Two Restrictions on Contraction,” Log. J. IGPL, vol. 11, iss. 5, p. 525–529, 2003.
[Bibtex]

@article{Bru03:two-restr-cntr,
author = {Kai Br{\"{u}}nnler},
title = {Two Restrictions on Contraction},
journal = {Log. J. {IGPL}},
volume = {11},
number = {5},
pages = {525--529},
year = {2003},
url = {https://doi.org/10.1093/jigpal/11.5.525},
doi = {10.1093/jigpal/11.5.525},
}

[4]

A. Das, “Rewriting with Linear Inferences in Propositional Logic,” in 24th International Conference on Rewriting Techniques and Applications (RTA), 2013, p. 158–173.
[Bibtex]

@inproceedings{Das13:rewriting,
Author = {Das, Anupam},
Booktitle = {24th {I}nternational {C}onference on {R}ewriting {T}echniques and {A}pplications ({RTA})},
Date-Added = {2013-03-05 20:52:11 +0000},
Date-Modified = {2014-04-26 16:27:15 +0000},
Doi = {10.4230/LIPIcs.RTA.2013.158},
Editor = {van Raamsdonk, Femke},
Keywords = {deep inference},
Pages = {158--173},
Publisher = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
Series = {Leibniz International Proceedings in Informatics (LIPIcs)},
Title = {Rewriting with Linear Inferences in Propositional Logic},
Url = {http://www.anupamdas.com/items/RewritingWithLinearInferences/RewritingWithLinearInferences.pdf},
Volume = {21},
Year = {2013},
}

[5] A. Šipraga, “An automated search of linear inference rules,” Research project. Supervised by Alessio Guglielmi and Anupam Das, 2012.
[Bibtex]

@article{Sip12:automated-search,
title={An automated search of linear inference rules},
author={Alvin \v{S}ipraga},
year={2012},
journal={Research project. {S}upervised by {A}lessio {G}uglielmi and {A}nupam {D}as},
url={http://arcturus.su/mimir/autolininf.pdf}
}

[6] A. Das and L. Straßburger, “No complete linear term rewriting system for propositional logic,” in 26th International Conference on Rewriting Techniques and Applications (RTA 2015), Dagstuhl, Germany, 2015, p. 127–142.
[Bibtex]

@InProceedings{DasStr15:no-comp-lin-sys,
author =  {Anupam Das and Lutz Stra{\ss}burger},
title =  {{No complete linear term rewriting system for propositional logic}},
booktitle =  {26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
pages =  {127--142},
series =  {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN =  {978-3-939897-85-9},
ISSN =  {1868-8969},
year =  {2015},
volume =  {36},
editor =  {Maribel Fern{\'a}ndez},
publisher =  {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address =  {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2015/5193},
}

[7]

A. Das and L. StraÃŸburger, “On linear rewriting systems for Boolean logic and some applications to proof theory,” Logical Methods in Computer Science, vol. {Volume 12, Issue 4}, 2017.
[Bibtex]

@article{DasStr16:on-lin-rew-sys,
title = {{On linear rewriting systems for Boolean logic and some applications to
proof theory}},
author = {Das, Anupam and StraÃŸburger, Lutz},
url = {https://lmcs.episciences.org/2621},
doi = {10.2168/LMCS-12(4:9)2016},
journal = {{Logical Methods in Computer Science}},
volume = {{Volume 12, Issue 4}},
year = {2017},
}

[8] G. Japaridze, “Elementary-base Cirquent Calculus I: Parallel and Choice Connectives,” FLAP, vol. 5, iss. 1, p. 367–388, 2018.
[Bibtex]

@article{Jap18:el-base-cirq-calc-i,
author = {Giorgi Japaridze},
title = {Elementary-base Cirquent Calculus {I:} Parallel and Choice Connectives},
journal = {{FLAP}},
volume = {5},
number = {1},
pages = {367--388},
year = {2018},
url = {http://collegepublications.co.uk/ifcolog/?00021}
}

[9]

M. Acclavio, R. Horne, and L. Straßburger, “Logic beyond formulas: a proof system on graphs,” in LICS 2020: 35th ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, 2020, pp. 38-52.
[Bibtex]

@inproceedings{AHS20:graph-ll,
title = {Logic beyond formulas: a proof system on graphs},
author = {Acclavio, Matteo and Horne, Ross and Stra{\ss}burger, Lutz},
url = {https://hal.inria.fr/hal-02560105},
booktitle = {{LICS 2020: 35th ACM/IEEE Symposium on Logic in Computer Science}},
address = {Saarbr{\"u}cken, Germany},
publisher = {ACM},
pages = {38-52},
year = {2020},
doi = {10.1145/3373718.3394763},
}

[10] C. Calk, A. Das, and T. Waring, Beyond formulas-as-cographs: an extension of Boolean logic to arbitrary graphs, 2020.
[Bibtex]

@misc{CDW20:graph-bool,
title={Beyond formulas-as-cographs: an extension of Boolean logic to arbitrary graphs},
author={Cameron Calk and Anupam Das and Tim Waring},
year={2020},
url={https://arxiv.org/abs/2004.12941}
eprint={2004.12941},
archivePrefix={arXiv},
primaryClass={cs.LO}
}