pith. sign in

arxiv: 2505.13284 · v2 · submitted 2025-05-19 · 💻 cs.LO

Intuitionistic BV (Extended version)

Matteo Acclavio , Lutz Strassburger This is my paper

Pith reviewed 2026-05-22 14:27 UTC · model grok-4.3

classification 💻 cs.LO
keywords intuitionistic logicdeep inferencecut eliminationnon-commutative connectiveBV logicIMLLsequent calculusNML
0
0 comments X

The pith

IBV is an intuitionistic version of BV whose MLL fragment is exactly IMLL, equipped with a deep inference system that admits cut elimination.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces IBV as an intuitionistic counterpart to BV. It achieves this by ensuring that the logic, when restricted to the connectives of multiplicative linear logic, coincides precisely with the established intuitionistic multiplicative linear logic IMLL. A deep inference proof system is supplied for IBV, and cut elimination is proved for that system. The construction further yields INML by removing associativity from the non-commutative sequence connective, together with a cut-free sequent calculus for INML.

Core claim

We present the logic IBV, which is an intuitionistic version of BV, in the sense that its restriction to the MLL connectives is exactly IMLL, the intuitionistic version of MLL. For this logic we give a deep inference proof system and show cut elimination. We also show that the logic obtained from IBV by dropping the associativity of the new non-commutative seq-connective is an intuitionistic variant of the recently introduced logic NML. For this logic, called INML, we give a cut-free sequent calculus.

What carries the argument

The deep inference proof system for IBV, which applies rules at any depth and incorporates the non-commutative seq connective to extend the MLL fragment while preserving the IMLL restriction.

If this is right

  • Cut elimination holds in the deep inference system for IBV.
  • The MLL fragment of IBV coincides with IMLL.
  • Dropping associativity of the seq connective produces the logic INML.
  • INML is equipped with a cut-free sequent calculus.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The cut-elimination result implies that IBV is consistent in the usual sense that falsehood is not derivable without premises.
  • The same deep-inference technique could be applied to introduce non-commutative features into other fragments of intuitionistic linear logic.
  • Proof search in these systems might be implemented by directly using the cut-free sequent calculus for INML.

Load-bearing premise

The specific rules and the new seq connective are chosen so that IBV restricts exactly to IMLL on the MLL connectives.

What would settle it

A sequent using only MLL connectives that is derivable in the IBV deep inference system but not in IMLL, or a cut in an IBV derivation that cannot be eliminated.

Figures

Figures reproduced from arXiv: 2505.13284 by Lutz Strassburger, Matteo Acclavio.

Figure 1
Figure 1. Figure 1: Proof systems discussed in this paper. The ones in the boxes are new. a unit’. That means that we no longer have 𝐴 ⊳ I ≡ 𝐴 ≡ I ⊳ 𝐴, but only 𝐴 ⊸ 𝐴 ⊳ I and 𝐴 ⊸ I ⊳ 𝐴. In classical BV the triple ⟨⊗, O, I⟩ forms an isomix category [7], and the con￾nective ⊳ is a degenerate linear functor (in the sense of [4]), that is, it validates the following implication.4 ( (𝐴 ⊳ 𝐵) ⊗(𝐶 ⊳ 𝐷)) ⊸ ( (𝐴 ⊗ 𝐶) ⊳ (𝐵 ⊗ 𝐷)) (1) We … view at source ↗
Figure 2
Figure 2. Figure 2: Inference rules for system IBV 𝑎 ⊸ 𝑎 ai• ↑ • I I ⊳ 𝐴 u ⊳ ↑ • 𝐴 𝐴 ⊳ I u ⊲ ↑ • 𝐴 I ⊗ 𝐴 u ⊗ ↑ .......... 𝐴 I ⊸ 𝐴 u⊸ ↑ ............ 𝐴 (𝐴 ⊳ 𝐶) ⊗(𝐵 ⊳ 𝐷) q ◦ ↑ ◦ (𝐴 ⊗ 𝐵) ⊳ (𝐶 ⊗ 𝐷) (𝐴 ⊳ 𝐶) ⊸ (𝐵 ⊳ 𝐷) q • ↑ • (𝐴 ⊸ 𝐵) ⊳ (𝐶 ⊸ 𝐷) [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Additional rules for SIBV. A formula is unit-free if it contains no occurrences of I. In order to define the deep inference rules for our systems, we need to define contexts, which are formulas where one atom occurrence is replaced by a hole [·]. In the intuitionistic setting we have to distinguish between positive contexts, denoted by 𝑃[·], and negative contexts, denoted by 𝑁[·], depending on the position… view at source ↗
Figure 4
Figure 4. Figure 4: Derivability of i ◦ ↓ in IBV. 𝑃 u ⊗ ↓ ................................................... 𝑃 ⊗ © ­ ­ ­ ­ ­ « I i ◦ ↓ ◦ 𝑄 q • ↓ • 𝑃 ⊸ 𝑄 ª ® ® ® ® ® ¬ s ◦ L ◦ © ­ « 𝑃 ⊸ 𝑃 i • ↑ • I ª ® ¬ ⊸ 𝑄 u⊸ ↑ ........................................ 𝑄 𝑅 u⊸ ↓ ..................................................... © ­ ­ ­ ­ ­ « I i ◦ ↓ ◦ 𝑆 ⊸ 𝑆 q ◦ ↓ ◦ 𝑅 ª ® ® ® ® ® ¬ ⊸ 𝑅 s • L • 𝑆 ⊗ © ­ « 𝑅 ⊸ 𝑅 i • ↑ • I ª ® ¬ u ⊗ ↑ ........… view at source ↗
Figure 5
Figure 5. Figure 5: Using i • ↑ to derive q ◦ ↑ and q • ↑ paper because (i) the unit I is only half a unit for the ⊳ connective, and the rules u ⊳ ↓ , u ⊲ ↓ , u ⊳ ↑ , u ⊲ ↑ would be needed anyway, (ii) it might be confusing to the reader to have implicit currying, and (iii) making everything explicit makes derivations easier to read. 3 Properties of the Systems In this section we show some basic properties of IBV and SIBV. Fo… view at source ↗
Figure 6
Figure 6. Figure 6: Cases for the splitting lemma. – If ⊢IBV (𝐴 ⊳ 𝐵) ⊸ 𝐾, then there are formulas 𝐾𝐴 and 𝐾𝐵 such that 𝐾𝐴 ⊳ 𝐾𝐵 𝐾 and 𝐴 ⊸ 𝐾𝐴 and 𝐵 ⊸ 𝐾𝐵 . Proof. The proof is by induction on the derivation, considering the bottom-most (non-dotted) rule instance in the derivation. In [PITH_FULL_IMAGE:figures/full_fig_p008_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Derivations for admissibility of ai• ↑ and q ◦ ↑ . The case for q • ↑ is similar. All subderivations exist by splitting and context reduction lemmas. Proof (for Theorem 7). We can remove all instances of the up-rules in a deriva￾tion, starting with a topmost one. Given such an instance r↑, we apply context reduction and splitting to the premise or r↑ (once for u ⊳ ↑ , u ⊲ ↑ , u ⊗ ↑ , u⊸ ↑ , and twice for a… view at source ↗
Figure 8
Figure 8. Figure 8: Left: Rules for IMLL Right: The cut rule and the generalized axiom of a sequent are interderivable in IBV using the rules com⊗ and asso⊗ . This allows us to define a sequent Γ ⊢ 𝐵 to be derivable in IBV if any of its formula interpretations is derivable in IBV. Lemma 15. Let r be an inference rule of IMLL. If every premise of and instance of r is derivable in IBV, then so is its conclusion. Proof. For the … view at source ↗
Figure 9
Figure 9. Figure 9: ai↓-rules for IBV− . If r ∈ {s ◦ L ,s ◦ R ,s • R ,s • L }, then we have either the following derivations ax 𝐴 ⊢ 𝐴 ax 𝐵 ⊢ 𝐵 ax 𝐶 ⊢ 𝐶 ⊸L + ⊗R (𝐴 ⊸ 𝐵), 𝐶, 𝐴 ⊢ 𝐵 ⊗ 𝐶 ⊸R + ⊗L (𝐴 ⊸ 𝐵) ⊗ 𝐶 ⊢ 𝐴 ⊸ (𝐵 ⊗ 𝐶) ax 𝐴 ⊢ 𝐴 ax 𝐵 ⊢ 𝐵 ax 𝐶 ⊢ 𝐶 2 × ⊸L 𝐴, 𝐵 ⊸ 𝐶, 𝐴 ⊸ 𝐵 ⊢ 𝐶 ⊸R + ⊗L 𝐴 ⊗(𝐵 ⊸ 𝐶) ⊢ (𝐴 ⊸ 𝐵) ⊸ 𝐶 (6) (ii) is shown by induction on the context, where both statements are proved simultaneously. ⊓⊔ Theorem 17. IBV is a conser… view at source ↗
Figure 10
Figure 10. Figure 10: Rules for the system BV− . The side condition for the ≡-rule is that 𝐴 and 𝐵 are equivalent modulo the equivalence relation generated by the relation ≡, defined below the dashed line. Similarly, the BV−-formulas are the BV formulas without the unit, i.e., they are generated from the countable set A of atoms and the binary connectives par (O), tensor (⊗), and seq (⊳), using the following grammar: 𝐴, 𝐵 ≔ 𝑎 … view at source ↗
Figure 11
Figure 11. Figure 11: Sequent calculus for unit-free NML− . Proof. By induction on 𝐴, proving at the same time that 𝐴 is negative iff 𝐴 ⊥ is in the image of (·)♭ . ⊓⊔ Proof (for Theorem 18). Let us first assume we have a derivation of 𝐴 in IBV− . We can apply the mapping (·)♭ to every formula in that derivation and obtain a valid BV− derivation. For the converse, it suffices to observe that all rules of BV− either preserve the… view at source ↗
read the original abstract

We present the logic IBV, which is an intuitionistic version of BV, in the sense that its restriction to the MLL connectives is exactly IMLL, the intuitionistic version of MLL. For this logic we give a deep inference proof system and show cut elimination. We also show that the logic obtained from IBV by dropping the associativity of the new non-commutative seq-connective is an intuitionistic variant of the recently introduced logic NML. For this logic, called INML, we give a cut-free sequent calculus.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 2 minor

Summary. The paper introduces IBV, an intuitionistic version of BV such that its MLL fragment coincides exactly with IMLL. It supplies a deep-inference proof system for IBV together with a cut-elimination argument. It further defines INML by dropping associativity of the seq connective, presents INML as an intuitionistic variant of NML, and gives a cut-free sequent calculus for INML.

Significance. If the cut-elimination and restriction results hold, the work supplies new deep-inference and sequent systems for intuitionistic non-commutative linear logic. This strengthens the proof-theoretic toolkit for resource-sensitive and concurrency-related logics and provides concrete cut-free calculi that could support further metatheoretic or computational investigations.

major comments (1)
  1. [§4] §4 (Restriction to IMLL): the manuscript asserts that the MLL fragment of IBV is exactly IMLL, but the argument that the new seq rules introduce no extra MLL derivations when restricted to multiplicative connectives is only sketched; an explicit lemma showing that every IBV derivation using only ⊗, ⅋, 1, ⊥, and the intuitionistic implication reduces to an IMLL derivation (and conversely) is needed to make the central definitional claim load-bearing.
minor comments (2)
  1. [§3] Notation for the seq connective and its rules should be introduced with an explicit side-by-side comparison to the corresponding rules in BV and NML to improve readability.
  2. [§5] The cut-elimination proof for IBV is given in deep inference; a brief remark on whether the same techniques adapt directly to the sequent calculus of INML would clarify the relationship between the two systems.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the careful reading of the manuscript and for the positive recommendation of minor revision. We address the major comment below.

read point-by-point responses

  1. Referee: [§4] §4 (Restriction to IMLL): the manuscript asserts that the MLL fragment of IBV is exactly IMLL, but the argument that the new seq rules introduce no extra MLL derivations when restricted to multiplicative connectives is only sketched; an explicit lemma showing that every IBV derivation using only ⊗, ⅋, 1, ⊥, and the intuitionistic implication reduces to an IMLL derivation (and conversely) is needed to make the central definitional claim load-bearing.

    Authors: We agree that an explicit lemma would make the restriction claim fully rigorous and load-bearing. In the revised manuscript we will insert a new lemma (Lemma 4.3) in §4 whose statement is precisely the one requested: every IBV derivation whose conclusion and all premises use only the MLL connectives ⊗, ⅋, 1, ⊥ together with the intuitionistic implication can be transformed into an IMLL derivation, and conversely every IMLL derivation embeds directly into IBV. The proof proceeds by induction on derivation height, showing that any application of a seq rule in the MLL fragment is either redundant (when the seq is not principal) or can be replaced by a combination of the existing MLL rules of IBV that coincide with those of IMLL. We will also add a short paragraph explaining why the seq rules cannot create new MLL derivations. This change is straightforward and does not affect any other results. revision: yes

Circularity Check

0 steps flagged

No significant circularity; derivation is self-contained

full rationale

The paper introduces IBV via an explicit deep-inference rule set whose MLL fragment is shown by direct comparison to coincide with the rules of IMLL; cut elimination is then established by a separate inductive argument on the full system. The restriction property follows from the absence of seq-interactions when only MLL connectives appear, rather than from any fitted parameter, self-referential definition, or load-bearing self-citation. All central claims rest on the supplied rules and the cut-elimination proof, which are independent of the target result and externally verifiable.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 2 invented entities

The claims rest on the definitional choice that IBV restricts to IMLL on MLL connectives and on standard background results about deep inference and sequent calculi; no numerical parameters or new physical entities are introduced.

axioms (1)
  • domain assumption Restriction of IBV to MLL connectives is exactly IMLL
    This assumption is used to characterize the logic as the intuitionistic version of BV.
invented entities (2)
  • IBV logic no independent evidence
    purpose: Intuitionistic non-commutative logic extending BV
    Newly defined combination of existing frameworks.
  • INML logic no independent evidence
    purpose: Non-associative variant of IBV
    Obtained by dropping associativity of the seq connective.

pith-pipeline@v0.9.0 · 5607 in / 1299 out tokens · 135907 ms · 2026-05-22T14:27:22.614350+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

31 extracted references · 31 canonical work pages

  1. [1]

    A Graphical Proof Theory of Logical Time

    Matteo Acclavio, Ross Horne, Sjouke Mauw, and Lutz Straßburger. A Graphical Proof Theory of Logical Time. In Amy P. Felty, editor,7th International Confer- ence on Formal Structures for Computation and Deduction (FSCD 2022), volume 228 ofLeibniz International Proceedings in Informatics (LIPIcs), pages 22:1–22:25, Dagstuhl, Germany, 2022. Schloss Dagstuhl ...

    work page 2022

  2. [2]

    Proofs as execution trees for the𝜋-calculus, 2025

    Matteo Acclavio and Giulia Manara. Proofs as execution trees for the𝜋-calculus, 2025

    work page 2025

  3. [3]

    Formulas as processes, deadlock-freedom as choreographies

    Matteo Acclavio, Giulia Manara, and Fabrizio Montesi. Formulas as processes, deadlock-freedom as choreographies. In Viktor Vafeiadis, editor,Programming Languages and Systems, pages 23–55, Cham, 2025. Springer Nature Switzerland

    work page 2025

  4. [4]

    Deep inference and probabilisticcoherencespaces.Applied Categorical Structures,20(3):209–228,2012

    Richard Blute, Prakash Panangaden, and Sergey Slavnov. Deep inference and probabilisticcoherencespaces.Applied Categorical Structures,20(3):209–228,2012

    work page 2012

  5. [5]

    A local system for classical logic

    Kai Brünnler and Alwen Fernanto Tiu. A local system for classical logic. In R. Nieuwenhuis and A. Voronkov, editors,LPAR 2001, volume 2250 ofLNAI, pages 347–361. Springer, 2001

    work page 2001

  6. [6]

    A purely logical account of sequentiality in proof search

    Paola Bruscoli. A purely logical account of sequentiality in proof search. InInter- national Conference on Logic Programming, pages 302–316. Springer, 2002

    work page 2002

  7. [7]

    Proof theory for full intuitionistic linear logic, bilinear logic, and mix categories.Theory and Applications of categories, 3(5):85–131, 1997

    J Robin B Cockett and Robert AG Seely. Proof theory for full intuitionistic linear logic, bilinear logic, and mix categories.Theory and Applications of categories, 3(5):85–131, 1997

    work page 1997

  8. [8]

    A system of interaction and structure.ACM Trans

    Alessio Guglielmi. A system of interaction and structure.ACM Trans. Comput. Logic, 8(1):1–es, January 2007

    work page 2007

  9. [9]

    Non-commutativity and MELL in the calculus of structures

    Alessio Guglielmi and Lutz Straßburger. Non-commutativity and MELL in the calculus of structures. In Laurent Fribourg, editor,Computer Science Logic, CSL 2001, volume 2142 ofLNCS, pages 54–68. Springer-Verlag, 2001

    work page 2001

  10. [10]

    A system of interaction and structure V: the exponentials and splitting.Math

    Alessio Guglielmi and Lutz Straßburger. A system of interaction and structure V: the exponentials and splitting.Math. Struct. Comput. Sci., 21(3):563–584, 2011. Intuitionistic BV 17

    work page 2011

  11. [11]

    Private Names in Non-Commutative Logic

    Ross Horne, Alwen Tiu, Bogdan Aman, and Gabriel Ciobanu. Private Names in Non-Commutative Logic. In Josée Desharnais and Radha Jagadeesan, editors,27th International Conference on Concurrency Theory (CONCUR 2016), volume 59 ofLeibniz International Proceedings in Informatics (LIPIcs), pages 31:1–31:16, Dagstuhl, Germany, 2016. Schloss Dagstuhl – Leibniz-Ze...

    work page 2016

  12. [12]

    De morgan dual nominal quantifiers modelling private names in non-commutative logic.ACM Trans

    Ross Horne, Alwen Tiu, Bogdan Aman, and Gabriel Ciobanu. De morgan dual nominal quantifiers modelling private names in non-commutative logic.ACM Trans. Comput. Logic, 20(4), jul 2019

    work page 2019

  13. [13]

    SystemBVwithouttheequalitiesforunit

    OzanKahramanoğulları. SystemBVwithouttheequalitiesforunit. InC.Aykanat, T. Dayar, and I. Körpeoğlu, editors,19th International Symposium on Computer and Information Sciences, ISCIS 2004, volume 3280 ofLecture Notes in Computer Science, pages 986–995. Springer-Verlag, 2004

    work page 2004

  14. [14]

    A System of Interaction and Structure III: The Complexity of BV and Pomset Logic

    Lê Thành D˜ ung Nguyên and Lutz Straßburger. A System of Interaction and Structure III: The Complexity of BV and Pomset Logic. working paper or preprint, 2022

    work page 2022

  15. [15]

    BV and Pomset Logic are not the same

    Lê Thành D˜ ung Nguyên and Lutz Straßburger. BV and Pomset Logic are not the same. In Florin Manea and Alex Simpson, editors,30th EACSL Annual Conference on Computer Science Logic (CSL 2022), volume 216 ofLeibniz International Pro- ceedings in Informatics (LIPIcs), pages 3:1–3:17, Dagstuhl, Germany, 2022. Schloss Dagstuhl – Leibniz-Zentrum für Informatik

    work page 2022

  16. [16]

    PhD thesis, Université Paris VII, 1993

    Christian Retoré.Réseaux et Séquents Ordonnés. PhD thesis, Université Paris VII, 1993

    work page 1993

  17. [17]

    Pomset logic as a calculus of directed cographs

    Christian Retoré. Pomset logic as a calculus of directed cographs. In V. M. Abrusci and C. Casadio, editors,Dynamic Perspectives in Logic and Linguistics, pages 221–247. Bulzoni, Roma, 1999. Also available as INRIA Rapport de Recherche RR-3714

    work page 1999

  18. [18]

    Pomset logic: The other approach to noncommutativity in logic

    Christian Retoré. Pomset logic: The other approach to noncommutativity in logic. Joachim Lambek: The Interplay of Mathematics, Logic, and Linguistics, pages 299– 345, 2021

    work page 2021

  19. [19]

    Linearlambdacalculusanddeepinference

    LucaRoversi. Linearlambdacalculusanddeepinference. InProceedings of the 10th International Conference on Typed Lambda Calculi and Applications, TLCA’11, page 184–197, Berlin, Heidelberg, 2011. Springer-Verlag

    work page 2011

  20. [20]

    Higher-Order Causal Theories Are Models of BV-Logic

    Will Simmons and Aleks Kissinger. Higher-Order Causal Theories Are Models of BV-Logic. In Stefan Szeider, Robert Ganian, and Alexandra Silva, editors,47th In- ternational Symposium on Mathematical Foundations of Computer Science (MFCS 2022), volume 241 ofLeibniz International Proceedings in Informatics (LIPIcs), pages 80:1–80:14, Dagstuhl, Germany, 2022. ...

    work page 2022

  21. [21]

    PhD thesis, Technische Universität Dresden, 2003

    Lutz Straßburger.Linear Logic and Noncommutativity in the Calculus of Struc- tures. PhD thesis, Technische Universität Dresden, 2003

    work page 2003

  22. [22]

    A system of interaction and structure II: The need for deep inference.Logical Methods in Computer Science, 2(2):1–24, 2006

    Alwen Fernanto Tiu. A system of interaction and structure II: The need for deep inference.Logical Methods in Computer Science, 2(2):1–24, 2006. 18 M. Acclavio, L. Straßburger A Proof for Footnote 5 Proposition 27.If(I⊳ 𝐴)⊸𝐴and(𝐴 ⊳I)⊸𝐴were provable inIBV, then ⊳and ⊗ would collapse (in the sense that𝐴 ⊳ 𝐵and𝐴 ⊗ 𝐵would be logically equivalent formulas). Pro...

    work page 2006

  23. [23]

    The bottom of the derivation is of the following form 𝐾1 ⊸ ©­ « (𝐾2 ⊸(𝐴 2 ⊗ 𝐵2)) ⊗(𝐴 1 ⊗ 𝐵1) s◦ R ◦𝐾2 ⊸((𝐴 2 ⊗ 𝐵2) ⊗(𝐴 1 ⊗ 𝐵1)) ª® ¬........................................................................................... (𝐾1 ⊗ 𝐾2)⊸((𝐴 1 ⊗ 𝐴2) ⊗(𝐵 1 ⊗ 𝐵2)) and we can use the inductive hypothesis to get formulas𝐾𝐿 and𝐾 𝑅 such that there are derivations o...

    work page

  24. [24]

    The bottom of the derivation is of the following form 𝐾1 ⊸ ©­ « (𝐴 1 ⊗ 𝐵1) ⊗((𝐴 2 ⊗ 𝐵2)⊸𝐾 2) s◦ L ◦((𝐴 1 ⊗ 𝐵1)⊸(𝐴 2 ⊗ 𝐵2))⊸𝐾 2 ª® ¬.............................................................................................. ((𝐴 1 ⊗ 𝐴2)⊸(𝐵 1 ⊗ 𝐵2))⊸(𝐾 1 ⊗ 𝐾2) and we can use the inductive hypothesis to get formulas𝐾𝐿 and𝐾 𝑅 such that there are derivations...

    work page

  25. [25]

    The bottom of the derivation is of the following form ©­ « ((𝐾 1 ⊸(𝐴 1 ⊗ 𝐵1))⊸(𝐴 2 ⊸𝐵 2)) s• L •(𝐾1 ⊗((𝐴 1 ⊗ 𝐵1)⊸(𝐴 2 ⊸𝐵 2))) ª® ¬ ⊸𝐾 2 ..................................................................................................... (𝐴 1 ⊗ 𝐴2)⊸(𝐵 1 ⊸𝐵 2)⊸(𝐾 1 ⊸𝐾 2) and we can use the inductive hypothesis to get formulas𝐾𝐿 and𝐾 𝑅 such that there are d...

    work page

  26. [26]

    The bottom of the derivation is of the following form ©­ « (𝐴 1 ⊗ 𝐵1)⊸((𝐴 2 ⊸𝐵 2) ⊗ 𝐾2) s• R •((𝐴 1 ⊗ 𝐵1)⊸(𝐴 2 ⊸𝐵 2)) ⊗ 𝐾2 ª® ¬ ⊸𝐾 1 .............................................................................................. ((𝐴 1 ⊗ 𝐴2)⊸(𝐵 1 ⊸𝐵 2))⊸(𝐾 2 ⊸𝐾 1) and we can use the inductive hypothesis to get formulas𝐾𝐿 and𝐾 𝑅 such that there are derivatio...

    work page

  27. [27]

    If one of these two formulas is absent, then it suffices to consider a different instance of the rulesq◦ R (if𝐾 2 does not occur), andsq◦ L (if𝐾 3 does not occur)

    We only discuss the case on the left where𝐾2 and𝐾 3 are present. If one of these two formulas is absent, then it suffices to consider a different instance of the rulesq◦ R (if𝐾 2 does not occur), andsq◦ L (if𝐾 3 does not occur). If both of them do not occur, then it suffices to consider an instance ofref◦. The case on the right is similar because of assoc...

    work page

  28. [28]

    If one of these two formulas is absent, then it suffices to consider a different instance of the rulesq• R (if𝐾 2 does not occur), orsq• L (if 𝐾3 does not occur)

    As in the previous case, we only discuss the case on the left in which𝐾1 and𝐾 2 are present. If one of these two formulas is absent, then it suffices to consider a different instance of the rulesq• R (if𝐾 2 does not occur), orsq• L (if 𝐾3 does not occur). If both of them do not occur, then it suffices to consider an instance ofref •. The case on the right...

    work page

  29. [29]

    If one of these two formulas does not occur, then it suffices to consider a different instance ofsq◦ R (if𝐾 2 does not occur), andsq◦ L (if𝐾 3 does not occur)

    As in the previous cases, we only discuss the case on the left in which𝐾1 and 𝐾2 are present. If one of these two formulas does not occur, then it suffices to consider a different instance ofsq◦ R (if𝐾 2 does not occur), andsq◦ L (if𝐾 3 does not occur). If both of them do not occur, then it suffices to consider an instance ofref ◦. The rightmost case is s...

    work page

  30. [30]

    If⊢ IBV 𝑃[ 𝐴], then there is a formula𝐾and derivations 𝐾⊸𝑋 P𝑋 𝑃[𝑋] and P𝐴 𝐾⊸𝐴 for any formula𝑋

    work page

  31. [31]

    Proof.By induction on the structure of each context — see (3)

    If⊢ IBV 𝑁 [ 𝐴], then there is a formula𝐾and derivations 𝑋⊸𝐾 P𝑋 𝑁 [𝑋] and P𝐴 𝐴⊸𝐾 for any formula𝑋. Proof.By induction on the structure of each context — see (3). We here only discuss here the cases for the positive contexts, since the arguments for the same cases for the negative contexts are analogous, with some minor differences in the (polarities of the...

    work page