Categorical Proof Theory of Classical Propositional Calculus

Short Description
Categorical Proof Theory of Classical Propositional. Calculus. Gianluigi Bellin. a. Martin Hyland. b. Edmund Robinson. a. Christian Urban …

Website: www.cs.bath.ac.uk | Filesize: 183kb

Content
Categorical Proof Theory of Classical Propositional
Calculus
Gianluigi Bellin a Martin Hyland b Edmund Robinson a
Christian Urban c
aQueen Mary, University of London, UK
bUniversity of Cambridge, UK
cUniversity of Munich (LMU), D
Abstract
We investigate semantics for classical proof based on the sequent calculus. We show that
the propositional connectives are not quite well-behaved from a traditional categorical perspective,
and give a more refined, but necessarily complex, analysis of how connectives
may be characterised abstractly. Finally we explain the consequences of insisting on more
familiar categorical behaviour.
Key words: classical logic, proof theory, category theory
1 Introduction
In this paper we describe the shape of a semantics for classical proof in accord with
Gentzen’s sequent calculus. For constructive proof we have the familiar correspondence
between deductions in minimal logic and terms of a typed lambda calculus. Deductions
in minimal logic (as in most constructive systems) reduce to a unique normal form, and
around 1970 Per Martin-L¨of (see [18]) suggested using equality of normal forms as
the identity criterion for proof objects in his constructive Type Theories: normal forms
serve as the semantics of proof. But ??-normal…