If a variable `x` has type σ and term `M` has type τ, then
the abstract `\xM` has type σ `-->` τ.
-If a term `M` has type σ `-->` &tau, and a term `N` has type
+If a term `M` has type σ `-->` τ, and a term `N` has type
σ, then the application `MN` has type τ.
These rules are clearly obverses of one another: the functional types
Structural Rules:
-Exchange: Γ, A, B, Δ |- C
- ---------------------------
- $Gamma;, B, A, Δ |- C
+ Γ, A, B, Δ |- C
+Exchange: ---------------------------
+ Γ, B, A, Δ |- C
-Contraction: Γ, A, A |- B
- -------------------
+ Γ, A, A |- B
+Contraction: -------------------
Γ, A |- B
-Weakening: Γ |- B
- -----------------
+ Γ |- B
+Weakening: -----------------
Γ, A |- B
Logical Rules:
---> I: Γ, A |- B
- -------------------
+ Γ, A |- B
+--> I: -------------------
Γ |- A --> B
---> E: Γ |- A --> B Γ |- A
- -----------------------------------------
+ Γ |- A --> B Γ |- A
+--> E: -----------------------------------
Γ |- B
</pre>
`A`, `B`, etc. are variables over formulas.
Γ, Δ, etc. are variables over (possibly empty) sequences
-of formulas. `Γ |- A` is a sequent, and is interpreted as
+of formulas. Γ `|- A` is a sequent, and is interpreted as
claiming that if each of the formulas in Γ is true, then `A`
must also be true.
Structural Rules:
Exchange: Γ, x:A, y:B, Δ |- R:C
- --------------------------------------
+ -------------------------------
Γ, y:B, x:A, Δ |- R:C
Contraction: Γ, x:A, x:A |- R:B
Γ |- \xM:A --> B
--> E: Γ |- f:(A --> B) Γ |- x:A
- ---------------------------------------------
+ -------------------------------------
Γ |- (fx):B
</pre>
In these labeling rules, if a sequence Γ 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:
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.