自然演繹
もう1つの重要な拡張は様相論理学などの論理に関するもので、それらは単なる基本的な真理値の判断以上のことをする必要がある。1965年に Dag Prawitz が様相論理のための自然演繹的記法を述べており、その後も様々な研究が行われてきた。簡単な例を示すため、必要性の様相論理での新たな判断 "A valid" を考える。これは次のような意味である。
「もし "B true" という形式の前提無しで "A true" ならば、"A valid" である」
この断定的判断は単項結合子 ◻A("necessarily A")として表され、以下のような導入規則と除去規則となる。
なお、前提 "A valid" には定義規則がないが、その代わりに妥当性の断定的定義が使われる。この様相は、局所化された形式で仮説を明示的に示すとより明確になる。"Ω;Γ ⊢ A true" と記したとき、Γ は以前のように真なる仮説群を表し、Ω は妥当な仮説群を表す。右辺には単純な判断 "A true" しかない。"Ω ⊢ A valid" は定義から "Ω;⋅ ⊢ A true" と同じ意味であるため、妥当性はここでは不要である。導入規則と除去規則は次の通りである。
様相仮説には独自の仮説規則と代入定理がある。
D 1 D 2 ⋯ D n ⋮ J {\displaystyle {\begin{matrix}D_{1}\quad D_{2}\cdots D_{n}\\\vdots \\J\end{matrix}}}
仮説的導出には、先頭行に書かれた前件群(Di、antecedent derivations)と最終行に書かれた1つの後件判断(J、succedent judgement)がある。それぞれの前提が仮説的導出の結果となっている場合もある。以下、判断(judgement)は前提のない導出として扱う。
仮説的判断の考え方は、含意の結合子に利用される。含意の導入規則と除去規則は次のようになる。
A t r u e u ⋮ B t r u e A ⊃ B t r u e ⊃ I u A ⊃ B t r u e A t r u e B t r u e ⊃ E {\displaystyle {\cfrac {\begin{matrix}{\cfrac {}{A\ true}}u\\\vdots \\B\ true\end{matrix}}{A\supset B\ true}}\supset I^{u}\qquad {\cfrac {A\supset B\ true\quad A\ true}{B\ true}}\supset E}
導入規則では、前件 u は結論には現れない。これは仮説の「範囲」を限定する機構であり、その存在理由は "B true" を確立することにある。それ以外の目的で使うことはできず、特に導入後に使うことはできない。例として、"A ⊃ (B ⊃ (A ∧ B)) true" の導出を示す。
判断とは、何らかの認識可能なこと、すなわち知識の対象である。誰かが実際に何かを知っていれば、その何かは自明である。従って、「雨が降っている」は判断であり、実際に雨が降っていることを知っている人にとって、その言葉は自明である。この場合、その言葉を聞いた人が窓の外を見たり、外に出てみれば、自明となる「証拠」が簡単に得られる。しかし数理論理学では、証拠は直接観測不可能なことが多く、むしろより基本的な自明な判断から導き出される(演繹される)。演繹の過程は証明を構成する。言い換えれば、判断はその証明を知る人にとっては自明となる。
論理における最も重要な判断は「A は真である」という形式となる。この A は任意の「命題」を表す式で置換される。真かどうかの判断には、より基本的な判断「A は命題である」が必須となる。他にも様々な判断が研究されている。例えば、「A は偽である」(論理学)、「A は時刻 t では真である」(時相論理)、「A は真でなければならない」あるいは「A は真でありうる」(様相論理学)、「プログラム M の型は τ である」(プログラミング言語と型理論)、「A は利用可能な資源から達成できる」(線型論理)などである。以下では、「A は命題である」を "A prop"、「A は真である」を "A true" と表す。
判断 "A prop" は、A の妥当な証明の構造を定義し、そこから命題の構造が定義される。このため、このような判断に対する推論規則を「構成規則; formation rules」とも呼ぶ。