Linear inferences are propositional tautologies of the form , where
and
are formulas with at most one occurrence of each propositional variable. These form a
-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
.
These inferences are fundamental in Linear Logic, since they govern the interaction between multiplicative conjunction and disjunction
(in the case of switch) and between the additive conjunction
and disjunction
(in the case of medial).
The set of all linear inferences was observed to be
-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.
coincides with the 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 as a rewriting system, modulo associativity and commutativity of
and
, we can derive other linear inferences. For instance the following is a derivation, with underlined:
However, notice that we could have also derived this inference using a simple application of the
rule:
This is not a priori derivable with the system above, unless we admit equations:
Henceforth I will
that all rewriting takes place modulo associativity, commutativity and the unit equations above.Example 2. (Atomicity of contraction). Any non-atomic instance of may be simplified using the medial rule. When
is a disjunction, it suffices to invoke associativity and commutativity of
. The interesting case is when
is a conjunction, for which we may apply the following reduction.
Applying this reduction recursively means that we can simulate each 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].
-independent linear inferences: the quest for minimality
Lutz Strassburger found in [1] a family of based on the 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 :
(1)
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
(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 via only linear inferences remained open until 2015, when Lutz and I showed the 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.
cannot be axiomatised by a polynomial-time set of linear inferences, unless
.
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
in deep inference. In the course of all this, I stumbled upon a new linear inference on 8 variables: (2)
One way to obtain this inference is by simply setting 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:
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 -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
(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
![[doi]](https://prooftheory.blog/wp-content/plugins/papercite/img/external.png)
[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},
}
![[doi]](https://prooftheory.blog/wp-content/plugins/papercite/img/external.png)
[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}
}
![[doi]](https://prooftheory.blog/wp-content/plugins/papercite/img/external.png)
[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},
}
![[doi]](https://prooftheory.blog/wp-content/plugins/papercite/img/external.png)
[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},
}
[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}
}
[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},
}
![[doi]](https://prooftheory.blog/wp-content/plugins/papercite/img/external.png)
[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},
}
[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}
}
![[doi]](https://prooftheory.blog/wp-content/plugins/papercite/img/external.png)
[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},
}
[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}
}