Pith. sign in

REVIEW 2 major objections 4 minor 58 references

Linear Realisability over nets: multiplicatives (long version)

T0 review · 2 major / 4 minor · reviewed 2026-08-12 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read The central claim is that a cut-free net proves a sequent exactly when it survives interaction with every opponent in every interpretation basis.

desk verdict A genuinely new and mostly careful realisability model for MLL/MLL* over nets, but the stated completeness for MLL rests on Proposition 188, whose proof is too sketchy to check as written. read the letter →

arxiv 2411.17486 v1 pith:NM5ETVLZ submitted 2024-11-26 cs.LO

Adrien Ragot , Thomas Seiller , Lorenzo Tortora de Falco This is my paper · ORCID
classification cs.LO MSC 03F5203B47
keywords linearlogicrealisabilityorthogonalityproofnetsdaimonscuteliminationcompletenessmultiplicativefragment
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

This paper aims to show that provability in multiplicative linear logic can be recovered purely from interaction between untyped proof nets. It builds a realisability model in which formulas denote types, sets of nets closed under bi-orthogonality, and two nets are orthogonal when their cut-elimination interaction reaches the empty daimon. The novelty is a cut-elimination procedure for generalised axioms: a daimon link cut against a tensor or par link gets new rewriting rules, making the daimon an adaptive opponent that never stops answering. The paper proves adequacy and completeness for MLL✠, multiplicative linear logic with generalised axioms, and then derives completeness for standard MLL. The upshot is that geometrical correctness and provability correctness both become interactively testable in one uniform model.

What carries the argument

The machinery is orthogonality defined by cut elimination on untyped multiplicative nets, extended by non-homogeneous rules for cuts between a daimon link $\langle \vdash_{\text{✠}} p_1,\dots,p_n\rangle$, a generalised axiom with no premises and any number of conclusions, and a tensor or par link. Two nets interact by pairing their ordered conclusions with cut links; they are orthogonal if the interaction rewrites to the empty daimon $\text{✠}_0$. The load-bearing rewriting properties are collected in Proposition 30: strong normalisation, a factorisation of every reduction as multiplicative steps followed by non-multiplicative steps, and commutation lemmas saying that irreversible (✠/par)-cuts can be delayed while reversible (✠/⊗)-cuts can be anticipated. These lemmas justify the orthogonality relation and the type constructions that carry the model.

What would settle it

Try to construct a cut-free net $S$ and sequent $\Gamma$ such that $S\in \llbracket \Gamma\rrbracket_B$ for every basis $B$ while $S$ does not represent an MLL✠ proof of $\Gamma$; Theorem 85 says none exists. A more local check is to search for a reduction sequence where the factorisation $\to^* = \to^*_{\text{mult}}\cdot \to^*_{\neg\text{mult}}$ fails, or where a $(\text{✠}/\otimes)$-cut cannot be commuted left of another step without changing the normal form.

Watch

Extended reading notes

Core claim

The central claim is Theorem 85: for a cut-free net $S$ and a sequent $\Gamma$, if $S$ belongs to $\llbracket \Gamma \rrbracket_B$ for every interpretation basis $B$, then $S$ proves $\Gamma$ in MLL✠. Theorem 88 is the same statement for MLL, restricted to nets whose daimons are binary and atomically labelled. With the adequacy theorem, this makes the orthogonality model complete as well as adequate: the nets realising a sequent in all bases are exactly the proof nets of the system. The proof runs through a particular basis, $1$, which maps each atom to the bi-orthogonal closure of the single-output daimon, and through a decomposition argument showing that any realiser in such a basis must be testable by the sequent and therefore correct.

Load-bearing premise

The model collapses if any of the rewriting lemmas for the new non-homogeneous cut elimination fails—specifically strong normalisation, the factorisation into multiplicative then non-multiplicative steps, or the commutation properties that let reversible (✠/⊗)-cuts be anticipated and irreversible (✠/par)-cuts be delayed.

Editorial extensions

If this is right

  • A cut-free net that realises a sequent in every basis must be an actual proof, so the model rules out universal realisers that are geometrically correct but not provable.
  • Completeness transfers from MLL✠ to MLL, so the same interactive criterion recognises ordinary multiplicative proofs once daimons are restricted to binary, atomically labelled links.
  • The factorisation of cut elimination gives correctness testing a phase structure: multiplicative interactions can be resolved first and daimon interactions afterwards, which is what allows tests to probe provability as well as geometry.
  • For cut-free nets in an approximable basis, testability by a sequent and correct typeability coincide, aligning the semantic notion of realisability with the syntactic notion of proof.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Beyond the paper, the same orthogonality recipe could be tried on richer fragments of linear logic, with the cut-elimination commutation lemmas as the main obstacle; the paper itself treats only multiplicatives.
  • The completeness proof for MLL deliberately exploits geometrically incorrect opponents, suggesting that incorrectness can serve as a computational resource for separating provability from mere geometry rather than as noise to be filtered out.
  • A concrete extension would be to map out which pairs of non-equivalent sequents are separated by specially chosen non-approximable bases; the paper shows one such pair, $X,X^\perp$ versus $X,Y$, leaving the general separation question open.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 4 minor

Summary. The paper introduces a realisability model for multiplicative linear logic (MLL and MLL✠) based on orthogonality between untyped proof nets with daimon (generalised axiom) links. The central construction is a cut-elimination system for nets that includes homogeneous and non-homogeneous cuts, an orthogonality relation defined by reduction to the empty daimon, and a type interpretation of formulas. The authors prove adequacy (Theorem 64) and two completeness theorems: Theorem 85 for MLL✠ and Theorem 88 for MLL, the latter applying to nets whose daimons are binary and atomically labelled. The proof is supported by a long appendix ending with a dependency graph. The main claimed contribution is that interactive realisability over nets characterises provability exactly.

Significance. The claimed result is significant: if the proof is completed, this is the first complete realisability model for multiplicative linear logic over general proof nets, and the use of non-homogeneous cut elimination to separate geometrical from provability correctness is a genuine novelty. The paper is careful in several respects: it proves the rewriting properties of the new cut-elimination system in detail (Proposition 30 and Appendix B), it provides a proof dependency graph (Figure 14), and the completeness direction is not obtained by fitting parameters but by a bootstrap through the daimon basis 1 and the independent Danos-Regnier criterion. My main concern is concentrated on one load-bearing lemma, Proposition 188, whose proof is a sketch; the surrounding material appears sound.

major comments (2)
  1. [Appendix G.6, Proposition 188, base case] The base case of the proof of Proposition 188 ends with the sentence 'Since furthermore ⋂_B ⟦X⟧_B is empty it follows that ⟦X⟧_B‖⟦Y⟧_B is also empty thus the proposition hold.' This is logically incoherent. For each basis B, ⟦X⟧_B is a type, and for the approximable basis 1 it contains ✠1, so each of these types is non-empty at a fixed basis. Emptiness of the intersection over all bases does not imply emptiness of the parallel composition at a fixed basis; indeed the parallel composition of two non-empty types contains the parallel sum of any two of their elements, and is generally non-empty. The argument therefore does not establish the claimed splitting a∈⟦X⟧_B and b∈⟦Y⟧_B.
  2. [Appendix G.6, Proposition 188, main step] The decisive step of the proof of Proposition 188 is the assertion 'one can easily check that a✠‖b✠ is not orthogonal to s⊲⊳s′ for all s′∈⟦g(B)⟧_B', together with the unproved equivalence 'a✠∈⟦g(A)⟧_B iff a∈⟦A⟧_B'. This is precisely the polarisation/deadlock analysis needed to generalise Figure 15 and Remark 90 from atomic dualities to arbitrary variable-disjoint formulas; it is not a routine check, because orthogonality requires reduction to a single ✠0 and component-wise convergence is insufficient (parallel pairs may get stuck at ✠0‖✠0). Since Proposition 188 is used directly in Lemma 189 and then in the tensor case of Theorem 88, the proof of the MLL completeness theorem (Theorem 88) is incomplete as written.
minor comments (4)
  1. [Figure 3 and Section 1.2] The displayed multiplicative cut-elimination rule contains a typo: the result is written as '⟨p1,q1⊲cut⟩+⟨q2,q2⊲cut⟩', but the second cut should be '⟨p2,q2⊲cut⟩'. The same typo appears in the description of the rule in the text.
  2. [Figure 4 and Remark 24] The caption of Figure 4 first states that p1, p2, q1, q2 are fresh positions and then explains that q1 and q2 may be elements of a or b and that p1 and p2 may be elements of q1,...,qn. This is confusing: the 'fresh' naming and the reuse of the same letters for existing positions should be reconciled.
  3. [Proposition 30] Items (2) and (3) of Proposition 30 use the notation 'S c− →·→∗ S′' and 'S→∗· c− →S′' without recalling that '·' denotes relation composition in this paper. Since these commutation statements are used pervasively, a parenthetical reminder at the first use would improve readability.
  4. [Theorem 77] The proof of Theorem 77 invokes the 'counter-proof criterion' of [4] without a proof or a precise statement in the present paper. Since the framework here extends the setting with non-homogeneous cut elimination, a more self-contained treatment of this external criterion would strengthen the paper.

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity: the completeness result is an engineered bootstrap that bottoms out in the external Danos-Regnier and Curien criteria, not in the paper's own conclusions; self-citations are positional only.

full rationale

I found no circular step; the derivation chain is acyclic (as the paper's Figure 14 also claims). The completeness direction (Theorem 85) proceeds in three proved stages, none of which assumes its conclusion. First, Section 6 chooses the daimon basis 1 (maps each atom to {✠1}⊥⊥) and proves, not stipulates, that realisers in that basis are syntactically testable: Lemma 186/Theorem 187/Prop. 83 are shown by induction using the internal decomposition Proposition 176. Second, Proposition 82 shows that for an approximable basis, testable realisers are provable, via Remark 81, Theorem 77 and Theorem 76; the proof is not definitional because membership in the interpretation ⟦Γ⟧B is fixed by biorthogonal closure, and the splitting of that closure is exactly what is established rather than assumed. Third, the load-bearing identification of testability with provability is Theorem 76, a proved reformulation of the external Danos-Regnier criterion (Theorem 40, cited to [4],[5]), and Theorem 77, which imports the external counter-proof criterion of Curien [4] (Theorem 168; the adaptation constraints are acknowledged in Remark 169). These anchors are independent, non-self-cited mathematical facts, and neither is stated in terms of the paper's types or its conclusions. Theorem 77's proof uses only the (⇒) direction of Theorem 76, which bottoms out in Theorem 40, so there is no cycle. Self-citations [15]–[20] are positional only (introduction and a footnote), never load-bearing. Two caveats are weighed but do not change the score. (1) Proposition 188 (Appendix G.6), load-bearing for the tensor case of Theorem 88, is an internal proof gap, not a circularity: its base case ('Since furthermore ⋂_B ⟦X⟧_B is empty it follows that ⟦X⟧_B‖⟦Y⟧_B is also empty thus the proposition hold') is incoherent, and the decisive polarisation step is dismissed with 'one can easily check'; Theorem 88 must therefore be regarded as conditional on a completed proof. (2) Proposition 182 explicitly omits a proof ('We will not give the detail here because this implication is not used in this work') and is non-load-bearing. Neither caveat involves a fitted parameter, a self-citation chain, or a definition that entails the result, so the honest circularity finding is low.

Assumptions & free parameters 0 free parameters · 2 assumptions · 0 invented entities

The central claim rests on the newly defined cut elimination and on two external correctness criteria. No free parameters are fitted; no new entities are postulated. The main unproved inputs are the Danos-Regnier criterion and Curien's counter-proof criterion, both cited from the literature.

assumptions (2)
  • domain assumption Danos-Regnier criterion (Theorem 40): cut-free MLL* nets are proof nets iff every switching is acyclic and connected.
    Imported from [4],[5]; used in Proposition 75 and Theorem 76 to connect orthogonality with tests to proof-net correctness.
  • domain assumption Curien's counter-proof criterion (Theorem 168 from [4]): an atomically testable cut-free net orthogonal to every proof of A⊥ is a proof of A.
    Used in proof of Theorem 77 to show tests are proofs of A⊥; this is an external completeness-type result from the Ludics literature.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Linear Realisability over nets: multiplicatives (long version)." pith.science (2026). https://pith.science/paper/NM5ETVLZ

@misc{pith2026241117486,
  author       = {Pith},
  title        = {Pith review of: Linear Realisability over nets: multiplicatives (long version)},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/NM5ETVLZ}},
  note         = {Machine review of arXiv:2411.17486}
}
read the original abstract

We provide a new realisability model based on orthogonality for the multiplicative fragment of linear logic, both in presence of generalised axioms (MLL*) and in the standard case (MLL). The novelty is the definition of cut elimination for generalised axioms. We prove that our model is adequate and complete both for MLL* and MLL.

Figures

Figures reproduced from arXiv: 2411.17486 by the authors.

Figure 1
Figure 1. Hypergraphs can naturally be represented in a grap [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Properties of hypergraphs: source–disjoint, tar [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. Rewriting defining the homogeneous cut eliminatio [PITH_FULL_IMAGE:figures/full_fig_p006_3.png] view at source ↗
Figures from the paper (11 more)
Figure 4
Figure 4. Figure 4: Rules defining the non–homogeneous cut eliminatio [PITH_FULL_IMAGE:figures/full_fig_p006_4.png]
Figure 5
Figure 5. Figure 5: Non homogeneous cut eliminations contains two sou [PITH_FULL_IMAGE:figures/full_fig_p007_5.png]
Figure 6
Figure 6. Figure 6: Grammar of formulas and (hyper)sequent, de Morgan [PITH_FULL_IMAGE:figures/full_fig_p008_6.png]
Figure 8
Figure 8. Figure 8: Induction defining the relation ≡R. The proof in the first row is represented by a net below it in the second row. The position p is always supposed fresh. In each case and for each 0 ≤ i ≤ 2, Si is a net which represent πi i.e. Si ≡R πi . In the case of the exchange r…
Figure 9
Figure 9. Figure 9: The interaction of two nets (Definition 41) and two orthogonal nets (Definition 42). Definition 41. Let S = (|S|,a(S)) and T = (|T|,a(T)) be two nets and k = min(#S,#T), we define their interaction S :: T = (|S :: T|,a(S :: T)) as: |S :: T| , |S|+|T|+∑1≤i≤min(#S,#T) hS…
Figure 10
Figure 10. Figure 10: The evolution of (switching) cycles and (switchi [PITH_FULL_IMAGE:figures/full_fig_p011_10.png]
Figure 11
Figure 11. Figure 11: The daimon link z2 is not orthogonal to z` k z`: a disconnected net never reduces to a connected one (and z0 is connected). Remark 81. Consider an approximable basis B and a sequent Γ = A1,...,An we have JΓKB = (JA1K ⊥ B k ··· k JAnK ⊥ B) ⊥. By Theorem 64, for any A ⊥…
Figure 12
Figure 12. Figure 12: The interaction of two orthogonal nets S and S with a daimon reduces to a daimon (with two less outputs). Remark 90. The completeness result for MLL (Theorem 88) only identifies cut–free and atomic proofs (i.e. where axioms introduce sequents of the form X,X ⊥). This …
Figure 13
Figure 13. Figure 13: Complements to [PITH_FULL_IMAGE:figures/full_fig_p020_13.png]
Figure 14
Figure 14. Figure 14: Relation of “dependency” between propositions i [PITH_FULL_IMAGE:figures/full_fig_p021_14.png]
Figure 15
Figure 15. Figure 15: The interaction of z2 with the net z` k z`, this cannot reduce to z0 since disconnection of the net is preserved by cut–elimination and z0 is connected. G.5 Proof of Theorem 85 Theorem 85 (MLLz completeness). Given a cut–free net S and a sequent Γ; • If for all basis …

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

58 extracted references · 54 canonical work pages

  1. [1]

    Minimality of the correctness criterion f or multiplicative proof nets

    Denis Bechet. Minimality of the correctness criterion f or multiplicative proof nets. Mathematical Structures in Computer Science , 8(6):543–558, 1998. doi:10.1017/S096012959800262X

    work page doi:10.1017/s096012959800262x 1998

  2. [2]

    A concurrent model for linear logic

    Emmanuel Beffara. A concurrent model for linear logic. Electronic Notes in Theo- retical Computer Science , 155:147–168, 2006. Proceedings of the 21st Annual Con- ference on Mathematical Foundations of Programming Semant ics (MFPS XXI). URL: https://www.sciencedirect.com/science/article/pii/S1571066106001927, doi:10.1016/j.entcs.2005.11.055

    work page doi:10.1016/j.entcs.2005.11.055 2006

  3. [3]

    Concurrent realizabil- ity on conjunctive structures

    Emmanuel Beffara, F´ elix Castro, Mauricio Guillermo, a nd ´Etienne Miquey. Concurrent realizabil- ity on conjunctive structures. In Marco Gaboardi and Femke v an Raamsdonk, editors, 8th In- ternational Conference on F ormal Structures for Computati on and Deduction, FSCD 2023, July 3-6, 2023, Rome, Italy , volume 260 of LIPIcs, pages 28:1–28:21. Schloss ...

    work page doi:10.4230/lipics.fscd.2023.28 2023

  4. [4]

    Introduction to linear logic and l udics, part II

    Pierre-Louis Curien. Introduction to linear logic and l udics, part II. CoRR, abs/cs/0501039, 2005. URL: http://arxiv.org/abs/cs/0501039, arXiv:cs/0501039

    arXiv 2005

  5. [5]

    The structure of mult iplicatives

    Vincent Danos and Laurent Regnier. The structure of mult iplicatives. Archive for Mathematical Logic , 28(3):181–203, 10 1989. doi:10.1007/BF01622878

    doi:10.1007/bf01622878 1989

  6. [6]

    V aleria C. V . de Paiva. A dialectica-like model of linear logic. In David H. Pitt, David E. Rydeheard, Peter Dybjer, Andrew M. Pitts, and Axel Poign´ e, editors,Category Theory and Computer Science, pages 341–356, Berlin, Heidelberg, 1989. Springer Berlin Heidelberg

    work page 1989

  7. [7]

    Linear logic

    Jean-Yves Girard. Linear logic. Theoretical Computer Science , 50(1):1 – 101, 1987. URL: http://www.sciencedirect.com/science/article/pii/0304397587900454, doi:10.1016/0304-3975(87)90045-4

    arXiv 1987

  8. [8]

    Multiplicatives

    Jean-Yves Girard. Multiplicatives. In G. Lolli, editor , Logic and Computer Science: New Trends and Applications, pages 11–34. Rosenberg & Sellier, 1987

    work page 1987

Show all 58 references
  1. [9]

    Proof-nets: The parallel syntax for p roof-theory

    Jean-Yves Girard. Proof-nets: The parallel syntax for p roof-theory. In Logic and Algebra , pages 97–124. Marcel Dekker, 1996

    1996

  2. [10]

    Locus solum: From the rules of logic t o the logic of rules

    Jean-Yves Girard. Locus solum: From the rules of logic t o the logic of rules. In Laurent Fribourg, editor, Computer Science Logic, pages 38–38, Berlin, Heidelberg, 2001. Springer Berlin He idelberg

    2001

  3. [11]

    From abstrac tion and indiscernibility to classification and types: revisiting hermann weyl’s theory of ideal elements

    Jean-Baptiste Joinet and Thomas Seiller. From abstrac tion and indiscernibility to classification and types: revisiting hermann weyl’s theory of ideal elements. Kagaku tetsugaku , 53(2):65–93, 2021. doi:10.4216/jpssj.53.2_65

    2021 doi

  4. [12]

    Realizability in classical logic

    Jean-Louis Krivine. Realizability in classical logic . Panoramas et synth `eses, 27:197–229, 2005. URL: https://hal.science/hal-00154500

    2005

  5. [13]

    Handbook of Linear Logic

    International Research Network (IRN) Linear Logic. Handbook of Linear Logic. International Research Network (IRN) Linear Logic, 2023. URL: https://ll-handbook.frama.io/ll-handbook/ll-handboo k-public.pdf

    2023

  6. [14]

    Modified realizability interpretation of classical linear logic

    Paulo Oliva. Modified realizability interpretation of classical linear logic. In 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007) , pages 431–442, 2007. doi:10.1109/LICS.2007.32

    2007 doi

  7. [15]

    Interaction graphs: Multiplicatives

    Thomas Seiller. Interaction graphs: Multiplicatives . Annals of Pure and Applied Logic , 163(12):1808–1837,

  8. [16]

    Interaction graphs: Exponentials

    Thomas Seiller. Interaction graphs: Exponentials. Log. Methods Comput. Sci. , 15, 2013

    2013

  9. [17]

    Interaction graphs: Full linear logic

    Thomas Seiller. Interaction graphs: Full linear logic . CoRR, abs/1504.04152, 2015. URL: http://arxiv.org/abs/1504.04152, arXiv:1504.04152

    2015 arXiv

  10. [18]

    Interaction graphs: Additives

    Thomas Seiller. Interaction graphs: Additives. Annals of Pure and Applied Logic , 167(2):95–154, 2016. doi:10.1016/j.apal.2015.10.001. 16

    2016 doi

  11. [19]

    Interaction graphs: Graphings

    Thomas Seiller. Interaction graphs: Graphings. Annals of Pure and Applied Logic , 168(2):278–320, 2017. doi:10.1016/j.apal.2016.10.007

    2017 doi

  12. [20]

    dependency

    Thomas Seiller. Mathematical informatics, 2024. Habi litation thesis. URL: https://theses.hal.science/tel-04616661. 17 Contents 1 Untyped nets 2 1.1 Directed hypergraphs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.2 Multiplicative nets...

    2024

  13. [22]

    S →∗ 1 S′→∗ 2 T , where→1 eliminates cut from C 1 or the cut it produces and →2 eliminates cuts from C 2 or the cut it produces. Proof. 1⇒ 2. If two cut c and d are unrelated: if c is not multiplicative, any cut created by the elimination of c will still be unrelated with d ( ...

  14. [23]

    Proposition 123

    We denote by S ⊲ ⊳(d,d′) S′ the net S0 + S′ 0 + (d ⊲ ⊳d′). Proposition 123. Given two nets S and S ′ respectively containing daimons d and d ′ so that S = S0 + d and S′ = S′ 0 + d′: S ⊲ ⊳(d,d′) S′ is equal to S ⊲ ⊳(d,d′) d′ + S′ 0. Proof. One merely needs to write the nets S ⊲...

  15. [24]

    T 1→∗ ✠ 0 and T2→∗ ✠ 0

  16. [25]

    S ⊲ ⊳d1,d′ 1 T1 ⊲ ⊳d2,d′ 2 T2 reduces to ✠ 0 Proof. 1⇒ 2. This is the easy implication. T2→∗ ✠ 0 thus by applying Proposition 127 S ⊲ ⊳d1,d′ 1 T1 ⊲ ⊳d2,d′ 2 T2 reduces to S ⊲ ⊳d1,d′ 1 T1 ⊲ ⊳d2, f (d′

  17. [26]

    We conclude since S→∗ ✠ 0 (Remark 131)

    ✠ 0 that is S ⊲ ⊳d1,d′ 1 T1 again applying Proposition 127 with T1→∗ ✠ 0 yields that S ⊲ ⊳d1,d′ 1 T1 reduces to S ⊲ ⊳d1 ✠ 0 that is S. We conclude since S→∗ ✠ 0 (Remark 131). 2⇒ 1. The other direction requires the use of Proposition 30 (item 2) and Proposition 30 (item 3). The...

  18. [27]

    Similarly because (S ⊲ ⊳d1,d′ 1 T1) ⊲ ⊳d2, f (d′

    T′ 2 Necessarily because c (and the cut it produces) is a cut that is not in T2 or any of its redexes, and because the cuts of T1 and T2 also are disjoint the reduction Equation 1 implies that T′ 2 must be cut–free and thus in particular a normal form of T2. Similarly because ...

  19. [28]

    T′ 2 reduces to S by→∗ 1 applying Proposition 127 one obtains that S1 = (S ⊲ ⊳d1,d′ 1 T1) ⊲ ⊳d2, f (d′

  20. [29]

    T′ 2 reduces to S in the following way: there is a reduction T1→ T′ 1 and S equals (S ⊲ ⊳d1,d′ 1 T′

  21. [30]

    From this argument one shows that S = (S ⊲ ⊳d1,d′ 1 T′

    Again because c (and the cut it produces) is a cut that is not in T1 or any of its redexes, 31 and because the cuts of T1 and T2 also are disjoint the reduction Equation 1 implies that T′ 1 must be cut–free and thus in particular a normal form of T1. From this argument one sho...

  22. [31]

    If T′ 1 (resp T′

    (2) Furthermore T′ 1 and T′ 2 are both cut–free and without conclusions they are therefor e sums of ✠ 0 links Remark 132. If T′ 1 (resp T′

  23. [32]

    ∑ 1≤i≤k ✠ 0) then S = (S ⊲ ⊳d1,d′ 1 ∑ 1≤i≤n ✠ 0) ⊲ ⊳d2, f (d′

    is ∑ 1≤i≤n ✠ 0 (resp. ∑ 1≤i≤k ✠ 0) then S = (S ⊲ ⊳d1,d′ 1 ∑ 1≤i≤n ✠ 0) ⊲ ⊳d2, f (d′

  24. [33]

    T′ 2 equals (S +∑ 1≤i≤n−1 ✠ 0) ⊲ ⊳d2, f (d′ 2) T′ 2 that will be (S + ∑ 1≤i≤n−1 ✠ 0) ⊲ ⊳d2, f (d′

  25. [34]

    From Equation 2 this means that necessarily n− 1 = 0 and k− 1 = 0 i.e

    ∑ 1≤i≤k ✠ 0 that is S + ∑ 1≤i≤n−1 ✠ 0 + ∑ 1≤i≤k−1 ✠ 0. From Equation 2 this means that necessarily n− 1 = 0 and k− 1 = 0 i.e. T′ 1 and T′ 2 equal ✠ 0. Therefore we conclude that T1→∗ ✠ 0 and T2→∗ ✠ 0 D.2.3 Proofs of section section 3 – Proposition 51 , Proposition 56 and Propo...

  26. [35]

    the density of the parallel composition ( Remark 50)

  27. [36]

    the head

    Proposition 48: more precisely, for any nets S1, S2, S3, S4 such that # S1≥ #S2 + #S3 + #S4, we have (S1 :: (S2‖ S3)) :: S4 = ((S1 :: S2) :: S3) :: S4 = (S1 :: S2) :: (S3‖ S4). By Proposition 51 it is enough to show that one of the two constructions is assoc iative. Let us do ...

  28. [37]

    A0 /YrightB0⊆ A /YrightB

  29. [38]

    We treat each point independently

    A0 ` B0⊆ A ` B Proof. We treat each point independently

  30. [39]

    Because we have the inclusion A0⊆ A and B0⊆ B it follow then that x = a0‖ b0 belongs to A‖− B and thus to A‖ B

    Consider x an element of A0‖− B0 then x is of the form a0‖ b0 with a0∈ A0 and b0∈ B0. Because we have the inclusion A0⊆ A and B0⊆ B it follow then that x = a0‖ b0 belongs to A‖− B and thus to A‖ B. As a consequence A0‖− B0⊆ A‖ B thus, because bi orthogonality preserves inclusi...

  31. [40]

    Using the previous demonstrated fact it follows that A⊥ 0‖ B⊥ 0 contains A⊥‖ B⊥

    If A0⊆ A and B0⊆ B we equivalently have the inclusions A⊥ 0 ⊇ A⊥ and B⊥ 0 ⊇ B⊥. Using the previous demonstrated fact it follows that A⊥ 0‖ B⊥ 0 contains A⊥‖ B⊥. Again using the fact that orthoganility invert inclusions we then derive that (A⊥ 0‖ B⊥ 0 )⊥ is included in (A⊥‖ B⊥)...

  32. [41]

    In the ⊗–case we reason similarly to the ‖ case

  33. [42]

    35 Proposition 136 (Remark 59)

    For the ` –case we can reason by duality using the ⊗–case. 35 Proposition 136 (Remark 59). Given a formula A and a basis B, we have /llbracketA⊥/rrbracketB⊆ /llbracketA/rrbracket⊥ B. Proof. By induction on the formula. If A = X is an atomic formula this is trivial. If A = B⊗ C...

  34. [44]

    S ✠ and T ✠ are orthogonal

  35. [45]

    Nat(P✠ (S)) and Nat(P✠ (T )) are orthogonal. Proof. Assume that S✠ :: T ✠ reduces to ✠ 0. In other words the following net reduces to ✠ 0: S✠ + T ✠ + ∑ 1≤i≤n ⟨S✠ (i), T ✠ (i) ⊲cut⟩. 41 Equivalently this means that S✠ :: T ✠ is an acyclic and connected graph. In particular if w...

  36. [46]

    The nets S and T are orthogonal

  37. [47]

    The nets S ✠ and T ✠ are orthogonal

  38. [48]

    The partition NatS(P✠ (S)) and NatT (P✠ (T )) are orthogonal. Proof. This follows from the two previous proposition, Proposition 159 and Proposition 158. 1⇔ 2. As for 1⇒ 2, we need to establish a property of the rewriting of nets: if N→mult N′ and N− →∗✠ 0 then N′− →∗✠ 0. As f...

  39. [49]

    S ⊥ S1‖···‖ Sn‖ T1‖···‖ Tk

  40. [50]

    ,pn ⊲` n p⟩⊥ S1 +··· + Sn +⟨S1(1)

    S +⟨p0, . . . ,pn ⊲` n p⟩⊥ S1 +··· + Sn +⟨S1(1) . . . ,Sn(1) ⊲⊗n q⟩‖ T1‖···‖ Tk Proof. By a simple induction of the size of the generalised ` connective. To derive the generalised theorem one must observe that the t ests of ` –formulas are tensors of the tests of the subformul...

  41. [51]

    Each test of A is the representation of a proof of A ⊥

  42. [52]

    soundness

    F or any cut–free net S |≃ at A if S is orthogonal to each (cut–free) T |≃ at A⊥ representing a proof of A ⊥ then S⊢✠ MLL A. Proof. The fact that 2⇒ 1 is the proof of Theorem 77 (it uses the counter proof criterion [ 4], Theorem 168). To show 1⇒ 2, consider a net S|≃ at A and ...

  43. [53]

    There exists an adequate basis

  44. [54]

    Any S ⊢MLL✠ A is orthogonal to any T ⊢MLL✠ A⊥. Proof. 1⇒ 2. Say B is an adequate basis then for any formula A we have ⦃A : MLL✠ ⦄⊆ /llbracketA/rrbracketB. Now since /llbracketA/rrbracketB equals /llbracketA ⊥⊥ /rrbracketB we derive /llbracketA/rrbracketB⊆ /llbracketA⊥/rrbracke...

  45. [55]

    S is orthogonal to each net T representing a proof of A ⊥

  46. [56]

    S ⊢MLL✠ A. Proof. 1⇒ 2. Assume that S|≃ at A0 with A0 such that there exists θ with θ A0 = A and that S is orthogonal to each proof nets T⊢MLL✠ A⊥. In particular any net T⊢MLL✠ A⊥ 0 with T|≃ at A⊥ 0 is such that T⊢MLL✠ A⊥ ( Proposition 33). As a consequence: S is orthogonal to...

  47. [57]

    S|≃ at ∆ for some sequent ∆ ≤ Γ

    S|≃Γ i.e. S|≃ at ∆ for some sequent ∆ ≤ Γ

  48. [58]

    adequate

    S ⊢MLL✠ Γ . Proof. Using remark 81 and the fact that the tests of a formula B in ∆ are proofs of B⊥ and by proposition 33 are proofs of A⊥. G Complements to section 6 G.1 Decomposition Proposition 176 (Decomposition). Let B be an interpretation basis, H be an hypersequent, A ,...

  49. [59]

    it follows that (S1 :: u)⊥(S2 :: v). Let us rewrite this net to conclude: S1 :: u :: S2 :: v = S1 :: u +⟨(S1 :: u)(1), (S2 :: v)(1) ⊲cut⟩+ S2 :: v (Definition 41 ) = S1 :: u +⟨S1(#S1), S2(#S2) ⊲cut⟩+ S2 :: v (Identity) = ( S1 +⟨S1(#S1), S2(#S2) ⊲cut⟩) :: u + S2 :: v (Propositio...

  50. [2012]

    doi:10.1016/j.apal.2012.04.005

    2012 doi

Pith tools

Reviewed August 12, 2026 · model on record in the stance chip above.