直観主義論理との関係
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2016/09/24 08:57 UTC 版)
「B,C,K,Wシステム」の記事における「直観主義論理との関係」の解説
定数記号 B, C, K, W はそれぞれよく知られた4つの命題論理の公理と対応する： AB: (B → C) → ((A → B) → (A → C)), AC: (A → (B → C)) → (B → (A → C)), AK: A → (B → A), AW: (A → (A → B)) → (A → B). MP: A → B , A ⊢ B {\displaystyle A\to B,A\vdash B} 公理 AB, AC, AK, AW 及び推論規則 MP は、直観主義命題論理の含意断片（英語版）に対して完全である。この体系に爆発原理 F → A と排中律に類する規則（例：パースの法則）を加えたものは古典命題論理と対応する。コンビネータ W とそれに関する公理図式を取り除いたものはBCK論理と対応する。これはBCK-λ計算と対応するものである。
※この「直観主義論理との関係」の解説は、「B,C,K,Wシステム」の解説の一部です。
「直観主義論理との関係」を含む「B,C,K,Wシステム」の記事については、「B,C,K,Wシステム」の概要を参照ください。
直観主義論理との関係
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/06/17 15:40 UTC 版)
「SKIコンビネータ計算」の記事における「直観主義論理との関係」の解説
コンビネータ K および S は、よく知られた次の命題論理の公理図式と対応する： AK: A → {\displaystyle \to } (B → {\displaystyle \to } A),AS: (A → {\displaystyle \to } (B → {\displaystyle \to } C)) → {\displaystyle \to } ((A → {\displaystyle \to } B) → {\displaystyle \to } (A → {\displaystyle \to } C)). 関数適用は推論規則モーダスポネンスと対応する： MP: A → B , A ⊢ B {\displaystyle A\to B,A\vdash B} 公理 AK, AS 及び推論規則 MP は、直観主義命題論理の含意断片に対して健全かつ完全である。この体系に爆発原理 F → A と排中律に類する規則（例：パースの法則）を追加したものは古典命題論理と対応する。
※この「直観主義論理との関係」の解説は、「SKIコンビネータ計算」の解説の一部です。
「直観主義論理との関係」を含む「SKIコンビネータ計算」の記事については、「SKIコンビネータ計算」の概要を参照ください。
- 直観主義論理との関係のページへのリンク
