自然演繹
Γ ⊢ π1 : A かつ Γ, u:A ⊢ π2 : B なら、 Γ ⊢ [π1/u] π2 : B である。
これまで、判断 "Γ ⊢ π : A" は、純粋に論理的な意味しかなかった。型理論では、論理的な観点からより計算的な観点へと変換が行われる。論理的には命題とされていたものが「型」となり、証明はラムダ計算におけるプログラムとなる。従って、"π : A" は、「プログラム π の型は A である」という解釈になる。論理結合子も異なった解釈となる。論理積は積(×)、含意は関数矢印(→)などとなる。ただし、これらの違いは単に表面的なものである。型理論では、構成規則、導入規則、除去規則を自然演繹的に表現する。実際、自然演繹を知っていれば、単純階型理論は容易に理解できる。
論理と型理論の違いは、焦点が型(命題)からプログラム(証明)に移っている点である。型理論は、プログラムの変換可能性や還元可能性に興味の中心がある。全ての型について、還元不可能な正規のプログラムが存在する。これを「正規形」または「値」と呼ぶ。全てのプログラムが正規形に還元可能なら、その型理論は「正規化; normalising」(あるいは弱正規化)されていると言える。正規形が唯一である場合、その理論は「強正規化; strongly normalising」されていると言える。
演繹(または証明)は、命題論理のような形式体系の文脈では正確に定義できる。命題 α は、前提の集合 Σ に推論規則を繰り返し適用することで演繹される。演繹は、この推論規則の繰り返し適用の記録である。
より形式的には、命題の有限な列 β1 ,..., βn が、前提の集合 Σ からの α の演繹であるとは、次が成り立つ場合である。
βn = α であり、かつ 全ての 1 ≤ i ≤ n について、βi が前提であるか(すなわち、βi ∈ Σ)または βi がそれ以前に出現した命題に何らかの推論規則を適用した結果である。
公理的命題論理のバージョンによって採用する公理や推論規則が異なる。例えば、フレーゲは、6つの公理と2つの規則を採用した。バートランド・ラッセルとアルフレッド・ノース・ホワイトヘッドは、5つの公理からなる体系を示唆した。
ヤン・ウカシェヴィチによる公理的命題論理のバージョンでは、次のような公理群 A を採用した。
[PL1] p → (q → p) [PL2] (p → (q → r)) → ((p → q) → (p → r)) [PL3] (¬p → ¬q) → (q → p)
そして、推論規則 R としては、モーダスポネンスを採用した。
[MP] α と α → β から、β を推論する。
推論規則により、Σ に含まれる論理式と公理群から新たな論理式を導出できる。