ONT Re: Higher Order Categorical Logic
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
Note 21
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
| A 'positive intuitionistic propositional calculus' is a conjunction calculus
| with an additional binary operation '<=' (= if). Thus, if A and B are formulas,
| so are T, A & B, and A <= B. (Yes, most people write B => A instead.) We also
| specify the following new arrow and rule of inference:
|
| !e!_A,B
| R4a. (A <= B) & B ---------> A,
|
| h
| C & B ---> A
| R4b. ----------------.
| h*
| C ----> A <= B
|
| Actually we should have written h* = !L!^C_A,B (h),
| but the subscripts are usually understood from context.
|
| We note that from R4b, with the help of R4a, one may derive
|
| !h!_C,B
| R'4b. C ---------> (C & B) <= B,
|
| g
| D ---> A
| R'4c. -------------------------------.
| g <= 1_B
| (D <= B) ----------> (A <= B)
|
| To derive these, we put
|
| !h!_C,B = (1_C&B)*,
|
| (g <= 1_B) = (g !e!_D,B)*.
|
| Conversely, one may derive R4b from R'4b and R'4c by putting
|
| h* = (h <= 1_B) !h!_C,B.
|
| For future reference, we also note the following two
| derived rules of inference:
|
| f
| A -----> B
| -----------------,
| #f
| T -----> B <= A
|
| g
| T -----> B <= A
| -----------------,
| g`
| A -----> B
|
| where
|
| #f = (f p2_1,A)*,
|
| g` = !e!_B,A <g O_A, 1_A>.
|
| L&S, pages 48-49.
|
| Lambek, J. & Scott, P.J.,
|'Introduction To Higher Order Categorical Logic',
| Cambridge University Press, Cambridge, UK, 1986.
|
| http://uk.cambridge.org/mathematics/catalogue/0521356539/
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤