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.
翻译:本文探讨一种以一阶谓词逻辑为基础、以实数集为预期语义的定量推理框架。相较于文献中的其他方法,我们主要在乘法实数域 $[0,\infty]$ 中展开研究,证明该数域支持三类连接词,分别称为非线性、线性加法与线性乘法连接词。均值与调和均值自然地成为有界存在量词与全称量词的候选算子,并且我们观察到它们与其他逻辑连接词之间的交互行为符合预期。我们通过一个众所周知的事实解释这一现象:极小/极大值与算术平均/调和平均值分别位于 p-均值谱系的两端。我们为此定量谓词逻辑提供了语法与语义定义,并通过示例应用展示了 softmax 如何作为 argmax 的定量语义,以及 Rényi 熵/Hill 数如何作为同一公式的加法/乘法语义。事实上,通过利用 Napier 对偶关系 $-\log \dashv 1/\exp$,加法实数域亦可融入该理论框架,这凸显了“加法性”与“乘法性”量之间的形式区别。最后,我们尝试通过富超范畴理论构建两种范畴语义,并讨论了为何超范畴结构可能并不适用于此类逻辑。