前の記事：一階述語論理の論理公理とΣ-公理系を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 は証明列の検査器であり、演繹定理を自動的に適用する機能は持ちません。仮定の依存関係や、含意の導入による証明変換を扱うには、別のデータ構造と推論規則が必要です。

まとめ

この記事では、根拠付きの論理式の列として証明を表現し、次の内容を検査しました。

論理公理と理論公理を区別する
証明行に根拠と参照先を持たせる
モーダスポネンスの適用条件を検査する
証明列の最後が指定した結論になっていることを確認する

この検査器を使って定理を扱うには、論理公理スキーマの具体化と、仮定を含む証明の表現が必要になります。

次の記事では、モーダスポネンスによる導出、矛盾からの導出、背理法との関係を確認します。

次の記事：一階述語論理の定理をPythonで追う：モーダスポネンスと背理法