Lawvere showed that generalised metric spaces are categories enriched over $[0, \infty]$, the quantale of the positive extended reals. The statement of enrichment is a quantitative analogue of being a preorder. Towards seeking a logic for quantitative metric reasoning, we investigate three $[0,\infty]$-valued propositional logics over the Lawvere quantale. The basic logical connectives shared by all three logics are those that can be interpreted in any quantale, viz finite conjunctions and disjunctions, tensor (addition for the Lawvere quantale) and linear implication (here a truncated subtraction); to these we add, in turn, the constant $1$ to express integer values, and scalar multiplication by a non-negative real to express general affine combinations. Quantitative equational logic can be interpreted in the third logic if we allow inference systems instead of axiomatic systems. For each of these logics we develop a natural deduction system which we prove to be decidably complete w.r.t. the quantale-valued semantics. The heart of the completeness proof makes use of the Motzkin transposition theorem. Consistency is also decidable; the proof makes use of Fourier-Motzkin elimination of linear inequalities. Strong completeness does not hold in general, even (as is known) for theories over finitely-many propositional variables; indeed even an approximate form of strong completeness in the sense of Pavelka or Ben Yaacov -- provability up to arbitrary precision -- does not hold. However, we can show it for theories axiomatized by a (not necessarily finite) set of judgements in normal form over a finite set of propositional variables when we restrict to models that do not map variables to $\infty$; the proof uses Hurwicz's general form of the Farkas' Lemma.

翻译：Lawvere 证明了广义度量空间是 $[0, \infty]$（正扩展实数的量化格）上的丰富范畴。该丰富性陈述是预序关系的一种定量类比。为寻求定量度量推理的逻辑，我们研究了基于 Lawvere 量化格的三种 $[0,\infty]$ 值命题逻辑。这三种逻辑共有的基本逻辑连接词是可被任意量化格解释的，即有限合取与析取、张量积（对 Lawvere 量化格为加法）以及线性蕴涵（此处为截断减法）；在此基础上，我们依次添加常数 $1$ 以表达整数值，以及非负实数的标量乘法以表达一般仿射组合。若允许使用推理系统而非公理系统，定量等式逻辑可在第三种逻辑中解释。针对每种逻辑，我们发展了一个自然演绎系统，并证明其相对于量化格值语义是可判定完备的。完备性证明的核心利用了莫茨金转置定理。一致性同样是可判定的，其证明利用了傅里叶-莫茨金线性不等式消去法。强完备性一般不成立，即使（如所周知）对于有限多个命题变元上的理论也是如此；实际上，巴维尔卡或本·雅科夫意义上的近似强完备性（即任意精度的可证性）也不成立。然而，对于由有限命题变元集上的范式判定集（不必有限）公理化的理论，在限制模型不将变元映射到 $\infty$ 的情况下，我们可证明其成立；该证明使用了法卡斯引理的赫维奇一般形式。