Curry-Howard isomorphism

Curry-Howard isomorphism formulas as types For the sake of this definition, if P is a proposition, we let $[\![P]\!]$be the corresponding type, and if p is a proof expression, we let $[\![p]\!]$ be the corresponding element of $[\![P]\!]$. We proceed to define $[\![~~]\!]$ inductively on the structure of proposition Pfrom section 2.5.

1.

We consider only atomic propositions of the form a=b in A. The type $[\![a=b\ \mbox{in}\ A]\!]$ will have the atomic proof object axiom if the proposition is axiomatically true.
If the proof expression e for a=b in A evaluates to a canonical proof built only from equality rules, then we arrange that $e \downarrow axiom$. This is a simple form of correspondence that ignores equality information. For instance

$[\![symmetry(3)]\!]\downarrow axiom\ \ \ [\![transitivity(e_1, e_2)]\!]\downarrow axiom.$

$\frac{\displaystyle [\![e]\!] \downarrow e'}{\displaystyle [\![equality\_intro(e)]\!]\downarrow e'}$

We also need these evaluation rules for the proof expressions for substitution and type equality.

$\frac{\displaystyle [\![p]\!]\downarrow p'}{\displaystyle [\![subst(p; e)]\!]\d... ...splaystyle [\![p]\!]\downarrow p'}{\displaystyle [\![eq(p; e)]\!]\downarrow p'}$

2.

$[\![P\ \&\ Q]\!] = [\![P]\!] \times [\![Q]\!]$ and
$[\![\&\!R(e_1, e_2)]\!] = pair([\![e_1]\!]; [\![e_2]\!]),$ and
$[\![\&\!L(e_1; u, v.\ e_2)]\!] = [\![e_2]\!] (1o\!f([\![e_1]\!]) / u, 2o\!f([\![e_1]\!] / v)).$

3.

$[\![P\vee Q]\!] = [\![P]\!] + [\![Q]\!]$,
$[\![V\!Rl(a)]\!] = inl([\![a]\!])$,
$[\![V\!Rr(b)]\!] = inr([\![b]\!])$,
$[\![V\!L(d; u.\ e_1; v.\ e_2)]\!] = decide([\![d]\!]; u.[\![e_1]\!]; v. [\![e_2]\!])$.

4.

$[\![P\Rightarrow Q]\!] = [\![P]\!] \rightarrow [\![Q]\!]$,
$[\![\Rightarrow\!\!R(x.\ e)]\!] = \lambda(x. [\![e]\!])$,
$[\![\Rightarrow\!\!L(f; p; y.\ q)]\!] = [\![g]\!] [ap([\![f]\!]; [\![p]\!]/y]$.

5.

$[\![\exists x\!:\!A.\ P[x]]\!] = prod(A; x.\ [\![P[x]]\!])$,
$[\![\exists R(a; p)]\!] = pair(a; [\![p]\!])$,
$[\![\exists L(p; u, v.\ g)]\!] = [\![g]\!] (1o\!f([\![p]\!]) / u, 2o\!f([\![p]\!] / v))$.

6.

$[\![\forall x\!:\!A.\ P[x]]\!] = fun(A; x.\ [\![P[x]]\!])$,
$[\![\forall R(x.\ e)]\!] = \lambda(x. [\![e]\!])$,
$[\![\forall L(f; a; y.\ e)]\!] = [\![g]\!][ap([\![f]\!]; a)/ y].$Curry-Howard isomorphism