This book in categorial proof theory formulates in terms of
category theory a generalization close to linear algebra of the
notions of distributive lattice and Boolean algebra. These notions
of distributive lattice category and Boolean category codify a
plausible nontrivial notion of identity of proofs in classical
propositional logic, which is in accordance with Gentzen's
cut-elimination procedure for multiple-conclusion sequents modified
by admitting new principles called union of proofs and zero proofs.
It is proved that these notions of category are coherent in the
sense that there is a faithful structure-preserving functor from
freely generated distributive lattice categories and Boolean
categories into the category whose arrows are relations between
finite ordinals-a category related to generality of proofs and to
the notion of natural transformation. These coherence results yield
a simple decision procedure for equality of proofs. Coherence in
the same sense is also proved for various more general notions of
category that enter into the notions of distributive lattice
category and Boolean category. Some of these coherence results,
like those for monoidal and symmetric monoidal categories are well
known, but are here presented in a new light. The key to this
categorification of the proof theory of classical propositional
logic is distribution of conjunction over disjunction that is not
an isomorphism as in cartesian closed categories.
General
Is the information for this product incomplete, wrong or inappropriate?
Let us know about it.
Does this product have an incorrect or missing image?
Send us a new image.
Is this product missing categories?
Add more categories.
Review This Product
No reviews yet - be the first to create one!
Welcome to Loot.co.za!
Sign in / Register |Wishlists & Gift Vouchers |Help | Advanced search
