ONT Re: Higher Order Categorical Logic
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
Note 13
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
I am skipping ahead to Part 1 of L&S -- we have been reading
from Part 0 (Introduction to Category Theory) all this time --
in order to pick up a quantum of motivation for the endeavor.
| Part 1. Cartesian Closed Categories & Lambda Calculus
|
| Introduction to Part 1
|
| Lambda calculus or combinatory logic is a topic that logicians have studied
| since 1924. Cartesian closed categories are more recent in origin, having
| been invented by Lawvere (1964, see also Eilenberg & Kelly, 1966). Both are
| attempts to describe axiomatically the process of substitution, so it is not
| surprising to find that these two subjects are essentially the same. More
| precisely, there is an equivalence of categories between the category of
| cartesian closed categories and the category of typed lambda calculi with
| surjective pairing. This remains true if cartesian closed categories are
| provided with a weak natural numbers object and if typed lambda calculi
| are assumed to have a natural numbers type with iterator.
|
| This result depends crucially on the 'functional completeness' of cartesian
| closed categories, which goes back to the functional completeness of combinatory
| logic due to Schoenfinkel and Curry. It asserts, in particular, that every arrow
| !f!(x) : 1 -> B expressible as a polynomial in an indeterminate arrow x : 1 -> A
| over a cartesian closed category $A$ (with given objects A and B) is uniquely
| of the form
|
| x f
| 1 ---> A ---> B,
|
| where f is an arrow in $A$ not depending on x.
|
| Functional completeness is closely related to the 'deduction theorem' for
| positive intuitionistic propositional calculi presented as deductive systems.
| In our version, it associates with each proof T |- B on the assumption T |- A
| a proof of A |- B without assumptions. However, functional completeness goes
| beyond this; it asserts that the proof of T |- B on the assumption T |- A is,
| in some sense, 'equivalent' to the proof by transitivity:
|
| T |- A A |- B
| --------------------.
| T |- B
|
| Deductive systems are also used to construct free cartesian closed categories
| generated by graphs, whose arrows A -> B are equivalence classes of proofs.
|
| L&S, page 41.
|
| Lambek, J. & Scott, P.J.,
|'Introduction To Higher Order Categorical Logic',
| Cambridge University Press, Cambridge, UK, 1986.
|
| http://uk.cambridge.org/mathematics/catalogue/0521356539/
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤