直觀主義論理
intuitionistic logic。constructive logic
二重否定 (否定の否定) の除去$ \neg\neg A\to A Peirce の法則$ ((A\to B)\to A)\to A
意味論
二重否定 (否定の否定) の導入$ 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}({\rm 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).