直觀主義論理
intuitionistic logic。constructive logic
二重否定 (
否定の否定) の除去
\neg\neg A\to APeirce の法則((A\to B)\to A)\to A
意味論
完備 Heyting 代數 (complete Heyting algebra; cHa)
二重否定 (
否定の否定) の導入
x\to\neg\neg xに對應する
得た知識は失はれない
BHK 解釋 (Brouwer-Heyting-Kolmogorov 解釋)
Kripke-Joyal 意味論
公理
sequent の右邊は高々一個の formula でなければならない
始式 :\frac{}{A\vdash A}(I)
弱化 (增 W) (weakening) :
\frac{\Gamma\vdash\Delta}{D,\Gamma\vdash\Delta}(WL),
\frac{\Gamma\vdash\quad}{\Gamma\vdash D}(WR) 轉置 (換 P) (permutation) :
\frac{\Gamma,C,D,\Pi\vdash\Delta}{\Gamma,D,C,\Pi\vdash\Delta}(PL), PR は無い
縮約 (減 C) (contraction) :
\frac{D,D,\Gamma\vdash\Delta}{D,\Gamma\vdash,\Delta}(CL), CR は無い
Cut :\frac{\Gamma\vdash D\quad D,\Pi\vdash\Lambda}{\Gamma,\Pi\vdash\Lambda}(Cut)
\neg:\frac{\Gamma\vdash D}{\neg D,\Gamma\vdash\quad}(\neg L),\frac{D,\Gamma\vdash\quad}{\Gamma\vdash\neg D}(\neg R)
\land:\frac{C,\Gamma\vdash\Delta}{C\land D,\Gamma\vdash\Delta}(\land L_1),\frac{D,\Gamma\vdash\Delta}{C\land D,\Gamma\vdash\Delta}(\land L_2),\frac{\Gamma\vdash C\quad\Gamma\vdash D}{\Gamma\vdash C\land D}(\land R)
\lor:\frac{C,\Gamma\vdash\Delta\quad D,\Gamma\vdash\Delta}{C\lor D,\Gamma\vdash\Delta}(\lor L),\frac{\Gamma\vdash\Delta,C}{\Gamma\vdash\Delta,C\lor D}(\lor R_1),\frac{\Gamma\vdash\Delta,D}{\Gamma\vdash\Delta,C\lor D}(\lor R_2)
\to:\frac{\Gamma\vdash C\quad D,\Pi\vdash\Lambda}{C\to D,\Gamma,\Pi\vdash\Lambda}(\to L),\frac{C,\Gamma\vdash D}{\Gamma\vdash C\to D}(\to R)
\forall:\frac{F\lbrack t/x\rbrack,\Gamma\vdash\Delta}{\forall xF,\Gamma\vdash\Delta}(\forall L),\frac{\Gamma\vdash F\lbrack a/x\rbrack}{\Gamma\vdash\forall xF}(\forall R)
\exist:\frac{F\lbrack a/x\rbrack,\Gamma\vdash\Delta}{\exist xF,\Gamma\vdash\Delta}(\exist L),\frac{\Gamma\vdash F\lbrack t/x\rbrack}{\Gamma\vdash\exist xF}(\exist R)
最小論理 (minimal logic)
中閒論理 (intermediate logic。超直觀主義論理 (superintuitionistic logic))
Gödel-Dummett 論理
(A\to B)\lor(B\to A).