論理式を文字列として直接扱うと、括弧や結合の優先順位、量化記号の作用範囲を意識し続ける必要があります。構文木として表現すれば、論理式の構造をプログラムでたどれるようになります。

この記事では、一階述語論理の構文をPythonのクラスとしてモデル化し、論理式の表示と自由変数の計算を実装します。

この記事で扱うのは論理式の構文です。ある論理式が真かどうかを決める対象領域や解釈は、意味論に含まれる別の概念です。

コード例は Python 3.12 以降を前提にしています。

一階述語論理の構文

一階述語論理では、論理式を次のような部品から組み立てます。

項: 変数、定数、関数適用
原子論理式: 述語の適用や等号
論理定数: $\top$（真）と $\bot$（偽）
論理結合子: 否定、連言、選言、含意、同値
量化記号: 全称量化と存在量化

論理式を作る前に、どの記号を使う言語なのかを固定します。集合論を形式化する場合は、等号 $=$ と所属関係 $\in$ を使い、関数記号を持たない言語を選ぶことがあります。この記事では、構文木の再利用性を優先し、述語記号と関数記号を一般化して実装します。

この区別は、構文と意味論を混同しないためにも重要です。例えば $\in$ を使うことは、Pythonの集合に対する所属判定を実行することではなく、所属関係を表す述語記号を論理式へ記述することです。

例えば、次の論理式を考えます。

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

この式は、変数 $x$ と $y$、述語 $P$ と $R$、含意、全称量化、存在量化から構成されています。

ここで、$x$ と $y$ は項を表す変数であり、$P$ と $R$ は述語記号です。述語記号がどの項の組に成り立つかは、構造が解釈として与えます。構文木は、その解釈をまだ持ちません。

項を表現する

まず、項を表すクラスを定義します。今回は変数と定数、複数の項を受け取る関数適用を用意します。

terms.py

from __future__ import annotations

import re
from abc import ABC, abstractmethod
from dataclasses import dataclass
from typing import ClassVar


def validate_symbol(name: str) -> None:
    if not re.fullmatch(r"[A-Za-z_][A-Za-z0-9_]*", name):
        raise ValueError(f"invalid symbol name: {name!r}")


class Term(ABC):
    @abstractmethod
    def free_variables(self) -> frozenset[str]:
        """項に自由に現れる変数名を返す。"""


@dataclass(frozen=True, slots=True)
class Variable(Term):
    name: str

    def __post_init__(self) -> None:
        validate_symbol(self.name)

    def free_variables(self) -> frozenset[str]:
        return frozenset({self.name})

    def __str__(self) -> str:
        return self.name


@dataclass(frozen=True, slots=True)
class Constant(Term):
    name: str

    def __post_init__(self) -> None:
        validate_symbol(self.name)

    def free_variables(self) -> frozenset[str]:
        return frozenset()

    def __str__(self) -> str:
        return self.name


@dataclass(frozen=True, slots=True)
class FunctionApplication(Term):
    name: str
    arguments: tuple[Term, ...]

    def __post_init__(self) -> None:
        validate_symbol(self.name)

    def free_variables(self) -> frozenset[str]:
        return frozenset().union(
            *(argument.free_variables() for argument in self.arguments)
        )

    def __str__(self) -> str:
        arguments = ", ".join(map(str, self.arguments))
        return f"{self.name}({arguments})"

free_variables() は、その項の中に束縛されずに現れる変数を返します。例えば、Variable("x") の自由変数は $\{x\}$ ですが、Constant("zero") には自由変数がありません。

論理式を表現する

論理式も抽象基底クラスにします。原子論理式は、述語記号と項の列からなる PredicateApplication と、2つの項の等号で表します。

formulas.py

from __future__ import annotations

from dataclasses import dataclass
from typing import ClassVar

from terms import Term, Variable, validate_symbol


class Formula:
    def free_variables(self) -> frozenset[str]:
        raise NotImplementedError


@dataclass(frozen=True, slots=True)
class Verum(Formula):
    def free_variables(self) -> frozenset[str]:
        return frozenset()

    def __str__(self) -> str:
        return "⊤"


@dataclass(frozen=True, slots=True)
class Falsum(Formula):
    def free_variables(self) -> frozenset[str]:
        return frozenset()

    def __str__(self) -> str:
        return "⊥"


@dataclass(frozen=True, slots=True)
class PredicateApplication(Formula):
    name: str
    arguments: tuple[Term, ...]

    def __post_init__(self) -> None:
        validate_symbol(self.name)

    def free_variables(self) -> frozenset[str]:
        return frozenset().union(
            *(argument.free_variables() for argument in self.arguments)
        )

    def __str__(self) -> str:
        arguments = ", ".join(map(str, self.arguments))
        return f"{self.name}({arguments})"


@dataclass(frozen=True, slots=True)
class Equality(Formula):
    left: Term
    right: Term

    def free_variables(self) -> frozenset[str]:
        return self.left.free_variables() | self.right.free_variables()

    def __str__(self) -> str:
        return f"({self.left} = {self.right})"


@dataclass(frozen=True, slots=True)
class Negation(Formula):
    formula: Formula

    def free_variables(self) -> frozenset[str]:
        return self.formula.free_variables()

    def __str__(self) -> str:
        return f"¬({self.formula})"


@dataclass(frozen=True, slots=True)
class BinaryFormula(Formula):
    left: Formula
    right: Formula

    operator: ClassVar[str] = ""

    def free_variables(self) -> frozenset[str]:
        return self.left.free_variables() | self.right.free_variables()

    def __str__(self) -> str:
        return f"({self.left} {self.operator} {self.right})"


@dataclass(frozen=True, slots=True)
class Conjunction(BinaryFormula):
    operator: ClassVar[str] = "∧"


@dataclass(frozen=True, slots=True)
class Disjunction(BinaryFormula):
    operator: ClassVar[str] = "∨"


@dataclass(frozen=True, slots=True)
class Implication(BinaryFormula):
    operator: ClassVar[str] = "→"


@dataclass(frozen=True, slots=True)
class Equivalence(BinaryFormula):
    operator: ClassVar[str] = "↔"


@dataclass(frozen=True, slots=True)
class Forall(Formula):
    variable: Variable
    formula: Formula

    def free_variables(self) -> frozenset[str]:
        return self.formula.free_variables() - {self.variable.name}

    def __str__(self) -> str:
        return f"∀{self.variable}. {self.formula}"


@dataclass(frozen=True, slots=True)
class Exists(Formula):
    variable: Variable
    formula: Formula

    def free_variables(self) -> frozenset[str]:
        return self.formula.free_variables() - {self.variable.name}

    def __str__(self) -> str:
        return f"∃{self.variable}. {self.formula}"

BinaryFormula に共通処理をまとめ、演算子だけをサブクラスで指定しています。各クラスを @dataclass(frozen=True, slots=True) にしているため、構文木は作成後に変更できず、構造的な等価性も比較できます。

論理式を組み立てる

先ほどの

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

をPythonで組み立てます。

example.py

from formulas import Exists, Forall, Implication, PredicateApplication
from terms import Variable


x = Variable("x")
y = Variable("y")

formula = Forall(
    x,
    Implication(
        PredicateApplication("P", (x,)),
        Exists(
            y,
            PredicateApplication("R", (x, y)),
        ),
    ),
)

print(formula)
print(sorted(formula.free_variables()))

∀x. (P(x) → ∃y. R(x, y))
[]

$x$ と $y$ はそれぞれ対応する量化記号の作用域にあるため、この論理式には自由変数がありません。

一方、次の式では $y$ が量化されていません。

free_variables_example.py

from formulas import Conjunction, PredicateApplication
from terms import Variable


x = Variable("x")
y = Variable("y")
formula = Conjunction(
    PredicateApplication("P", (x,)),
    PredicateApplication("Q", (y,)),
)

print(sorted(formula.free_variables()))

['x', 'y']

文（閉論理式）と自由変数

自由変数を1つも持たない論理式を、文または閉論理式と呼びます。数学基礎論の文脈では「命題」と呼ばれることもありますが、この記事では、真偽値そのものと混同しないように is_sentence と表記します。

predicates.py

from formulas import Formula


def is_sentence(formula: Formula) -> bool:
    return not formula.free_variables()

ただし、自由変数がないことは、その論理式が真であることを意味しません。例えば、対象領域や述語の解釈がなければ、$\forall x\,P(x)$ の真偽は決まりません。

「命題」と「真である論理式」は別の概念です。自由変数がないことは、評価に必要な変数割当が残っていないことを意味しますが、実際の真偽は意味論によって決まります。

構文と意味論を分ける

今回のクラスが表しているのは、論理式の形だけです。

Forall は、変数を全称量化する構文を表す
PredicateApplication は、述語を項へ適用する構文を表す
free_variables() は、束縛されていない変数を構文木から計算する

一方、次の情報はまだありません。

変数が値を取る対象領域
定数記号や関数記号の解釈
述語記号がどの要素に成り立つか
論理式の真偽値

これらを Structure と変数割当として与え、論理式を評価するのが意味論です。構文木を先に独立して実装すると、構文の操作と評価規則を分離できます。

まとめ

一階述語論理の論理式を、項と論理式の構文木としてPythonで表現しました。自由変数は、各構文要素に対して次のように再帰的に計算できます。

変数: その変数自身
定数: 空集合
結合子: 子の自由変数の和集合
量化記号: 本体の自由変数から束縛変数を除く

今回の実装は構文だけを扱っており、論理式の真偽は評価しません。構文木を出発点に、代入、論理公理、証明列、意味論へと対象を広げられます。

次の記事では、構文木に対する代入と、変数捕獲を避ける置換を実装します。

次の記事：一階述語論理の代入をPythonで実装する：全称閉包と変数捕獲を避ける置換