前の記事：一階述語論理の証明列をPythonで検査する：公理と推論規則の実装

論理公理と理論公理を用意すると、論理式を「証明できる式」として扱えるようになります。

この記事では、前の記事で作った証明列検査器を使い、モーダスポネンスによる導出、矛盾からの導出、背理法との関係を確認します。目的は高性能な自動定理証明ではなく、証明が公理と推論規則の列として組み立てられることをPythonで追うことです。

この連載では、命題論理のトートロジーを公理として含む古典一階述語論理を扱います。

公理系から式を導く

$\Sigma \vdash \varphi$ は、理論の公理集合 $\Sigma$ と論理公理から、推論規則を使って $\varphi$ を導けることを表します。

最も基本的な推論規則がモーダスポネンスです。

\frac{\alpha \qquad \alpha \to \beta}{\beta}

例えば、0引数述語 $P$ と $P \to Q$ を公理として仮定すれば、$Q$ を導けます。

$P$（$\Sigma$ の元）
$P \to Q$（$\Sigma$ の元）
$Q$（1と2からモーダスポネンス）

この導出は、理論の公理から結論を得る最小の例です。

矛盾から別の式を導く

Pythonの構文木には、矛盾を明示的に表す論理定数 Falsum を追加しています。$\bot$ を偽として解釈すると、次の式は命題論理のトートロジーです。

\bot \to \varphi

$\bot$ と $\bot \to \varphi$ が得られていれば、モーダスポネンスによって $\varphi$ を導けます。

explosion.py

from formulas import Falsum, Implication, PredicateApplication
from axiom_system import AxiomSystem
from proof import LogicalAxiom, ModusPonens, ProofLine, TheoryAxiom
from proof_checker import ProofChecker


bottom = Falsum()
q = PredicateApplication("Q", ())
bottom_implies_q = Implication(bottom, q)

lines = [
    ProofLine(bottom, TheoryAxiom()),
    ProofLine(bottom_implies_q, LogicalAxiom()),
    ProofLine(q, ModusPonens(implication_index=1, premise_index=0)),
]

checker = ProofChecker(
    AxiomSystem(
        logical_axioms=frozenset({bottom_implies_q}),
        theory_axioms=frozenset({bottom}),
    )
)
checker.check(lines, conclusion=q)

ここで $\bot$ は、構文木に追加した論理定数 Falsum で表しています。これは古典論理だけでなく、直観主義論理でも認められる矛盾からの導出です。Pythonの例外を矛盾として扱うのではなく、矛盾を表す論理式として証明列に含めています。

背理法との関係

背理法は、証明したい式 $\alpha$ の否定を仮定した公理系が矛盾することから、$\alpha$ を導く方法です。形式的には、次の関係として説明できます。

\Sigma \cup \{\lnot\alpha\}\text{ が矛盾する}
\quad\Longrightarrow\quad
\Sigma \vdash \alpha

この背理法は、古典的なトートロジーを用います。この変換を一般に実行するには、仮定を含む証明、仮定を閉じる含意の導入、演繹定理などが必要です。現在の ProofChecker は、仮定の依存関係を持たない証明列の検査器なので、背理法を自動的に適用する機能までは実装していません。

「矛盾から任意の式を導けること」と「背理法で仮定を取り除けること」は別の処理です。前者は矛盾を前提にした推論規則、後者は仮定を含む証明を変換する仕組みです。

定理をコードで扱うときの境界

証明列検査器が確認できるのは、与えられた列が採用した公理系と推論規則に従っていることです。次のことまでは確認していません。

その公理系が意図した数学理論を表していること
公理系が健全であること
真であるすべての式を証明できること
証明を自動的に探索できること

健全性は、証明できる式が意味論上も真であることを表します。完全性は、意味論上真である式を証明できることを表します。これらは、個々の証明列を検査するプログラムとは別のメタ理論です。

まとめ

定理は、公理と推論規則から得られる論理式である
モーダスポネンスは、証明列を組み立てる基本的な推論規則である
矛盾から任意の式を導くことと、背理法で仮定を閉じることは異なる
Pythonの検査器は、証明列の正しさを確認する小さなモデルである
健全性・完全性・自動探索は、検査器とは別の課題である

次の記事では、構造と変数割当によって論理式へ意味を与え、証明論との関係を整理します。

次の記事：一階述語論理の意味論をPythonの構文木から考える：モデルと証明論の接続