English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Lawvere showed that generalised metric spaces are categories enriched over$[0, \infty]$, the quantale of the positive extended reals. The statement ofenrichment is a quantitative analogue of being a preorder. Towards seeking alogic for quantitative metric reasoning, we investigate three$[0,\infty]$-valued propositional logics over the Lawvere quantale. The basiclogical connectives shared by all three logics are those that can beinterpreted in any quantale, viz finite conjunctions and disjunctions, tensor(addition for the Lawvere quantale) and linear implication (here a truncatedsubtraction); to these we add, in turn, the constant $1$ to express integervalues, and scalar multiplication by a non-negative real to express generalaffine combinations. Quantitative equational logic can be interpreted in thethird logic if we allow inference systems instead of axiomatic systems. Foreach of these logics we develop a natural deduction system which we prove to bedecidably complete w.r.t. the quantale-valued semantics. The heart of thecompleteness proof makes use of the Motzkin transposition theorem. Consistencyis also decidable; the proof makes use of Fourier-Motzkin elimination of linearinequalities. Strong completeness does not hold in general, even (as is known)for theories over finitely-many propositional variables; indeed even anapproximate form of strong completeness in the sense of Pavelka or Ben Yaacov-- provability up to arbitrary precision -- does not hold. However, we can showit for theories axiomatized by a (not necessarily finite) set of judgements innormal form over a finite set of propositional variables when we restrict tomodels that do not map variables to $\infty$; the proof uses Hurwicz's generalform of the Farkas' Lemma.

Propositional Logics for the Lawvere Quantale