On Quantifiers for Quantitative Reasoning

TL;DR

This paper develops a first-order predicate logic over the reals with novel bounded quantifiers based on means, exploring their semantics and applications in quantitative reasoning.

Contribution

It introduces a new quantitative predicate logic using multiplicative reals and means as quantifiers, with semantics and categorical approaches, advancing formal reasoning with quantities.

Findings

Means and harmonic means serve as natural bounded quantifiers.

Softmax functions as semantics of argmax in this logic.

Rényi entropy and Hill numbers are modeled as additive/multiplicative semantics.

Abstract

We explore a kind of first-order predicate logic with intended semantics in the reals. Compared to other approaches in the literature, we work predominantly in the multiplicative reals $[0,\infty]$, showing they support three generations of connectives, that we call non-linear, linear additive, and linear multiplicative. Means and harmonic means emerge as natural candidates for bounded existential and universal quantifiers, and in fact we see they behave as expected in relation to the other logical connectives. We explain this fact through the well-known fact that min/max and arithmetic mean/harmonic mean sit at opposite ends of a spectrum, that of p-means. We give syntax and semantics for this quantitative predicate logic, and as example applications, we show how softmax is the quantitative semantics of argmax, and R\'enyi entropy/Hill numbers are additive/multiplicative semantics of the same formula. Indeed, the additive reals also fit into the story by exploiting the Napierian duality $-\log \dashv 1/\exp$, which highlights a formal distinction between 'additive' and 'multiplicative' quantities. Finally, we describe two attempts at a categorical semantics via enriched hyperdoctrines. We discuss why hyperdoctrines are in fact probably inadequate for this kind of logic.