second-order predicate logic

ウィキペディア

二階述語論理

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2023/10/10 09:13 UTC 版)

二階述語論理（にかいじゅつごろんり、英: second-order predicate logic）あるいは単に二階論理（にかいろんり、英: second-order logic）は、一階述語論理を拡張した論理体系であり、一階述語論理自体も命題論理を拡張したものである^[1]。二階述語論理もさらに高階述語論理や型理論に拡張される。

一階述語論理と同様に議論領域（ドメイン）の考え方を使う。ドメインとは、量化可能な個々の元の集合である。一階述語論理では、そのドメインの個々の元が変項の値となり、量化される。例えば、一階の論理式 ∀x (x ≠ x + 1) では、変項 x は任意の個体を表す。二階述語論理は個体の集合を変項の値とし、量化することができる。例えば、二階の論理式 ∀S ∀x (x ∈ S ∨ x ∉ S) は、個体の全ての集合 S と全ての個体 x について、x が S に属するか、あるいは属さないかのどちらかであるということを主張している。最も一般化された二階述語論理は関数の量化をする変項も含んでいる（詳しくは後述）。

二階論理の表現能力

二階述語論理は一階述語論理よりも表現能力が高い。例えば、ドメインが全ての実数の集合としたとき、一階述語論理を使って「それぞれの実数には加法の逆元が存在する」ということを ∀x ∃y (x + y = 0) と表せる。しかし、「空でなく上に有界な実数の集合があるとき常にその集合には上限が存在する」という命題を表すには、二階述語論理が必要となる。ドメインが全ての実数の集合としたとき、次の二階の論理式がこの命題を表している。

${\displaystyle \forall A{\Big [}(\exists w(w\in A)\land \exists z\,\forall w(w\in A\rightarrow w\leq z))\rightarrow \exists x\,\forall y([\forall w(w\in A\rightarrow w\leq y)]\leftrightarrow x\leq y){\Big ]}.}$カテゴリ

表 話 編 歴 数理論理学
一般	形式言語 構成規則 形式体系 演繹システム（英語版） 形式的証明 形式意味論 論理式 集合 元 クラス 古典論理 公理 自然演繹 推論規則 関係 定理 論理的帰結 公理系 型理論 記号（英語版） 統語論（英語版） 理論（英語版）
Traditional logic（英語版）	命題 推論 論証 妥当性 Cogency 三段論法 Square of opposition（英語版） ベン図
命題論理・ ブール論理	ブール関数 命題論理 命題論理式（英語版） 論理演算 真理値表 多値論理
述語論理	一階 量化子 述語（英語版） 二階 Monadic predicate calculus（英語版）
素朴集合論	集合 空集合 元 数え上げ 外延 有限集合 無限集合 部分集合 冪集合 可算集合 非可算集合 帰納的集合 定義域 終域 像 写像 関数 関係 順序対
集合論	数学基礎論 ツェルメロ＝フレンケル集合論 選択公理 一般集合論（英語版） Kripke–Platek 集合論（英語版） フォン・ノイマン＝ベルナイス＝ゲーデル集合論（英語版） モース-ケリー集合論 タルスキ＝グロタンディーク集合論（英語版）
モデル理論	モデル（英語版） 解釈（英語版） 超準モデル（英語版） 有限モデル理論 真理値 妥当性
証明論	形式的証明 演繹システム（英語版） 形式体系 定理 論理的帰結 推論規則 統語論（英語版） シークエント計算
計算理論 再帰理論	計算可能性 計算複雑性 複雑性クラス P≠NP予想 再帰 帰納的集合 帰納的可算集合 決定問題 停止性問題 チャーチ＝チューリングのテーゼ 計算可能関数 原始再帰関数 μ再帰関数 チューリングマシン ラムダ計算