証明

数理論理学における証明 (英: proof) とは文の有限列で、特定の性質を満たすものである。数学の通常の証明と区別が必要な場合、形式的証明 (英: formal proof) ということもある。

定義

文の有限列構文解析に失敗 (SVG（ブラウザのプラグインで MathML を有効にすることができます）: サーバー「https://ja.wikipedia.org/api/rest_v1/」から無効な応答 ("Math extension cannot connect to Restbase."):): {\displaystyle \phi_0,...\phi_n} と理論Tが以下の性質を満たすとき、この有限列をφ_nのTからの証明という。

• 任意の自然数構文解析に失敗 (SVG（ブラウザのプラグインで MathML を有効にすることができます）: サーバー「https://ja.wikipedia.org/api/rest_v1/」から無効な応答 ("Math extension cannot connect to Restbase."):): {\displaystyle 0 \leq i \leq n} について、
  • φ_iが論理公理である、もしくは
  • φ_iがTの元(公理)である、もしくは
  • 構文解析に失敗 (SVG（ブラウザのプラグインで MathML を有効にすることができます）: サーバー「https://ja.wikipedia.org/api/rest_v1/」から無効な応答 ("Math extension cannot connect to Restbase."):): {\displaystyle \phi_0,...\phi_{i-1}} に含まれる文に推論規則を適用してφ_iを導出できる。

文φの理論Tからの証明が存在するとき、φはTから証明可能 (英: provable) である、またはφはTの定理 (英: theory) であるといい、構文解析に失敗 (SVG（ブラウザのプラグインで MathML を有効にすることができます）: サーバー「https://ja.wikipedia.org/api/rest_v1/」から無効な応答 ("Math extension cannot connect to Restbase."):): {\displaystyle T \vdash \phi} と表す。