Quantitative Linear Logic

TL;DR

This paper introduces quantitative sequent calculi for real-valued logics, enabling differentiable semantics for additive connectives, with applications to probabilistic and machine learning systems.

Contribution

It develops a family of calculi, pQLL, that generalize fuzzy and linear logics with real-valued proof measures, including a cut-elimination theorem and completeness results.

Findings

Proves cut-elimination for pQLL calculi.

Shows pQLL reduces to MALL as p approaches infinity.

Establishes completeness for enriched residuated soft lattices.

Abstract

Real-valued logics have seen a renewed interest in verification for probabilistic and quantitative systems, in particular machine learning models, where they can be used to directly integrate specifications in the training objective. To do so effectively one has to strike a balance between the logical properties of the connectives and their semantics. A major hurdle in this sense is to give ``soft'' (i.e. differentiable) semantics to additive connectives -- in linear and fuzzy logics, additives are necessarily ``hard'' lattice operations. In this paper, we solve this problem by combining an accurate analysis of the properties of sum and product on the reals with a significant revision of sequent calculus. We introduce `quantitative sequent calculi', which simultaneously generalize hypersequent calculi of fuzzy logics and deep inference, and in which validity of a proof and provability of a sequent are real-valued quantities. 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 = \infty$, pQLL reduces to MALL, with provability in pQLL converging to provability in MALL when $p \to \infty$.