index 5f225d3..57158c6 100644 (file)
@@ -188,7 +188,7 @@ roughly as follows:
If a variable `x` has type &sigma; and term `M` has type &tau;, then
the abstract `\xM` has type &sigma; `-->` &tau;.

-If a term `M` has type &sigma; `-->` &tau, and a term `N` has type
+If a term `M` has type &sigma; `-->` &tau;, and a term `N` has type
&sigma;, then the application `MN` has type &tau;.

These rules are clearly obverses of one another: the functional types
@@ -205,32 +205,32 @@ Axiom: ---------

Structural Rules:

-Exchange: &Gamma;, A, B, &Delta; |- C
-          ---------------------------
-          \$Gamma;, B, A, &Delta; |- C
+          &Gamma;, A, B, &Delta; |- C
+Exchange: ---------------------------
+          &Gamma;, B, A, &Delta; |- C

-Contraction: &Gamma;, A, A |- B
-             -------------------
+             &Gamma;, A, A |- B
+Contraction: -------------------
&Gamma;, A |- B

-Weakening: &Gamma; |- B
-           -----------------
+           &Gamma; |- B
+Weakening: -----------------
&Gamma;, A |- B

Logical Rules:

---> I:   &Gamma;, A |- B
-         -------------------
+         &Gamma;, A |- B
+--> I:   -------------------
&Gamma; |- A --> B

---> E:   &Gamma; |- A --> B         &Gamma; |- A
-         -----------------------------------------
+         &Gamma; |- A --> B         &Gamma; |- A
+--> E:   -----------------------------------
&Gamma; |- B
</pre>

`A`, `B`, etc. are variables over formulas.
&Gamma;, &Delta;, etc. are variables over (possibly empty) sequences
-of formulas.  `&Gamma; |- A` is a sequent, and is interpreted as
+of formulas.  &Gamma; `|- A` is a sequent, and is interpreted as
claiming that if each of the formulas in &Gamma; is true, then `A`
must also be true.

@@ -262,7 +262,7 @@ Axiom: -----------
Structural Rules:

Exchange: &Gamma;, x:A, y:B, &Delta; |- R:C
-          --------------------------------------
+          -------------------------------
&Gamma;, y:B, x:A, &Delta; |- R:C

Contraction: &Gamma;, x:A, x:A |- R:B
@@ -280,13 +280,17 @@ Logical Rules:
&Gamma; |- \xM:A --> B

--> E:   &Gamma; |- f:(A --> B)      &Gamma; |- x:A
-         ---------------------------------------------
+         -------------------------------------
&Gamma; |- (fx):B
</pre>

In these labeling rules, if a sequence &Gamma; in a premise contains
labeled formulas, those labels remain unchanged in the conclusion.

+What is means for a variable `x` to be chosen *fresh* is that
+`x` must be distinct from any other variable in any of the labels
+used in the proof.
+
Using these labeling rules, we can label the proof
just given:

@@ -303,6 +307,9 @@ x:A |- (\y.x):(B --> A)

We have derived the *K* combinator, and typed it at the same time!

+Need a proof that involves application, and a proof with cut that will
+show beta reduction, so "normal" proof.
+
[To do: add pairs and destructors; unit and negation...]

Excercise: construct a proof whose labeling is the combinator S.