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, \(p\)QLL, indexed by a hardness degree \(p\), prove cut-elimination theorem for them, and show completeness for enriched residuated
'soft' lattices.
For \(p = \infty \), \(p\)QLL reduces to MALL, with provability in \(p\)QLL converging to provability in MALL when \(p \to \infty \).