前の記事：一階述語論理の証明列を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$ を導けます。
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の検査器は、証明列の正しさを確認する小さなモデルである
- 健全性・完全性・自動探索は、検査器とは別の課題である
次の記事では、構造と変数割当によって論理式へ意味を与え、証明論との関係を整理します。