直觉主义逻辑

直觉主义逻辑构造性逻辑是最初由 阿蘭德·海廷开发的为 鲁伊兹·布劳威尔数学直觉主义计划提供形式基础的 符号逻辑。这个系统保持跨越生成导出命题的变换的 证实性而不是 真理性。从实用的观点,也有使用直觉逻辑的强烈动机,因为它有 存在性质,这使它还适合其他形式的 数学构造主义

语法

Rieger-Nishimura 格。它的節點是不別直覺邏輯等價之異的一元命題公式,按直覺邏輯蘊含排序。

直觉逻辑的公式的 语法类似于 命题逻辑一阶逻辑。但是直覺邏輯的連結詞不像 經典邏輯那樣是可互定義的,因此它們的選擇是重要的。在直覺命題邏輯中通常使用 →, ∧, ∨, ⊥ 作為基本連結詞,把 ¬ 作為 ¬A = (A → ⊥) 的簡寫處理。在直覺一階邏輯中量詞 ∃, ∀ 都是需要的。

不同在于很多经典逻辑的 重言式在直觉逻辑中不再是可证明的。例子不只包括 排中律 P ∨ ¬P,还有 皮尔士定律 ((PQ) → P) → P,甚至还有 双重否定除去。在经典逻辑中,P → ¬¬P 和 ¬¬PP 二者都是定理。在直觉逻辑中,只有前者是定理: 双重否定可以介入但不能除去。

对很多经典有效重言式不是直觉逻辑的定理的观察导致了弱化经典逻辑的证明论的想法。

相继式演算

根岑发现简单限制他的系统LK(他的经典逻辑的相继式演算)就导致了关于直觉逻辑的一个可靠和完备的系统。他称之为系统LJ。

希尔伯特式演算

推理规则是 肯定前件,公理有:

  • THEN-1: φ → (χ → φ)
  • THEN-2: (φ → (χ → ψ)) → ((φ → χ) → (φ → ψ))
  • AND-1: φ ∧ χ → φ
  • AND-2: φ ∧ χ → χ
  • AND-3: φ → (χ → (φ ∧ χ))
  • OR-1: φ → φ ∨ χ
  • OR-2: χ → φ ∨ χ
  • OR-3: (φ → ψ) → ((χ → ψ) → (φ ∨ χ → ψ))
  • NOT-1: (φ → χ) → ((φ → ¬χ) → ¬ φ)
  • NOT-2: φ → (¬φ → χ)

对于一阶逻辑系统还要加上 普遍化规则,和如下公理:

  • PRED-1: (∀x Z(x)) → Z(t)
  • PRED-2: Z(t) → (∃x Z(x))
  • PRED-3: (∀x (WZ(x))) → (W → ∀x Z(x))
  • PRED-4: (∀x (Z(x) → W)) → (∃x Z(x) → W)

算子的不可互定义性

在经典命题逻辑中,有可能选取 合取析取蕴涵中的一个作为原始的,并依据它和 否定来定义另两个,比如在 扬·武卡谢维奇命题逻辑三公理中。甚至可以依据 自足算子比如 皮尔士箭头(NOR)或 Sheffer竖线(NAND)定义它们四个。类似的,在经典一阶逻辑中,一个量词可以依据另一个量词和否定来定义。

这是 二值原理的推论,它使得这种连结词仅仅是 布尔函数。二值原理在直觉逻辑中不成立,只有 无矛盾律成立。作为结果没有连结词可以豁免,而上述公理都是必须的。多数经典恒等式只是直觉逻辑中在一个方向上的定理,尽管某些定理是两个方向的。它们如下:

合取与析取:

合取与蕴涵:

析取与蕴涵:

全称量词与存在量词:

所以,例如 “a 或 b”是比“如果非 a 则 b”更强的陈述,而在经典逻辑中它们是可互换的。

據 Alexander Kuznetsov 的證明,任一下述定義的連結詞可以充當直覺邏輯的自足算子: [1]

其他语言