前の記事：一階述語論理の論理公理とΣ-公理系をPythonで表す
論理式を構文木として表現し、論理公理と理論公理を用意しても、証明列が正しいとは限りません。
形式的な証明では、各行がどの公理に由来するのか、どの推論規則を適用したのかを明示します。この記事では、前の記事で定義した Formula を使い、証明列を検査する小さなプログラムを実装します。
ここで実装するのは、証明を自動的に探索する証明支援系ではありません。指定された証明列が、指定された公理集合とモーダスポネンスに従っているかを検査するモデルです。
証明列と根拠
証明は、論理式を並べた有限列です。各行について、次のいずれかを説明できなければなりません。
- 論理公理の具体例である
- 理論の公理集合 $\Sigma$ の要素である
- それ以前の行から推論規則で導かれる
推論規則の適用元を記録しておけば、証明列を人間が確認する場合にも、プログラムで検査する場合にも根拠をたどれます。
証明行を表現する
proof.py
from __future__ import annotations
from abc import ABC, abstractmethod
from dataclasses import dataclass
from axiom_system import AxiomSystem
from formulas import Formula, Implication
class InvalidProof(ValueError):
pass
class Justification(ABC):
@abstractmethod
def validate(
self,
*,
index: int,
formula: Formula,
system: AxiomSystem,
proved: list[Formula],
) -> str:
"""この根拠が証明列の現在位置で正しいことを検査する。"""
@dataclass(frozen=True, slots=True)
class LogicalAxiom(Justification):
def validate(
self,
*,
index: int,
formula: Formula,
system: AxiomSystem,
proved: list[Formula],
) -> str:
if formula not in system.logical_axioms:
raise InvalidProof(f"line {index}: not a logical axiom instance")
return "logical axiom"
@dataclass(frozen=True, slots=True)
class TheoryAxiom(Justification):
def validate(
self,
*,
index: int,
formula: Formula,
system: AxiomSystem,
proved: list[Formula],
) -> str:
if formula not in system.theory_axioms:
raise InvalidProof(f"line {index}: not an element of Sigma")
return "theory axiom"
@dataclass(frozen=True, slots=True)
class ModusPonens(Justification):
implication_index: int
premise_index: int
def validate(
self,
*,
index: int,
formula: Formula,
system: AxiomSystem,
proved: list[Formula],
) -> str:
if not 0 <= self.implication_index < index:
raise InvalidProof(f"line {index}: invalid implication reference")
if not 0 <= self.premise_index < index:
raise InvalidProof(f"line {index}: invalid premise reference")
implication = proved[self.implication_index]
premise = proved[self.premise_index]
if not isinstance(implication, Implication):
raise InvalidProof(f"line {index}: first formula is not an implication")
if implication.left != premise or implication.right != formula:
raise InvalidProof(f"line {index}: modus ponens does not apply")
return (
"modus ponens from lines "
f"{self.implication_index} and {self.premise_index}"
)
@dataclass(frozen=True, slots=True)
class ProofLine:
formula: Formula
justification: Justification
LogicalAxiom と TheoryAxiom は、それぞれ論理公理・理論公理であることを検査します。ModusPonens は参照する2行の番号を持ち、その参照がモーダスポネンスの形になっていることを検査します。
モーダスポネンスを検査する
ここでは、次のモーダスポネンスだけを推論規則として実装します。
\frac{\alpha \qquad \alpha \to \beta}{\beta}
つまり、$\alpha$ と $\alpha \to \beta$ がすでに証明列に現れていれば、$\beta$ を導けます。
proof_checker.py
from __future__ import annotations
from collections.abc import Callable
from axiom_system import AxiomSystem
from formulas import Formula
from predicates import is_sentence
from proof import InvalidProof, ProofLine
class ProofChecker:
def __init__(
self,
system: AxiomSystem,
trace: Callable[[str], None] | None = None,
) -> None:
self._system = system
self._trace_callback = trace
def check(self, lines: list[ProofLine], conclusion: Formula) -> None:
proved: list[Formula] = []
for index, line in enumerate(lines):
if not is_sentence(line.formula):
raise InvalidProof(f"line {index}: proof lines must be sentences")
message = line.justification.validate(
index=index,
formula=line.formula,
system=self._system,
proved=proved,
)
self._trace(f"line {index}: {message}")
proved.append(line.formula)
if not proved or proved[-1] != conclusion:
raise InvalidProof("the proof does not establish the conclusion")
self._trace(f"conclusion: {conclusion}")
def _trace(self, message: str) -> None:
if self._trace_callback is not None:
self._trace_callback(message)
証明列を前から順番に処理しているため、未来の行や存在しない行を参照する証明は拒否されます。
証明列を検査する
次の例では、$\Sigma$ に含まれる0引数述語 $P$ と $P \to Q$ から $Q$ を導きます。$\forall x\,(x = x)$ は論理公理の具体例ですが、この例のモーダスポネンスには使いません。
- $\forall x\,(x = x)$（論理公理）
- $P$（$\Sigma$ の元）
- $P \to Q$（$\Sigma$ の元）
- $Q$（2と3からモーダスポネンス）
example_proof.py
from axiom_system import AxiomSystem
from proof import InvalidProof, LogicalAxiom, ModusPonens, ProofLine, TheoryAxiom
from proof_checker import ProofChecker
from formulas import Equality, Forall, Implication, PredicateApplication
from terms import Variable
x = Variable("x")
p = PredicateApplication("P", ())
q = PredicateApplication("Q", ())
p_implies_q = Implication(p, q)
reflexive = Forall(x, Equality(x, x))
lines = [
ProofLine(reflexive, LogicalAxiom()),
ProofLine(p, TheoryAxiom()),
ProofLine(p_implies_q, TheoryAxiom()),
ProofLine(q, ModusPonens(implication_index=2, premise_index=1)),
]
system = AxiomSystem(
logical_axioms=frozenset({reflexive}),
theory_axioms=frozenset({p, p_implies_q}),
)
checker = ProofChecker(system, trace=print)
try:
checker.check(lines, conclusion=q)
except InvalidProof as error:
print(f"証明列が不正です: {error}")
else:
print("証明列は正しいです。")
line 0: logical axiom
line 1: theory axiom
line 2: theory axiom
line 3: modus ponens from lines 2 and 1
conclusion: Q()
証明列は正しいです。
モーダスポネンスの参照順を逆にすると、最初の参照が含意ではなくなるため、検査器は次のように拒否します。
invalid_lines = [
*lines[:3],
ProofLine(q, ModusPonens(implication_index=1, premise_index=2)),
]
try:
checker.check(invalid_lines, conclusion=q)
except InvalidProof as error:
print(f"証明列が不正です: {error}")
else:
print("証明列は正しいです。")
line 0: logical axiom
line 1: theory axiom
line 2: theory axiom
証明列が不正です: line 3: first formula is not an implication
この検査器は、証明列の各行が正しいかを確認します。ただし、証明列を自動生成したり、論理公理スキーマを自動的に展開したりはしません。
演繹定理との関係
適切な形式体系では、演繹定理によって次の関係が成り立ちます。
\Sigma \cup \{\alpha\} \vdash \beta
\quad\Longleftrightarrow\quad
\Sigma \vdash \alpha \to \beta
今回の ProofChecker は証明列の検査器であり、演繹定理を自動的に適用する機能は持ちません。仮定の依存関係や、含意の導入による証明変換を扱うには、別のデータ構造と推論規則が必要です。
まとめ
この記事では、根拠付きの論理式の列として証明を表現し、次の内容を検査しました。
- 論理公理と理論公理を区別する
- 証明行に根拠と参照先を持たせる
- モーダスポネンスの適用条件を検査する
- 証明列の最後が指定した結論になっていることを確認する
この検査器を使って定理を扱うには、論理公理スキーマの具体化と、仮定を含む証明の表現が必要になります。
次の記事では、モーダスポネンスによる導出、矛盾からの導出、背理法との関係を確認します。