IA038 Types and Proofs
4. The Curry-Howard Isomorphism
Jiří Zlatuška March 14, 2023
i
2
3.1.2. Terms using another formulation
r,x:Uhv:V T h t : A h « : U
T\-u:U   A\- v :V
^TJk^tu^ V
►-E
x-I
rhi:f/xF r h 7r\t : C7
x-lE
rht:[/xF T h 7T2t : V
x-2E
or expressed in logic notation
Id
\..r :l      r :\ V h /
r h Xx.v
F\-u:U   a \~a ■ V
r, a h (u,v)
p Axiom [parcel p] wJv A\-u
I
E
F,A\-tu:V
T\-7tH:U
■IE
r\-7T2t:V
A-2E
3
3.1.4 Conversion
Conversion expressed using alternative logical system for ND
T,x : U\-v : V
--►-I
&\-u: U
5
A few bits of history dates
1934 Gentzen's Natural Deduction 1940 Church's Lambda-Calculus
1956^Pjgjgs4^ published normalization of Natural deduction proofs directly (Gentzen used Sequent Calculus, even though a direct proof inJMJXlay^h«^^ in his writings l)
^(^1956^Curry and Feys published Combinatory Logic, a system based purely on combinators
without variables; the types of basic combibators (I, K, S) corresponded to Hilbert axioms for Propositional Logic
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
roofJTheoQL
Lamb<ia=c|ücul
variable (in terms) <6 term ^ type variable type
)e ccj^jvninto Jttypable term Iredex
eduction/cq value
assumption
proof (construction)
propositional variable
formula ------
o^icah^ construction of a proposition
redundancy within a proof structure, lemma usage
\ redundancy wi irtation -^^^maTJzation^
proof/'constructions normalization
form
8
Asidef(Combinatory Loffic and Hilbert-style systems
JCIojaftbraatorial terms over alphabet consisting of constants ~K-a^(b^a)^ S(a^>(b^>c)^>((a^>b)^>(a^>c)): for evervA B, C G Typ, and typed variables xt G Ct:
Hilbert system
Two axiom schemes
and Modus Ponens:
P e Ca^b     Q gCa (PQ) e Cb
xeCJ
x var of type T
((A ^{B^ C))    OA^B) ^{A^ C))
9
Exam
Proof
JHilbert 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)
A => A
This corresponds to a termyiSlOK : A =>• A
Example of term normalization
11
u : U v.V -A-I
(u, v) : UAV
-A-2E
7ľ2(u, v) : U
12
(7T2(y,x),7T1(y,x)) :AxB
14
Using logic notation
T,x : U\-v : V
T h Xx.v :U^V
-I
Ah«:[/
T, A h (Xx.t)u T\-u:U Ahv
T, A h : U
K-I
A-2E
r,Aht[M/x] :V
T\-u:U
A\-v
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 AA\- t\xz : A
ldz A-1E
z : B A A h (^z.^z) : A A B \- XzJtt%7t\zU (B A A)     (A A B)
A-I
y.Bhy.B
Id,
x : A\- x : A
x : A,y : B \- (y, x) : B A A
Id* A-I
: A, 2/ : 5 h (Az.(7r2z, 7r1^>)((2/, £>) : A A 5
-E
/3-conversion
y.Bhy.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, y : 5 h 7T2(y,x) : A
A-2E
x : A,y : B \- (y,x) : B A A
A-I
a : A, j/ : 5 h ^(y.x) : A
A-1E
£ : A, 2/ : B h (tt2(j/, x),7r1(y, x)) : A A B
A-I
18
19
20