Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Propositional Logics for the Lawvere Quantale

Giorgio Bacci, Radu Mardare, Prakash Panangaden, Gordon Plotkin

TL;DR

This work develops three propositional logics over Lawvere's quantale $[0,\infty]$ and provides natural deduction systems with decidable completeness relative to quantale semantics. It analyzes metatheoretical properties, including deduction behavior, totality, normal forms, and the decidability of satisfiability via a normalization-based reduction to affine inequalities, leveraging Motzkin and Fourier–Motzkin results. The authors prove incompleteness in general but obtain completeness for finitely axiomatized theories and a restricted approximate strong completeness in certain settings, employing Hurwicz's form of Farkas' lemma. They also show how quantitative equational logic can be encoded within these logics using inference systems, thus enabling reasoning about distances in extended metric spaces through a single valued predicate. Overall, the paper provides a robust semantic and proof-theoretic foundation for quantale-valued logics and their applications to quantitative algebra and metric reasoning, with avenues for extending to polynomial inequalities via Positivstellensatz.

Abstract

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.

Propositional Logics for the Lawvere Quantale

TL;DR

This work develops three propositional logics over Lawvere's quantale and provides natural deduction systems with decidable completeness relative to quantale semantics. It analyzes metatheoretical properties, including deduction behavior, totality, normal forms, and the decidability of satisfiability via a normalization-based reduction to affine inequalities, leveraging Motzkin and Fourier–Motzkin results. The authors prove incompleteness in general but obtain completeness for finitely axiomatized theories and a restricted approximate strong completeness in certain settings, employing Hurwicz's form of Farkas' lemma. They also show how quantitative equational logic can be encoded within these logics using inference systems, thus enabling reasoning about distances in extended metric spaces through a single valued predicate. Overall, the paper provides a robust semantic and proof-theoretic foundation for quantale-valued logics and their applications to quantitative algebra and metric reasoning, with avenues for extending to polynomial inequalities via Positivstellensatz.

Abstract

Lawvere showed that generalised metric spaces are categories enriched over , 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 -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 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 ; the proof uses Hurwicz's general form of the Farkas' Lemma.
Paper Structure (13 sections, 11 theorems, 34 equations, 3 figures, 2 tables)

This paper contains 13 sections, 11 theorems, 34 equations, 3 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Preliminaries and Notation
  3. Logics for the Lawvere Quantale
  4. Natural Deduction Systems
  5. Deduction Theorems
  6. Totality Lemma
  7. Theories and Models
  8. Normal Forms
  9. Normalization Algorithm
  10. Completeness and Incompleteness
  11. Inference Systems for the Lawvere Quantale
  12. The inference system of Quantitative Algebra
  13. Conclusions

Key Result

theorem 1

Let $\mathcal{L} \in \{ \mathbb{L}, \mathbb{L}_{\mathbbm{1}}, \mathbb{L}_{\mathbbm{1}}^*\}$. If a judgement $\gamma$ is provable from $S$ in $\mathcal{L}$, then $\gamma$ is a semantic consequence of $S$ in $\mathcal{L}$ (in symbols, $S \Vdash_{\mathcal{L}} \gamma$ implies $S \models_{\mathcal{L}} \g

Figures (3)

  • Figure 1: The natural deduction system of $\mathbb{L}$
  • Figure 2: The natural deduction system of $\mathbb{L}_{\mathbbm{1}}^*$ (scalar product rules)
  • Figure 3: Conversion into normal representation: (a) Rule 3 and (b) Rule 5 of the normalization algorithm

Theorems & Definitions (22)

  • definition 1
  • theorem 1: Soundness of LLQ
  • lemma 1: Totality Lemma
  • lemma 2
  • definition 2
  • lemma 3
  • definition 3: Normal form
  • definition 4
  • theorem 2: Normal representation
  • theorem 3: Decidability of satisfiability in LLQ
  • ...and 12 more