Logic Without Syntax

2005/04/04 by Dominic Hughes, Hughes, Dominic
Computer Science · Mathematics · #Category Theory (math.CT) #FOS: Mathematics #Formal Methods in Verification #Logic (math.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #math.CT #math.LO

paper · pdf · doi:10.48550/arxiv.math/0504065

arxiv created 2005/04/04 · openalex publication_date 2005/04/04 · arxiv updated 2009/12/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

This paper presents an abstract, mathematical formulation of classical propositional logic. It proceeds layer by layer: (1) abstract, syntax-free propositions; (2) abstract, syntax-free contraction-weakening proofs; (3) distribution; (4) axioms (p OR NOT p). Abstract propositions correspond to objects of the category G(Rel^L) where G is the Hyland-Tan double glueing construction, Rel is the standard category of sets and relations, and L is a set of literals. Abstract proofs are morphisms of a tight orthogonality subcategory of Gl(Rel^L), where we define Gl as a lax variant of G. We prove that the free binary product-sum category (contraction-weakening logic) over L is a full subcategory of Gl(Rel^L), and the free distributive lattice category (contraction-weakening-distribution logic) is a full subcategory of Gl(Rel^L). We explore general constructions for adding axioms, which are not Rel-specific or (p OR NOT p)-specific.

Citations

• Complement reducible graphs
• Natural deduction and coherence for weakly distributive categories
• Linear logic

Related

• Category theoretic semantics for theorem proving in logic programming: embracing the laxness
• Bicategorical Models of Classical Propositional Logic
• Modelling Linear Logic Without Units (Preliminary Results)
• Axiomatizing Category Theory in Free Logic
• Logic programming: laxness and saturation