前の記事：一階述語論理の代入をPythonで実装する：全称閉包と変数捕獲を避ける置換
一階述語論理では、論理式を並べるだけでは証明になりません。どの式を公理として認め、どの推論規則を使うかを先に定める必要があります。
この記事では、前の記事で実装した構文木と代入処理を使い、論理公理、理論の公理集合 $\Sigma$、$\Sigma$-公理系の関係を整理します。
ここでは、命題論理のトートロジーを真理値表で定める古典一階述語論理を採用します。
論理公理と理論公理
論理公理は、特定の数学理論に依存せず、一階述語論理の推論で共通して使う公理です。
一方、$\Sigma$ は集合論や算術など、対象とする理論に固有の公理からなる集合です。論理公理と $\Sigma$ の元を合わせたものを $\Sigma$-公理系と呼びます。
\Sigma\text{-公理系}
=
\text{論理公理}
\cup
\Sigma
論理公理と理論公理は、どちらも証明列の出発点になりますが、役割が異なります。論理公理は推論の枠組みを定め、$\Sigma$ の元はその理論で何を仮定するかを定めます。
論理公理のスキーマ
論理公理は、個別の論理式を列挙するのではなく、論理式を変数として表したスキーマで定めます。各スキーマと、その全称閉包として表される命題を論理公理として扱います。$\Sigma$ は命題の集合であり、証明列も命題の列です。
論理式 $\alpha$、$\beta$、変数 $x, y, z, x_0, x_1, y_0, y_1$、項 $t$ を使うと、代表的なスキーマは次のようになります。
- 命題論理のトートロジー
- $x$ が $\alpha$ に自由に現れないときの $\alpha \to \forall x\,\alpha$
- $\forall x\,(\alpha \to \beta) \to (\forall x\,\alpha \to \forall x\,\beta)$
- $\forall x\,\alpha \to \alpha(x \mapsto t)$
- $\alpha(x \mapsto t) \to \exists x\,\alpha$
- $\forall x\,\neg\alpha \to \neg\exists x\,\alpha$
- $x = x$
- $(x = y) \leftrightarrow (y = x)$
- $((x = y) \land (y = z)) \to (x = z)$
- $((x_0 = y_0) \land (x_1 = y_1)) \to (x_0 \in x_1 \leftrightarrow y_0 \in y_1)$
4と5の $\alpha(x \mapsto t)$ は、自由な $x$ だけを $t$ へ置換した式です。置換項による変数捕獲を避ける必要があるため、スキーマの具体化には代入と $\alpha$ 変換を使います。
10は、等しい対象を所属関係 $\in$ へ代入できることを表す、集合論の言語に固有のスキーマです。任意の関数記号や述語記号を持つ一般の言語で等号を扱うには、それぞれに対応する合同性のスキーマが必要です。この記事の Equality は構文として表現するだけであり、一般の等号付き一階述語論理を完全に公理化するものではありません。
全称閉包と公理インスタンス
スキーマに現れる変数を全称量化して得られる文を全称閉包と呼びます。
\alpha(x_0, \ldots, x_n)
\quad\longmapsto\quad
\forall x_0\cdots\forall x_n\,\alpha
例えば、$x = x$ は変数 $x$ を含むスキーマですが、その全称閉包は次の命題です。
\forall x\,(x = x)
証明列で扱うのはスキーマそのものではなく、具体的な代入と全称閉包によって得られた公理インスタンスです。
Pythonで公理系を表す
from dataclasses import dataclass
from formulas import Formula
from predicates import is_sentence
@dataclass(frozen=True, slots=True)
class AxiomSystem:
logical_axioms: frozenset[Formula]
theory_axioms: frozenset[Formula]
def __post_init__(self) -> None:
axioms = self.logical_axioms | self.theory_axioms
if any(not is_sentence(formula) for formula in axioms):
raise ValueError("axioms must be sentences")
論理公理スキーマは無限個の具体例を持ちます。このデータ構造はスキーマ全体を生成するものではなく、具体化と全称閉包を済ませた有限個の公理インスタンスだけを保持します。__post_init__() では、それらが文であることを確認します。
from axiom_system import AxiomSystem
from formulas import Equality, Forall, PredicateApplication
from terms import Variable
x = Variable("x")
reflexive = Forall(x, Equality(x, x))
p = PredicateApplication("P", ())
system = AxiomSystem(
logical_axioms=frozenset({reflexive}),
theory_axioms=frozenset({p}),
)
この例では、$\forall x\,(x = x)$ を論理公理の具体例、0引数述語 $P$ を理論 $\Sigma$ の公理として登録しています。どちらも自由変数を持たない文です。実際のスキーマ生成では、代入可能性の確認、変数捕獲を避ける $\alpha$ 変換、全称閉包の生成を組み合わせます。
証明との関係
$\Sigma$-公理系から推論規則を有限回適用して得られた論理式を、$\Sigma$-公理系における定理と呼びます。
\Sigma \vdash \varphi
は、$\Sigma$-公理系から $\varphi$ の形式的な証明が存在することを表します。証明列の各行が公理系に属するか、以前の行から推論できるかを検査する処理は、次の記事で実装します。
まとめ
- 論理公理は理論によらず共通する推論の基盤である
- $\Sigma$ は対象とする理論に固有の公理集合である
- $\Sigma$-公理系は論理公理と $\Sigma$ の元からなる
- 公理スキーマは代入と全称閉包によって具体的な公理インスタンスになる
- 具体的な公理インスタンスと推論規則から証明列を構成する
次の記事では、各行の根拠を記録した証明列をPythonで検査します。