January 2005. Archived as math.LO/0504065 at arXiv.org (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**(**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 **G**_{≤}(**Rel**^{L}), 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**(**Rel**^{L}), and the free distributive lattice category
(contraction-weakening-distribution logic) is a full subcategory of
**G**_{≤}(**Rel**^{L}). We explore general constructions for adding axioms,
which are not **Rel**-specific or
(*p*∨¬*p*)-specific.

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