IA038 Types and Proofs
4. The Curry-Howard Isomorphism
Jiří Zlatuška March 14, 2023
i
2
3.1.2. Terms using another formulation
-ldp      Axiom [parcel p]
r,x:U\-v:V V h t : U     V A\~u:U
--->-E
T\-Xx.v:U^V T,A\-tu:V
T\-u:U   A\- v :V T h t : U x V T \-t : U x V
-x-I -x-lE -x-2E
V,A\-{u,v):U xV T\-7tH:U T h tt2£ : V
or expressed in logic notation
ldp      Axiom [parcel p]
T,x:U\-v:V T h Xx.v : C7=>F rh«:[/ Ahi;:y
>-I
r h t : £/=>y Ah«:[/ T, A h tu : F
-E
r, A h^j) : UAV
A-I
r h t : CMF ri-Tr1*: £/
A-1E
r h ttH : y
A-2E
3
3.1.4 Conversion
Expressed using Natural Deduction derivation trees
[x : U]x
v : V
Xx.v :U^V
—>-Ia
(Xx.v)u : V
u:U v.V
(u,v) : U x V tt^ (u, v) : U
X-I
x-lE
u:U v.V
(u,v) : U x V tt2(u, v) : C/
X-I
x-2E
Conversion ej
.alternative logical system for ND
T,x:U\~v:V
T h Xx.v : U V
r, A h (Xx.t)u : y
T\-u:U Ah?; : y T, A h (u,v) : U x V
x-I x-lE
T\-u:U A\-v:V T, A h (u,v) : C7 x V T,A\-7T2(u,v) : C7
x-I x-2E
T,A\-t[u/x] :V
T\-u:U
A\- v :V
5
A few bits of history dates
1934 Gentzen's Natural Deduction
T94Y) Church's Lambda-Calculus
1956/Prawitz published normalization of Natural deduction proofs directly (Gentzen used Sequent Calculus, even though a direct proof in ND by him was recently discovered in his writings 1)
1956 >^Jurry and Feys published Combinatory Logic, a system based purely on combinators
without variables; the types of basic combibatois (I, K, S) corresponded to Hilbert axioms for Propositional Logic <4--■-^
oward combined results of Prawitz, Curry and Feys into the correspondence/isomorphism oward's worh published in "To H. B. Curry", a festschrift for Curry's 80 birthday
1 Plato and Gentzen: Gentzen's Proof of Normalization for Natural Deduction, The Bulletin of Symbolic Logic, Vol. 14, No. 2, June 2008, 240-257
7
Some essential pieces of the correspondence
Lambda-calculus
-to
Proof Theory
variable (in terms) term
type variable type
type constructor typable term redex
reduction/computation
assumption proof (construction) - propositional variable formula
logical operation construction of a proposition
redundancy within a proof structure, lemma usage
^pnrmalJ^tl'PP
j computation
t^roof/coristruction in normal form 1 normalization-1 -—■
8
Aside: Combinatory Logic and Hilbert-style systems
Combinatorial terms over alphabet consisting of constants ~Ka=>(b=>A)j S(a^>(b^C)^((a^b)^(a^c))7 for every A, B, C G Typ, and typed variables xt £ CT' ^=   ^ ■ r^*---—
A^(B^A)
g qA^(B^-A) g
(a=>(b=>c))=>((a=>b)=>(a=>c))
£(a=>(b=>c))=>((a^b)=>(a
Hilbert system
Two axiom schemes
4)   A^(B^ A)
7   ((A ^{B^ C))     ((A ^B)^(A^ C))
and Modus Ponens:
9
Exam
Proof o!
in Hilbert system:
Hilbert system proof: ^
(A    {{B    A)    A))     {{A ^(B^ A)) ^ (A ^ A))      A =>\(B    A) A\
(A^(B^A)^(A^ A)
A^(B^A)
This ffiorresponds to a term (SK)K : A =>• A
A => A
a^((b^a)^a)
a^(b^a)
Example of term normalization
(\z.{K2zpKlz))({y,x)) —>(3 (7T2(u,x),7T1(y,x)) —^second {x^l{y,x)) —>first (x,y)
11
Natural Deduction definition of conversion/proof simplification
[x :Uf
J
v : V
Xx.v :U^V
it : U
(Xx.v)u : V u:U v:V
(u,	V)	: UAV
TT1	(u,	v) : U
it :	U	v : V
(u,	v)	: CMF
TT2	(it,	i;) : U
A-I A-1E
A-I A-2E
-E i;[it/ic] : V
it : C7
i; : V
12
[z:_B x A]' 7ľ2z : A r-
X-2E
[z: B x AY ttxz \ A
[tt'
,'z,7T1z) : Ax B
Xz.^yz) : (B x A) -)> (A x B)
x-lE x-I
\
\
[y : B]y       [x : A]1
(y, x) : B x A
x-
(Xz.{7r2z,7r1z))({y,x)) :ixß
[ž/ : B]y       [x : A]£
(ž/, x) : B x A
x-I
/3-conversion
[y : 5]«       [x : A]£
n2 (y, x) : A
X-2E
(ž/, a;) : B x A
x-I
A"1 (ž/, z) : A
x-lE
pairing
x-I
[x : 4*       [V : £?ľ (a;, ž/) : A x B
x-I
14
Using logic notation
T,x:U\~v:V
-I
T h Xx.v :U^V A\-u:U r, A h (Xx.t)u : V
T\-u:U A\-v:V
A-I
-E T,A\-t[u/x]:V
T, A h (u,v) : C/ AV
-.-A-1E rhu:[/
r, A h tt^u.v) : U
T\-u:U A\-v:V -A-I
T, A h (u,v) : U AV
-L—L-A-2E A h v : V
r, A h ir2(u,v) : U
15
Proof simplification using the logic-based system
z:BAA\-z:BAA z : B A A h tt2z : A
ldz A-2E
z:BAA\-z:BAA
z : B AAV kxz : A
Id, A-1E
z : B A A h (^z.^z) : A A B h Az.(tt2z, tt1*) :(BAi)^(iAB)
A-I
B\-y: B
Id,
x : A\- x : A
x : A,y : B \- (y, x) : B A A
x : A7y : B\- (Xz.(tt2z7 7r1z))((2/, #)) : A A B
-E
/3-conversion
y:B\-y: B
Id,
x : A\- x : A
Id,
x : A,y : B \- (y, x) : B A A
A-I
y:B\-y:B
Id,
x : A\- x : A
Id,
a : A, 2/ : 5 h 7T2(y7x) : A
A-2E
a : A, 2/ : B h (2/, a) :5Ai
A-I
a : A, 2/ : B h ^(y.x) : A
A-1E
£ : A, 2/ : 5 h (tt2(j/, x),7T1(y, x)) : A A B
A-I
pairing
x : A\- x : A
Id,
x : A,y : B \- (x,y) : A A B
Idy
A-I
16
18
19
20