証明可能性
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/03/25 04:10 UTC 版)
論理式 φ が論理式の集合 Σ から証明可能であるとは、Σ に属する論理式と論理公理から推論規則の有限回の適用によって φ が得られることを意味する。そして、Σ に属する論理式と論理公理から φ を導出する仮定を示した論理式の有限列を、Σ からの φ の形式的証明とよぶ。これらの概念は次のように厳密に定義することができる。 φ を論理式、Σ を論理式の集合とする。Σ からの φ の形式的証明 (formal proof) あるいは証明 (proof) とは、論理式の有限列 (φ0, ..., φn) で次をみたすものをいう：φn = φ 。 n 以下の任意の自然数 k に対して、次のいずれかが成り立つ： (a) φk ∈ Σ 。 (b) φk は論理公理である。 (c) ある i, j < k が存在して、φk は φi , φj からのモーダス・ポーネンスによる導出である。 (d) ある i < k が存在して、φk は φi からの全称化による導出である。 Σ からの φ の証明が存在するとき、φ は Σ から証明可能 (provable) である、あるいは φ は Σ の定理 (theorem) であるといい、 Σ ⊢ φ {\displaystyle \Sigma \vdash \varphi } と書く。
※この「証明可能性」の解説は、「一階述語論理」の解説の一部です。
「証明可能性」を含む「一階述語論理」の記事については、「一階述語論理」の概要を参照ください。
ウィキペディア小見出し辞書の「証明可能性」の項目はプログラムで機械的に意味や本文を生成しているため、不適切な項目が含まれていることもあります。ご了承くださいませ。
お問い合わせ。
- 証明可能性のページへのリンク
