ONT Re: Higher Order Categorical Logic
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
Note 23
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
| 2. The Deduction Theorem
|
| The usual deduction theorem asserts:
|
| if A & B |- C then A |- C <= B.
|
| This result is here incorporated into R4,
| with the deduction symbol '|-' replaced
| by actual arrows in the appropriate
| deductive system $L$:
|
| h : A & B -> C
| ------------------.
| h* : A -> C <= B
|
| However, at a higher level, the horizontal bar
| functions as a deduction symbol, and we obtain
| a new form of the deduction theorem. It deals
| with proofs from an 'assumption' x : T -> A.
|
| In other words, we form a new deductive system $L$(x) by adjoining a new
| arrow x : T -> A and talk about proofs !f!(x) : B -> C in this new system.
| More precisely, $L$(x) has the same formulas (= objects) as $L$ and its
| proofs (= arrows) !f!(x) are freely generated from those of $L$ and the
| new arrow x by the appropriate rules of inference (= operations).
| Clearly, if $L$ is a conjunction calculus (positive calculus,
| intuitionistic calculus, classical calculus, respectively),
| so is the new deductive system $L$(x).
|
| Proposition 2.1. (Deduction Theorem). In a conjunction,
| positive, intuitionistic, or classical calculus, with every
| proof !f!(x) : B -> C from the assumption x : T -> A there is
| associated a proof f : A & B -> C in $L$ not depending on x.
|
| We write
|
| f = !k!_x:A !f!(x),
|
| where the subscript "x : A"
| indicates that x is of type A.
|
| Proof. [L&S, pages 51-52].
|
| Remark 2.1. Logicians don't usually talk of an assumption x : T -> A
| if there is a known proof a : T -> A or another assumption y : T -> A,
| but from our algebraic viewpoint this does not matter.
|
| The reader is warned that we do not distinguish notationally
| between composition of proofs g o f in $L$ and in $L$(x).
|
| In $L$
|
| !k!_x:A (gf) = g f p2_A,B,
|
| and in $L$(x) it is
|
| !k!_x:A (gf) = g p2_A,B <p1_A,B, f p2_A,B>.
|
| L&S, pages 50-52.
|
| Lambek, J. & Scott, P.J.,
|'Introduction To Higher Order Categorical Logic',
| Cambridge University Press, Cambridge, UK, 1986.
|
| http://uk.cambridge.org/mathematics/catalogue/0521356539/
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤