A Concrete Category of Classical Proofs

from blog Home on consequently.org, | ↗ original
Abstract: I show that the cut-free proof terms defined in my paper “Proof Terms for Classical Derivations” form a well-behaved category. I show that the category is not Cartesian—and that we’d be wrong to expect it to be. (It has no products or coproducts, nor any initial or final objects. Nonetheless, it is quite well behaved.) I show that the...