Pith Number

pith:2VN6YPPC

pith:2026:2VN6YPPCXFPLRPOGWJMWUDTUAM

not attested not anchored not stored refs resolved

Quantitative Linear Logic

Charles Grellois, Ekaterina Komendantskaya, Matteo Capucci, Robert Atkey

A family of quantitative sequent calculi pQLL assigns real values to proofs and sequents, proving cut-elimination and completeness for soft lattices while converging to MALL as hardness p increases.

arxiv:2605.13348 v2 · 2026-05-13 · cs.LO · math.LO

Open paper page JSON Open Graph Bundle Merged state Verified badge What is a Pith Number?

Add to your LaTeX paper

\usepackage{pith}
\pithnumber{2VN6YPPCXFPLRPOGWJMWUDTUAM}

Prints a linked badge after your title and injects PDF metadata. Compiles on arXiv. Learn more · Embed verified badge

Record completeness

1 Bitcoin timestamp

2 Internet Archive

3 Author claim open · sign in to claim

4 Citations open

5 Replications open

✓ Portable graph bundle live · download bundle · merged state

The bundle contains the canonical record plus signed events. A mirror can host it anywhere and recompute the same current state with the deterministic merge algorithm.

Claims

C1strongest claim

We present a family of calculi, pQLL, indexed by a hardness degree p, prove cut-elimination theorem for them, and show completeness for enriched residuated 'soft' lattices. For p = ∞, pQLL reduces to MALL, with provability in pQLL converging to provability in MALL when p → ∞.

C2weakest assumption

The assumption that real-valued sum and product can be lifted to a residuated lattice structure while preserving the logical properties needed for cut elimination and completeness, without introducing inconsistencies when the hardness parameter p varies.

C3one line summary

pQLL calculi assign real-valued strength to proofs, generalize hypersequent and deep inference systems, prove cut elimination, and achieve completeness for soft residuated lattices, recovering MALL as p goes to infinity.

References

61 extracted · 61 resolved · 3 Pith anchors

[1] Reynald Affeldt, Alessandro Bruni, Ekaterina Komendantskaya, Natalia Slusarz, and Kathrin Stark. 2024. Taming Differentiable Logics with Coq Formalisation. In 15th International Conference on Interact 2024 · doi:10.4230/lipics.itp.2024.4

[2] Paolo Aglianò. 2025. An algebraic investigation of linear logic. Archive for Mathematical Logic (2025), 1–23 2025

[3] Arnon Avron. 1987. A Constructive Analysis of RM. The Journal of symbolic logic 52, 4 (1987), 939– 1987

[4] https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/constructive-analysis-of-rm/ 342F0DE51D0878BEC48C03E65FBA03BC

[5] Matthias Baaz, Agata Ciabattoni, and Christian G. Fermüller. 2003. Hypersequent Calculi for Gödel Logics - a Survey. J. Log. Comput. 13, 6 (2003), 835–861. https://doi.org/10.1093/LOGCOM/13.6.835 2003 · doi:10.1093/logcom/13.6.835

Formal links

3 machine-checked theorem links

Cited by

1 paper in Pith

Quantitative Linear Logic for Neuro-Symbolic Learning and Verification

Receipt and verification

First computed	2026-05-18T02:44:48.317756Z
Builder	pith-number-builder-2026-05-17-v1
Signature	Pith Ed25519 (`pith-v1-2026-05`) · public key
Schema	pith-number/v1.0

Canonical hash

d55bec3de2b95eb8bdc6b2596a0e740315c41c4c76f4d990b8f9a1a4a590db24

Aliases

arxiv: 2605.13348 · arxiv_version: 2605.13348v2 · doi: 10.48550/arxiv.2605.13348 · pith_short_12: 2VN6YPPCXFPL · pith_short_16: 2VN6YPPCXFPLRPOG · pith_short_8: 2VN6YPPC

Agent API

Resolver JSON Graph JSON Events JSON Schema Signing key

Verify this Pith Number yourself

curl -sH 'Accept: application/ld+json' https://pith.science/pith/2VN6YPPCXFPLRPOGWJMWUDTUAM \
  | jq -c '.canonical_record' \
  | python3 -c "import sys,json,hashlib; b=json.dumps(json.loads(sys.stdin.read()), sort_keys=True, separators=(',',':'), ensure_ascii=False).encode(); print(hashlib.sha256(b).hexdigest())"
# expect: d55bec3de2b95eb8bdc6b2596a0e740315c41c4c76f4d990b8f9a1a4a590db24

Canonical record JSON

{
  "metadata": {
    "abstract_canon_sha256": "616c9003bfff668b59d147136b83496c11d676f9ca305365b1137a024b91b2ba",
    "cross_cats_sorted": [
      "math.LO"
    ],
    "license": "http://creativecommons.org/licenses/by/4.0/",
    "primary_cat": "cs.LO",
    "submitted_at": "2026-05-13T11:05:08Z",
    "title_canon_sha256": "39a33d9475a347461adb210135d7d2ec0ad386423024aa6d59b75af923bcebd6"
  },
  "schema_version": "1.0",
  "source": {
    "id": "2605.13348",
    "kind": "arxiv",
    "version": 2
  }
}