Dominic Hughes - Selected Papers

Logic Without Syntax [pdf - ps - ps.gz - bibtex]
January 2005. Archived as math.LO/0504065 at (with minor corrections), April 4, 2005.

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¬p.

Abstract propositions correspond to objects of the category G(RelL) 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 G(RelL), where we define G as a lax variant of G. We prove that the free product-sum category (contraction-weakening logic) over L is a full subcategory of G(RelL), and the free distributive lattice category (contraction-weakening-distribution logic) is a full subcategory of G(RelL). We explore general constructions for adding axioms, which are not Rel-specific or (p¬p)-specific.

[Note: this paper supercedes this old technical report.]