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

ここまでの記事では、論理式の構文木、自由変数への代入、論理公理、証明列を扱いました。ここで、証明論と対になる意味論の役割を整理します。

意味論は、論理式を構造の中で解釈し、真かどうかを定めます。一方、証明論は、論理公理と推論規則から論理式を導けるかを扱います。

この記事の目的は、Pythonで論理式を大量に評価することではありません。構文木に意味を与えるために何が必要かを確認し、$\Sigma \vdash \varphi$ と $\Sigma \models \varphi$ がどのように異なるかを整理することです。

構文だけでは真偽は決まらない

例えば、次の論理式は構文木として組み立てられます。

\forall x\,(P(x) \to \exists y\,R(x, y))

しかし、これが真かどうかは構文だけでは決まりません。少なくとも次の情報が必要です。

変数が値を取る対象領域
定数記号や関数記号の解釈
述語記号がどの要素に成り立つか
自由変数へ割り当てる値

対象領域と定数記号・関数記号・述語記号の解釈を合わせたものを構造と呼びます。自由変数を含む論理式を評価するときは、構造とは別に変数割当も与えます。構文木が論理式の形を表すのに対して、構造が記号の意味を与えます。

構造と変数割当

一階述語論理の構造 $M$ は、対象領域と各記号の解釈からなります。概念的には次のように表せます。

後で定義する Structure は、対象領域、定数記号、関数記号、述語記号の解釈を持つ最小のデータ構造です。記号の引数の個数や、関数の戻り値が対象領域に含まれることまでは検査しません。

変数割当 $s$ は、変数から対象領域の要素への写像です。

s : \mathrm{Var} \to |M|

自由変数を含む式を評価する場合は、どの変数にどの要素を割り当てるかを指定します。文のように自由変数を持たない式では、評価結果は変数割当の選び方に依存しません。

構文と意味の対応

構文木の各構成要素には、構造の中での解釈が対応します。

構文	意味論で行うこと
$\top$	真として評価する
$\bot$	偽として評価する
変数	変数割当から値を取り出す
定数	構造における定数の解釈を取り出す
関数適用	引数を評価し、関数の解釈へ渡す
$P(t)$	項を評価し、述語の解釈へ渡す
$t = u$	2つの項の評価結果を比較する
$\neg\alpha$	$\alpha$ の真偽を反転する
$\alpha \land \beta$	$\alpha$ と $\beta$ の両方を評価する
$\alpha \lor \beta$	$\alpha$ と $\beta$ の少なくとも一方を評価する
$\alpha \to \beta$	$\alpha$ が偽、または $\beta$ が真かを評価する
$\alpha \leftrightarrow \beta$	$\alpha$ と $\beta$ の真偽が一致するかを評価する
$\forall x\,\alpha$	対象領域の各要素で $\alpha$ を評価する
$\exists x\,\alpha$	対象領域の少なくとも一つの要素で $\alpha$ を評価する

構文木を評価する

対象領域が有限である場合に限り、構文木を再帰的に評価できます。evaluate_term() は項を対象領域の要素へ、evaluate_formula() は論理式を真偽値へ対応させます。

semantics.py

from __future__ import annotations

from collections.abc import Callable, Mapping
from dataclasses import dataclass

from formulas import (
    Conjunction,
    Disjunction,
    Equality,
    Equivalence,
    Exists,
    Falsum,
    Forall,
    Formula,
    Implication,
    Negation,
    PredicateApplication,
    Verum,
)
from terms import Constant, FunctionApplication, Term, Variable


Element = object
Assignment = Mapping[str, Element]


@dataclass(frozen=True, slots=True)
class Structure:
    domain: tuple[Element, ...]
    constants: Mapping[str, Element]
    functions: Mapping[str, Callable[..., Element]]
    predicates: Mapping[str, Callable[..., bool]]

    def __post_init__(self) -> None:
        if not self.domain:
            raise ValueError("the domain must be nonempty")


def evaluate_term(
    term: Term,
    structure: Structure,
    assignment: Assignment,
) -> Element:
    if isinstance(term, Variable):
        return assignment[term.name]
    if isinstance(term, Constant):
        return structure.constants[term.name]
    if isinstance(term, FunctionApplication):
        function = structure.functions[term.name]
        arguments = [
            evaluate_term(argument, structure, assignment)
            for argument in term.arguments
        ]
        return function(*arguments)
    raise TypeError(f"unknown term: {term!r}")


def evaluate_formula(
    formula: Formula,
    structure: Structure,
    assignment: Assignment,
) -> bool:
    if isinstance(formula, Verum):
        return True
    if isinstance(formula, Falsum):
        return False
    if isinstance(formula, PredicateApplication):
        predicate = structure.predicates[formula.name]
        arguments = [
            evaluate_term(argument, structure, assignment)
            for argument in formula.arguments
        ]
        return predicate(*arguments)
    if isinstance(formula, Equality):
        return (
            evaluate_term(formula.left, structure, assignment)
            == evaluate_term(formula.right, structure, assignment)
        )
    if isinstance(formula, Negation):
        return not evaluate_formula(formula.formula, structure, assignment)
    if isinstance(formula, Conjunction):
        return (
            evaluate_formula(formula.left, structure, assignment)
            and evaluate_formula(formula.right, structure, assignment)
        )
    if isinstance(formula, Disjunction):
        return (
            evaluate_formula(formula.left, structure, assignment)
            or evaluate_formula(formula.right, structure, assignment)
        )
    if isinstance(formula, Implication):
        return (
            not evaluate_formula(formula.left, structure, assignment)
            or evaluate_formula(formula.right, structure, assignment)
        )
    if isinstance(formula, Equivalence):
        return (
            evaluate_formula(formula.left, structure, assignment)
            == evaluate_formula(formula.right, structure, assignment)
        )
    if isinstance(formula, Forall):
        return all(
            evaluate_formula(
                formula.formula,
                structure,
                {**assignment, formula.variable.name: value},
            )
            for value in structure.domain
        )
    if isinstance(formula, Exists):
        return any(
            evaluate_formula(
                formula.formula,
                structure,
                {**assignment, formula.variable.name: value},
            )
            for value in structure.domain
        )
    raise TypeError(f"unknown formula: {formula!r}")

全称量化では、変数割当を対象領域の各要素で更新してすべての結果を調べます。存在量化では、少なくとも一つの結果が真になるかを調べます。量化された変数だけを更新するため、外側にある自由変数への割当は保たれます。

有限構造で評価する

まず、自由変数を持つ $P(x)$ に、変数割当を与えて評価します。ここでは $P$ を偶数であることを表す述語として解釈します。

semantics_example.py

from formulas import Exists, Forall, Implication, PredicateApplication
from semantics import Structure, evaluate_formula
from terms import Variable


structure_4 = Structure(
    domain=(0, 1, 2, 3),
    constants={},
    functions={},
    predicates={
        "Even": lambda value: value % 2 == 0,
        "Successor": lambda left, right: right == left + 1,
    },
)

x = Variable("x")
y = Variable("y")
even_x = PredicateApplication("Even", (x,))
every_even_has_successor = Forall(
    x,
    Implication(
        even_x,
        Exists(y, PredicateApplication("Successor", (x, y))),
    ),
)

print(evaluate_formula(even_x, structure_4, {"x": 2}))
print(evaluate_formula(even_x, structure_4, {"x": 1}))
print(evaluate_formula(every_even_has_successor, structure_4, {}))

True
False
True

3つ目の式は、$\forall x\,(\operatorname{Even}(x) \to \exists y\,\operatorname{Successor}(x, y))$ を表します。対象領域が $\{0, 1, 2, 3\}$ なら、偶数の $0$ と $2$ にはそれぞれ後者 $1$ と $3$ が存在するため真になります。

対象領域を $\{0, 1, 2\}$ へ変えると、$2$ の後者が領域にないため、同じ閉論理式が偽になります。

structure_3 = Structure(
    domain=(0, 1, 2),
    constants={},
    functions={},
    predicates=structure_4.predicates,
)

print(evaluate_formula(every_even_has_successor, structure_3, {}))

False

一つの構造で論理式が真になったことは、その論理式がすべての構造で真になることを意味しません。有限構造での評価結果と、論理式の妥当性は区別してください。

証明論との違い

証明論では、次の記号で「$\Sigma$ から $\varphi$ を導ける」ことを表します。

\Sigma \vdash \varphi

意味論では、次の記号で「$\Sigma$ を満たすすべての構造で $\varphi$ が真になる」ことを表します。

\Sigma \models \varphi

両者は似た結論を表しますが、定義は異なります。

観点	問い
証明論	公理と推論規則から $\varphi$ を導けるか
意味論	$\Sigma$ の公理を満たすすべての構造で $\varphi$ が真か

Pythonで証明列を検査する処理と、Pythonで一つの構造を評価する処理は、同じ論理式を扱えても別の操作です。

健全性と完全性

証明論と意味論は、健全性と完全性によって接続されます。

\Sigma \vdash \varphi \implies \Sigma \models \varphi

これは健全性を表します。証明できる式は、$\Sigma$ のすべてのモデルで真になります。

\Sigma \models \varphi \implies \Sigma \vdash \varphi

これは完全性を表します。$\Sigma$ のすべてのモデルで真になる式を、形式体系の中で証明できます。

Pythonで扱える範囲

今回の評価器は、構文木・構造・変数割当の関係を動かして確認するためのモデルです。次のことは扱いません。

対象領域が無限である構造に対する $\forall$ と $\exists$ の評価
関数記号や述語記号の解釈が、対象領域上で全域的に定義されていることの証明
任意の構造で成り立つこと、すなわち $\Sigma \models \varphi$ の確認
健全性・完全性そのものの証明

特に、Pythonで有限構造を一つ評価しただけでは、健全性も完全性も確認できません。これらは、個々の構文木や証明列を超えたメタ理論上の性質です。

厳密な証明へ進むなら

今回のようなPython実装は、定義を分解し、具体例で振る舞いを観察する用途に向いています。一方で、量化を含む意味論、代入補題、健全性、完全性まで厳密に扱うには、定義と証明を同じ形式体系で管理できる証明支援系が適しています。

LeanやCoqでは、論理式・構造・満たすという関係を帰納的に定義し、その性質を定理として証明できます。今回の評価器で確認した「構文木に構造と変数割当を与える」という対応は、そのような形式化へ進むための入口になります。

まとめ

構文木は論理式の形を表し、構造と変数割当が記号の意味を与える
最小評価器では、有限構造における項・論理式・量化記号の評価を確認できる
証明論は $\Sigma \vdash \varphi$、意味論は $\Sigma \models \varphi$ を扱う
健全性・完全性は証明論と意味論を接続するメタ理論上の定理である
任意の構造について厳密に証明するには、LeanやCoqのような証明支援系が適している

Pythonによる実装では、構文・公理・証明・意味の役割分担を具体例とともに確認できます。そこから一般の定理を厳密に扱う段階では、証明支援系へ移るのが自然です。

参考