Rational Lawvere Logic

Connections between arithmetic and logical reasoning are well known. A completeness interpretation of Farkas’ Lemma appears already in the literature (e.g., in [46]). In algebraic complexity there is the Nullstellensatz proof system which uses a simple reduction of propositional satisfaction to polynomial equation solvability (e.g., [11, 52]) and the Positivstellensatz calculus [29] which considers polynomial inequalities.

Parallel to Lawvere’s real-valued approach we must mention the vast development of fuzzy logic, for example [51, 12, 31]. Fuzzy logic generally employs (if not explicitly) quantales on the real interval $[0,1]$. The most relevant for us is product logic [32, 30, 56, 22], defined over the multiplicative quantale on $[0,1]$. Through the quantale isomorphism $e^{-x}$, $𝔸𝕃$ corresponds to product logic extended with constants in $[0,1]$, and $ℝ𝕃$ corresponds to a further extension with an operation $e^{-\ln x\ln y}$. Neither of these extensions seems to be in the literature. Moreover, this interpretation of the logical connectives seems unnatural for quantitative reasoning over $[0,\mathrm{\infty }]$, and impedes direct access to results we use, e.g., in linear algebra (such as Khachiyan’s ellipsoid method, used for complexity), and in real algebraic geometry (such as the Krivine-Stengle Positivstellensatz, used for completeness).

We must also mention the extensive works on graded (or weighted) structures, such as linear logic’s exponentials, comonads, types, or categories (e.g., [33, 28, 4, 17, 18, 42]). The gradings usually employ general semirings of some kind. However $[0,\mathrm{\infty }]$ in particular is also discussed, for example in [28, 4, 33, 18]. Various possibilities for multiplication are considered: two commutative ones (ours is one) and a non-commutative one. In Section 2, we discuss all the possible monotonic, commutative, and associative addition and multiplication operations on $[0,\mathrm{\infty }]$ that extend the usual ones on $(0,\mathrm{\infty })$. They are all definable in our logic (as are the non-commutative ones, as a straightforward extension of our discussion shows).

Section 2 gives preliminary definitions and notation. Section 3 gives the syntax and semantics of $ℝ𝕃$, and Section 4 presents a deduction system for it. Section 5 presents some nontrivial applications. Section 6 develops the completeness result. Section 7 gives the complexity results for $ℝ𝕃$ and its affine fragment $𝔸𝕃$. Section 8 gives concluding remarks and discusses future work.

We would like to extend sum from the positive reals $(0,\mathrm{\infty })$ to $[0,\mathrm{\infty }]$ so that we still get a sum that is associative, commutative, and monotonic w.r.t $\le$ (equivalently w.r.t. ${\le }^{op}$). One can show there are three choices for defining such a sum, as given in Table 1, with ${+}_1$ being the addition of the Lawvere quantale.

Thus, for an additive quantale on $[0,\mathrm{\infty }]$, if we use the natural order $\le$, the correct choice for sum is ${+}_2$; if we use the reverse order ${\le }^{op}$, the correct choice is ${+}_1$. The first is not unital, since $0{+}_2\mathrm{\infty }=0$; the Lawvere quantale, is both unital and integral. We chose ${+}_1$, as this enables us to directly encode examples from quantitative equational logic (Section 5). The right adjoint to $-{+}_{1}a$, can be explicitly formulated in terms of truncated substruction $\text{<object type="image/svg+xml" data="dagpub-standalone-manual-2026-03-04-17-42-50-page-1.pdf2svg.svg" id="S2.SS0.SSS0.P0.SPx1.p2.m9.g1nest" class="ltx\_graphics ltx\_img\_square" width="6" height="5" style="width: 12px; height: unset; max-width: 100\%"></object>}$, appropriately extended to $[0,\mathrm{\infty }]$ as shown in Table 1. Indeed, it holds that $b\text{<object type="image/svg+xml" data="dagpub-standalone-manual-2026-03-04-17-42-50-page-1.pdf2svg.svg" id="S2.SS0.SSS0.P0.SPx1.p2.m11.g1nest" class="ltx\_graphics ltx\_img\_square" width="6" height="5" style="width: 12px; height: unset; max-width: 100\%"></object>}a=inf\{c\mid c{+}_{1}a\ge b\}$.

One can show there are two associative, commutative, and monotonic extensions of multiplication from $[0,\mathrm{\infty })$ to $[0,\mathrm{\infty }]$: ${\times }_1$ and ${\times }_2$, as given in Table 1.

Thus, for a multiplicative quantale on $[0,\mathrm{\infty }]$, if we use the natural order $\le$, it is ${\times }_1$; if we use the reverse order ${\le }^{op}$, it is ${\times }_2$. We discuss our choice of multiplication in relation to the Lawvere quantale. On the one hand, if the choice were dictated by the quantale order, ${\times }_2$ would seem the natural candidate. On the other hand, unlike ${\times }_2$, choosing ${\times }_1$ yields a semiring (both multiplications distribute over $+$, but the unit of ${+}_1$ is not the null element for ${\times }_2$, as $\mathrm{\infty }{\times }_{2}0=\mathrm{\infty }$). Ultimately, we choose ${\times }_1$. While no choice is perfect, having a semiring enables us to directly encode examples from measure theory (Section 5) and to obtain a deduction theorem (Theorem 8).

Although the logic will use the order of the Lawvere quantale, we will still exploit the quantalic structure associated with ${\times }_1$ by adding as a logical connective the right adjoint to $-{\times }_{1}a$, which can be explicitly formulated in terms of division $÷$, appropriately extended to $[0,\mathrm{\infty }]$ as given in Table 1. Indeed, it holds that $b÷a=sup\{c\mid c{\times }_{1}a\le b\}$.

We conclude by showing that the other operations, namely ${+}_2$, ${+}_3$, and ${\times }_2$, can be expressed in terms of ${+}_1$, ${\times }_1$, $\text{<object type="image/svg+xml" data="dagpub-standalone-manual-2026-03-04-17-42-50-page-1.pdf2svg.svg" id="S2.SS0.SSS0.P0.SPx2.p4.m6.g1nest" class="ltx\_graphics ltx\_img\_square" width="6" height="5" style="width: 12px; height: unset; max-width: 100\%"></object>}$, and $\mathrm{\infty }$ (and so, eventually, in $ℝ𝕃$). First, binary sups and infs can be:

Next, we define functions $N,Z:[0,\mathrm{\infty }]\to [0,\mathrm{\infty }]$ by $N(a)=\mathrm{\infty }\text{<object type="image/svg+xml" data="dagpub-standalone-manual-2026-03-04-17-42-50-page-1.pdf2svg.svg" id="S2.SS0.SSS0.P0.SPx2.p5.m2.g1nest" class="ltx\_graphics ltx\_img\_square" width="6" height="5" style="width: 12px; height: unset; max-width: 100\%"></object>}a$ and $Z(a)=a{\times }_1\mathrm{\infty }$. These are “boolean functions” returning either $0$ or $\mathrm{\infty }$ (i.e., $\top$ and $\perp$ in the Lawvere quantale), as:

Hence, $N$ is a test for $\mathrm{\infty }$, while $Z$ is a test for $0$. We can next define a conditional using $\vee$ and $\wedge$:

and finally obtain:

Hereafter, when working on $[0,\mathrm{\infty }]$, we simply write $+$ for the sum instead of ${+}_1$ and $\times$ for the multiplication instead of ${\times }_1$. The other operations, namely $\text{<object type="image/svg+xml" data="dagpub-standalone-manual-2026-03-04-17-42-50-page-1.pdf2svg.svg" id="S2.SS0.SSS0.P0.SPx2.p6.m6.g1nest" class="ltx\_graphics ltx\_img\_square" width="6" height="5" style="width: 12px; height: unset; max-width: 100\%"></object>}$ and $÷$ (written as a fraction), are those from Table 1. We continue writing $\le$ for the natural order on $[0,\mathrm{\infty }]$ and ${\le }^{op}$ for Lawvere’s order.

Let $\mathbb{P}$ be a set of propositional letters, ranged over by $P,Q,R,\mathrm{\dots }$. The formulas of $ℝ𝕃$ are freely generated by the following grammar, for arbitrary $P\in \mathbb{P}$ and $r\in [0,\mathrm{\infty })$.

We define expected logical connectives as derived operators:

We assume the following precedence rule: multiplication and division have highest precedence, followed by $\neg$, then $\oplus$, next $\wedge$ and $\vee$, and finally $⊸$ and $⧟$ have lowest precedence. Thus, $\theta \varphi \oplus \psi \wedge \neg \theta \psi ⊸\theta$ is interpreted as the formula $(((\theta \varphi )\oplus \psi )\wedge (\neg (\theta \psi )))⊸\theta$.

Interpretations are maps $ℐ:\mathbb{P}\to [0,\mathrm{\infty }]$, extended to all formulas as follows:

Consequently, the derived connectives are interpreted as follows (recall Lemma 3):

Affine Lawvere Logic ($𝔸𝕃$), introduced in [9], is the sublogic of $ℝ𝕃$ defined for $P\in \mathbb{P}$ and $r\in [0,\mathrm{\infty })$, by the following grammar:²²2In [9] $\wedge$ and $\vee$ belong to the syntax, but they can be obtained as derived operators, as in $ℝ𝕃$.

While, in $ℝ𝕃$, an interpretation evaluates a formula to a value in $[0,\mathrm{\infty }]$, formulas such as $\neg \varphi$ or $\varphi \perp$ evaluate either to $0$ (“true”) or to $\mathrm{\infty }$ (“false”). For example:

We call such formulas boolean. They yield derived operators, such as:

These have useful “boolean” meanings. For example:

Using them, we can express useful facts, e.g., $|\varphi |$ says that “$\varphi$ is finite” and $Z\varphi$ that “$\varphi$ is strictly positive”. We use $\varphi \le \psi$ and as synonyms for $\psi \ge \varphi$ and $\psi >\varphi$.

A sequent in $ℝ𝕃$ is a syntactic construct of the form

where $\mathrm{\Gamma }={\varphi }_1,\mathrm{\dots },{\varphi }_n$ is a finite ordered list of formulas, possibly with repetitions, the antecedents of the sequent, and the formula $\varphi$ is its consequent. For $\mathrm{\Gamma }$ and $\mathrm{\Delta }$ such lists of formulas, $\mathrm{\Gamma },\mathrm{\Delta }$ denotes their concatenation; and $⊢\varphi$ is a sequent with no antecedents.

A sequent ${\varphi }_1,\mathrm{\dots },{\varphi }_n⊢\psi$ is satisfied by an interpretation $ℐ$ (alternatively, $ℐ$ is a model for the sequent), denoted $ℐ\vDash ({\varphi }_1,\mathrm{\dots },{\varphi }_n⊢\psi )$, whenever

In particular, $ℐ\vDash (⊢\psi )$ means that $ℐ(\psi )=0$. We write $ℐ\vDash S$ and say that $ℐ$ is a model for $S$ if $ℐ$ satisfies all sequents in $S$. A sequent is satisfiable if it has a model; it is unsatisfiable if it has no models; it is a tautology if it is satisfied by all interpretations. In particular, $⊢\varphi ⊸\varphi$, $⊢\top$, and $⊢\neg \neg \varphi ⧟(\perp >\varphi )$ are tautologies, while $⊢\varphi ⧟(\neg \neg \varphi )$ is not.

Note the distinction between $\varphi ⊸\psi$ and the boolean formula $\varphi \ge \psi$: while for all interpretations $ℐ$, we have $ℐ\vDash (⊢\varphi ⊸\psi )$ iff $ℐ\vDash (⊢\varphi \ge \psi )$, it may not hold that $ℐ(\varphi ⊸\psi )=ℐ(\varphi \ge \psi )$, as $ℐ(\varphi ⊸\psi )$ could be a non-zero finite number.

The total variation distance $d_{TV}(\mu ,\nu )={\max }_{A\subseteq X}|\mu (A)-\nu (A)|$, is encoded in $ℝ𝕃$ by the formula $t_{\mu ,\nu }:-{\bigwedge }_{A\subseteq \{1..n\}}({⨁}_{i\in A}{\mu }_i⧟{⨁}_{i\in A}{\nu }_i)$. A simple example to start with is to demonstrate that the total variation is a pseudo-metric, i.e., satisfies the axioms of reflexivity, symmetry, and triangle inequality, which can be expressed in $\mathbb{P}𝕃$:

The first two are trivial to derive. The derivation of the third is shown below:

Note that (perm) is used implicitly and some steps of the derivation use meta-rules which are derivable from the rules in Table 2, such as (${\wedge }_1$) and (${\wedge }_2$).

The total variation is not just a pseudo-metric, but a proper metric satisfying the Fréchet positivity axiom, which can be expressed in $ℝ𝕃$ by the sequent

The above uses the boolean formulas of $ℝ𝕃$, which can be expressed using multiplication by $\perp$. In fact, this is a non-linear property that cannot be captured by $𝔸𝕃$ as it allows only affine formulas.

The Kantorovich distance³³3Also known as the Wasserstein distance or Earth mover’s distance. between $\mu$ and $\nu$ can be defined using the following two equivalent (dual) formulations

where $\omega$ ranges over joint probability distributions with $\mu$ as left-marginal (i.e., ${\sum }_j{\omega }_{ij}={\mu }_i$, for all $i$) and $\nu$ as right-marginal (i.e., ${\sum }_i{\omega }_{ij}={\nu }_j$, for all $j$); and $f$ over non-expanding $[0,\mathrm{\infty })$-valued maps on $X$, i.e., $|f_i-f_j|\le d_{ij}$, for all $i,j$.

As its definitions involve $inf$ (infimum) on one hand, and $sup$ (supremum) on the other hand, we cannot express the Kantorovich distance as a single formula in $ℝ𝕃$. However, we can still reason about it if we can find a finite set of sequents that uniquely characterises its value. The set we propose, hereafter denoted by $𝒦$, contains the following sequents:

where $W_{ij}$, $F_i$, and $K_{\mu ,\nu }$ are propositional atoms. This set is derived by following the steps of the proof of (strong) duality in linear programs [57], tailored to the K-R duality presented above. The sequents to the left represent the conjunction of the constraints from both the primal and dual linear programs (i.e., the marginal conditions on $\omega$ and the non-expanding condition on $f$). Those to the right imply ${⨁}_i{F}_i{\mu }_i⧟{⨁}_i{F}_i{\nu }_i⊢{⨁}_{i,j}{W}_{ij}{d}_{ij}$, corresponding to the optimality condition for the feasible solutions. The atom $K_{\mu ,\nu }$ is a convenience.

This encoding is such that all the models of $𝒦$ assign the atom $K_{\mu ,\nu }$ value $d_K(\mu ,\nu )$, i.e., the Kantorovich distance between $\mu$ and $\nu$. Indeed, next we show that from $𝒦$ we can deduce

The above follows by deriving the following two sequents from $𝒦$

as they imply ${⨁}_{i,j}{W}_{ij}{d}_{ij}⊢{⨁}_i{F}_i{\mu }_i⧟{⨁}_i{F}_i{\nu }_i$. Note that this corresponds to the steps of the proof of weak duality in linear programs. We show only the derivation of the first one as the other is similar. Below we provide only the schematic steps of the derivation, which would otherwise take too much space

In the above a concatenation of the form $\varphi ⊢\psi ⊢\vartheta$ means that both $\varphi ⊢\psi$ and $\psi ⊢\vartheta$ are derivable; the desired result follows by repeated applications of (cut).

Now that we have established a way to encode the Kantorovich distance, we can prove some of its properties. A well-known result from [27] relating the Kantorovich distance with the total variation is $d_K(\mu ,\nu )\ge d_{\min }\cdot d_{TV}(\mu ,\nu )$, where $d_{\min }={\min }_{i\ne j}{d}_{ij}$. According to our encoding, such a statement is equivalent to establishing the provability of $K_{\mu ,\nu }⊢({\bigvee }_{i\ne j}{d}_{ij})t_{\mu ,\nu }$ from $𝒦$.

Due to a lack of space, below, we provide only the sketch of the proof. The key steps of it are to show that the sequents below follow from $𝒦$ for all $A\subseteq \{1,\mathrm{\dots },n\}$

from which, by using (quant), (${\vee }_2$), one gets ${⨁}_{i\ne j}{W}_{ij}⊢t_{\mu ,\nu }$. Thus, by applying the inference rules of $ℝ𝕃$, (1), and the fact that $d_{ii}=0$ for all $i$, we get

The desired inference follows from the above by repeated applications of (cut).

We showed in in [9] how one can embed the finitary part of QEL in $𝔸𝕃$ (i.e., the axioms and rules of QEL other than its infinitary rule). To do so, we add, as propositional letters in our logic, all the equalities of the form $\mathrm{⌜}s=t\mathrm{⌝}$ for all terms $s,t$ of a chosen quantitative algebra. A quantitative equation such as $⊢s{=}_{\epsilon }t$ is then encoded in Lawvere logic as the sequent $\epsilon ⊢\mathrm{⌜}s=t\mathrm{⌝}$, or equivalently as $⊢\mathrm{⌜}s=t\mathrm{⌝}\le \epsilon$.

Next, a quantitative judgement such as the triangle inequality, which in QA has the form

can be encoded in Lawvere logic as follows, if we want to emphasize $\epsilon$ and $\delta$,

or if $\epsilon$ and $\delta$ are generic, we can use an even more compact encoding that emphasize the relation between triangle inequality and transitivity

The logic $𝔸𝕃$ of [9] lacks a deduction theorem, and the embedding of QEL in $𝔸𝕃$ therefore relied on extending $𝔸𝕃$ with certain inference rules. However, in $ℝ𝕃$ this problem disappears, as the inferences in [9, Table 2] can be formalized as proper sequents using the deduction theorem (Theorem 8), exactly as we have done above for the triangle inequality.

Additionally, while $𝔸𝕃$ can handle only affine functions, $ℝ𝕃$ can encode more complex examples, including polynomials and rational functions and even rational powers.

For instance, interpolative barycentric algebras (IBAs) were introduced in [43] as a quantitative generalization of Stone’s barycentric algebras [59]. Barycentric algebras, sometimes called convex algebras, have binary operators ${+}_e$ for $e\in [0,1]$, where the intended interpretation of $s{+}_{e}t$ on reals or distributions is the $e$-convex combination of $s$ and $t$. To characterize the $p$-Wasserstein metric on the space of distributions for a strictly positive integer $p$, IBAs must satisfy the following axiom:

This can be encoded in $ℝ𝕃$ using a couple of judgements. Let $d$ be a fresh propositional letter; then $(I_p)$ can be represented in $ℝ𝕃$ by:

The compact quantitative algebraic theories of [47] have the property (in the case of QEL) that if a sequent is provable, then it is provable without the infinitary rule. So our finitary encodings of theories in $ℝ𝕃$ are complete for compact theories in that any QEL consequence of such a theory is also, via the encoding, an $ℝ𝕃$ consequence. As shown in [47], the theories of rational Wasserstein metrics are compact, as is the theory of quantitative semilattices [9].

The first reduction comprises the following nine one-move rule schemas. The intent is to reduce the judgments in both the premises and the conclusions of configurations to a simplified canonical form, propositional canonical form (PCF), where logical connectives are applied only to propositional letters.

where $P,Q\in \mathbb{P}$ are fresh propositional letters not occurring in the source configurations of the moves (chosen in a standard way) and at least one among $\varphi$ or $\psi$ is not a propositional letter.

The correctness of the rules follows from the monotonicity properties of the connectives: $\oplus$ and $\times$ are monotone in both arguments; $⊸$ is antimonotone in its first argument and monotone in its second; and $/$ is monotone in its first argument and antimonotone its second.

Observe that, since the rules bring subformulas to the top level, their repeated application ensures that every sequent is eventually brought into PCF. The next phases will keep sequents in this form, except for finitising ones.

The following two rule schemas (the first with three moves) are designed to eliminate all occurrences of $⊸$:

where $P,Q,R$ are propositional letters and $R$, chosen in a standard way, is fresh in the move source configurations. The rule ($⊸$-EL) removes occurrences of $P⊸Q$ on the left-hand side of sequents; its correctness relies on the axioms (lin) and (wem). Dually, the rule ($⊸$-R) removes occurrences of $P⊸Q$ on the right-hand side of sequents; its correctness follows from (quant). The fresh propositional letter $R$ is used to maintain the sequents in PCF. As for the previous phase, repeated applications of these rules ensure the elimination of $⊸$ from all sequents except the finitising ones.

The two rule schemas below (the second one comprising four moves) remove all occurrences of $/$:

where $P,Q,R,T\in \mathbb{P}$ are propositional letters and $R,T$ are fresh in the source configurations (chosen in a standard way). The rule ($/$-EL) removes occurrences of $P/Q$ on the left-hand side of sequents; its correctness follows from (adj). Dually, the rule ($/$-ER) removes $P/Q$ from the right-hand side of sequents; its soundness follows from (lin). The propositional letter $R$ is used to encode that $Q$ is non-zero using the combinations of the sequents $R⊢\perp$ and $QR⊢\perp$; the propositional letter $T$ to maintain the sequent in PCF.

This is a rule schema comprising two moves:

where $P$ is a propositional letter occurring in $S$ such that neither $⊢|P|$ nor $P⊢\perp$ are in $S$.

The moves (F) and ($\perp$) correspond, respectively, to non-deterministically choosing whether $P$ is finite or infinite. This phase is completed when all propositional letters in $S$ have been “tagged” in one of the two ways above. Note that the applicability conditions ensure that the rules are never applied vacuously or repeated twice on the same propositional letter.

Recall that a formula is in polynomial form if it has no occurrences of $\perp$, $⊸$, or $/$. The last two requirements have been taken care of by the previous phases. This phase, which we split into two stages, concerns the first requirement.

Stage 1. It removes the occurrences of infinitary propositional letters ($P⊢\perp$) by means of the following seven rule schemas (the last two comprising two moves each)