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 (closely related) many-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. Propositional Boolean logic can already be interpreted in the first of these logics; {\L}ukasiewicz logic can be interpreted in the second; Ben Yaacov's continuous propositional logic can be interpreted in the third; and quantitative equational logic can be interpreted in the third 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 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 for theories over finitely-many propositional variables; indeed even an approximate form of strong completeness in the sense of Ben Yaacov -- provability up to arbitrary precision -- does not hold. However, we can show it for such theories having only models never mapping variables to $\infty$; the proof uses Hurwicz's general form of the Farkas lemma.

翻译：Lawvere指出，广义度量空间是在$[0, \infty]$（正扩展实数构成的quantale）上富集（enriched）的范畴。这种富集性陈述是预序关系的定量类比。为探索定量度量的逻辑，我们研究了Lawvere quantale上的三种（密切相关的）多值命题逻辑。这三种逻辑共享的基本逻辑连接词是可在任意quantale中解释的那些，即有限合取与析取、张量（在Lawvere quantale中为加法）及线性蕴涵（此处为截断减法）；在此基础上，我们依次添加常数1以表达整数值，以及与非负实数作标量乘法以表达一般仿射组合。命题布尔逻辑已可在第一种逻辑中解释；Łukasiewicz逻辑可在第二种逻辑中解释；Ben Yaacov的连续命题逻辑可在第三种逻辑中解释；若允许使用推理系统而非公理系统，则定量等式逻辑可在第三种逻辑中解释。针对每种逻辑，我们发展了自然演绎系统，并证明其在quantale值语义下具有可判定的完备性。完备性证明的核心利用了Motzkin转置定理。一致性也具有可判定性；其证明利用了线性不等式的Fourier-Motzkin消去法。强完备性一般不成立，即便对于具有有限多个命题变元的理论也是如此；实际上，Ben Yaacov意义上的近似强完备性形式（即任意精度的可证性）也不成立。然而，对于仅将变元映射至非$\infty$值的模型的理论，我们可以证明强完备性；其证明使用了Farkas引理的Hurwicz一般形式。