Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

On propositional logic semirings

Wenxi Li, Zhongzhi Wang

TL;DR

This work develops an algebraic framework for propositional logic by modeling it with an idempotent-complement semiring $S_c[X]$ on a countable atom set $X$, where $x_i\cdot x_j$ denotes conjunction and $x_i\circ x_j$ disjunction. It then employs Gröbner-Shirshov bases to define a deduction calculus: provability $\Gamma\vdash\beta$ is equivalent to $\beta-1$ being trivial modulo the ideal generated by $\{\alpha-1:\alpha\in\Gamma\}$, and the single-step entailment $\alpha\vdash\beta$ corresponds to $\alpha^c\circ\beta=1$. The construction proceeds both for finitely generated cases, with a normal form $\{1,\sum^{\circ}_{k\in D} y_k\}$, and for countable generators via a direct-limit $S_c[X]$, establishing a universal property and freeness of the $I$-$C$ semiring. Through a sequence of examples, the paper illustrates how semantic entailment translates into semiring computations and discusses limitations in reducing proof complexity for large instances. Overall, the work provides a rigorous algebraic lens on logical deduction with potential implications for symbolic reasoning and automated proof systems.

Abstract

Propositional logic serves as a fundamental cornerstone in mathematical logic. This paper delves into a semiring characterization of propositional logic, employing the Gröebner-Shirshov basis theory to furnish an algebraic framework for deduction and proof grounded in atoms of propositional logic. The result is an algebraic approach to proving propositions in propositional logic. To illustrate the effectiveness and constraints of this method, we conclude with several specific examples.

On propositional logic semirings

TL;DR

This work develops an algebraic framework for propositional logic by modeling it with an idempotent-complement semiring on a countable atom set , where denotes conjunction and disjunction. It then employs Gröbner-Shirshov bases to define a deduction calculus: provability is equivalent to being trivial modulo the ideal generated by , and the single-step entailment corresponds to . The construction proceeds both for finitely generated cases, with a normal form , and for countable generators via a direct-limit , establishing a universal property and freeness of the - semiring. Through a sequence of examples, the paper illustrates how semantic entailment translates into semiring computations and discusses limitations in reducing proof complexity for large instances. Overall, the work provides a rigorous algebraic lens on logical deduction with potential implications for symbolic reasoning and automated proof systems.

Abstract

Propositional logic serves as a fundamental cornerstone in mathematical logic. This paper delves into a semiring characterization of propositional logic, employing the Gröebner-Shirshov basis theory to furnish an algebraic framework for deduction and proof grounded in atoms of propositional logic. The result is an algebraic approach to proving propositions in propositional logic. To illustrate the effectiveness and constraints of this method, we conclude with several specific examples.
Paper Structure (5 sections, 17 theorems, 6 equations)

This paper contains 5 sections, 17 theorems, 6 equations.

Table of Contents

  1. Introduction
  2. Gröbner-Shirshov bases for finitly generated semirings
  3. Idempotent complement semirings
  4. propositional logical semirings
  5. Examples

Key Result

Theorem 2.1

NLW Let the ordering on $Rig[\tilde{X}\cup Y]$ be as above. Then $kRig[\tilde{X}\cup Y|\{(x_{i}\cdot x^{c}_{i},\theta),(x_{i}\circ x^{c}_{i},1),(x_{i}\circ x_{i},x_{i}),(x^{c}_{i}\circ x^{c}_{i},x^{c}_{i}),(y_{k},x^{k_{1}}_{1}\cdot \cdots \cdot x^{k_{n}}_{n})\}]= kRig[\tilde{X}\cup Y|R_{1}]$ and $R_

Theorems & Definitions (37)

  • Definition 2.1
  • Theorem 2.1
  • Definition 2.2
  • Proposition 3.1
  • proof
  • Proposition 3.2
  • Proposition 3.3
  • proof
  • Lemma 4.1
  • proof
  • ...and 27 more