Pith. sign in

REVIEW 3 cited by

Polynomial Lawvere Logic

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 2402.03543 v3 pith:7HQDGJ2K submitted 2024-02-05 cs.LO

Polynomial Lawvere Logic

Giorgio Bacci , Radu Mardare , Prakash Panangaden , Gordon Plotkin This is my paper
classification cs.LO
keywords judgementslawverelogiccompletecompletenessextendedpolynomialpositive
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved
0 comments
read the original abstract

We study Polynomial Lawvere logic PL, a logic defined over the Lawvere quantale of extended positive reals with sum as tensor, to which we add multiplication, thereby obtaining a semiring structure. PL is designed for complex quantitative reasoning, allowing judgements that express inequalities between polynomials on the extended positive reals. We introduce a deduction system and demonstrate its expressiveness by deriving a classical result from probability theory relating the Kantorovich and the total variation distances. Although the deductive system is not complete in general, we achieve completeness for finitely axiomatizable theories. The proof of completeness relies on the Krivine-Stengle Positivstellensatz (a variant of Hilbert's Nullstellensatz). Additionally, we provide new complexity results, both for PL and its affine fragment AL, regarding two decision problems: satisfiability of a set of judgements and semantical consequence from a set of judgements. The former is NP-complete in AL and in PSPACE for PL; the latter is co-NP complete in PL and in PSPACE for PL.

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 3 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. Adequate Losses via Quantitative Linear Logic

    cs.LO 2026-05 unverdicted novelty 8.0

    pQLL calculi make proof validity and sequent provability real-valued quantities, generalizing hypersequent calculi and deep inference while proving cut-elimination and completeness for soft residuated lattices.

  2. Adequate Losses via Quantitative Linear Logic

    cs.LO 2026-05 accept novelty 8.0

    pQLL calculi assign real-valued strength to proofs, generalize hypersequent and deep inference systems, prove cut elimination, and achieve completeness for soft residuated lattices, recovering MALL as p goes to infinity.

  3. Adequate Losses via Quantitative Linear Logic

    cs.LO 2026-05 conditional novelty 7.0

    pQLL is a quantitative linear logic with real-valued provability and smooth soft additives, complete for softale semantics, converging to MALL as p→∞.