A Taste of Quantitative Logic

Abstract

Quantitative logic, after Lawvere, is one whose judgments are valued in real numbers, rather than merely being a logic about real numbers. By doing this we can guarantee good structural properties of the logic, such as being able to treat addition as an additive connective in the sense of Girard. Moreover, by employing the full spectrum of sums multiplication distributes over, we are able to approximate ‘hard’ connectives with ‘soft’ ones, with application in machine learning. In the talk I will showcase these features by describing a sequent calculus for a quantitative version of linear logic. This is work in progress with Atkey, Grellois, and Komendantskaya.