Sự tương ứng Curry–Howard

(Chứng minh trở thành chương trình.) Bằng quy nạp theo dẫn xuất suy luận tự nhiên của $\vdash \varphi$. Nếu quy tắc cuối là dẫn nhập $\to$, dẫn $\varphi=\psi\to\chi$ từ một chứng minh con của $\chi$ dưới giả thiết $\psi$: theo giả thiết quy nạp chứng minh con đó dịch thành hạng $t$ với $x{:}A_\psi \vdash t : A_\chi$ (giả thiết trở thành biến tự do $x$); khi đó $\lambda x{:}A_\psi.\,t$ đóng và có kiểu $A_\psi\to A_\chi=A_\varphi$. Nếu quy tắc cuối là loại bỏ $\to$ (modus ponens) từ $\psi\to\chi$ và $\psi$: theo giả thiết quy nạp ta có các hạng $t_1 : A_\psi\to A_\chi$ và $t_2 : A_\psi$; khi đó $t_1\,t_2 : A_\chi$. Các quy tắc dẫn nhập $\wedge$ và loại bỏ $\wedge$ dịch đối xứng thành ghép cặp $\langle t_1,t_2\rangle$ và hai phép chiếu. Mọi quy tắc của hệ chứng minh đều có quy tắc xây hạng tương ứng, nên quy nạp theo dẫn xuất cho ra một hạng đóng được định kiểu thuộc kiểu $A_\varphi$.

(Chương trình trở thành chứng minh.) Ngược lại, bằng quy nạp theo dẫn xuất kiểu $\vdash t : A$. Mỗi quy tắc kiểu — biến, trừu tượng hóa, áp dụng, ghép cặp, phép chiếu — có đúng hình dạng cây như một quy tắc suy luận tự nhiên — giả thiết, dẫn nhập $\to$, loại bỏ $\to$, dẫn nhập $\wedge$, loại bỏ $\wedge$. Vậy lấy cùng cây dẫn xuất, xóa mọi hạng, và đọc mỗi kiểu như công thức nó dịch từ: đây chính xác là một chứng minh trực giác hợp lệ của $\varphi$ (với $A=A_\varphi$).

Vì hai phép dịch (chứng minh $\to$ hạng, và hạng $\to$ chứng minh) là nghịch đảo cấu trúc của nhau trên các cây dẫn xuất — mỗi phép hoàn tác chính xác điều phép kia làm, quy tắc theo quy tắc — $\varphi$ chứng minh được đúng khi $A_\varphi$ có cư dân. $\blacksquare$