形式論理記号の読み方 — ∀、⇒、×をテストコードへ移して読む

定義

形式論理（formal logic） は、文を記号で書き、その意味ではなく形だけから真偽を機械的に判定できるようにする表記法です。

「ログインしていない人にはボタンを無効にする」という文は、人によって少しずつ読み方が異なります。ボタンを表示しなければよいのか、表示するが押せなければよいのか。記号で書けば読み方は一つになります。

\forall x \in \Omega,\quad \neg Auth(x) \Rightarrow \neg Enabled(x)

この文書では、仕様と証明でよく使う記号を、値を集める集合記号、真偽を結ぶ論理結合子、「すべて」と「ある」を表す量化子の三つに分けて説明します。各記号を TypeScript に移したコードも示します。コードとして読めれば、記号は難しくありません。

なぜ必要か

テストは結局、「この入力でこの性質が守られるか」を問うものです。しかし「この入力」と「この性質」を文章で書くと、二つの場所に穴ができます。

範囲が曖昧です。 「さまざまな画面幅」は個数も境界も示しません。Width = {320, ..., 3840} なら3,521個だと分かります。
方向が曖昧です。 「編集者なら使える」が「編集者だけが使える」まで意味するかは文章だけでは不明です。記号なら ⇒ と ⇔ が分かれるため混同できません。

AI に仕様を渡すときは特に重要です。文章仕様は実装しやすい方向に解釈されがちですが、記号仕様にはその余地がほとんどありません。Bend のような証明言語が受け取る入力も、結局はこの記号をコードにしたものです。

仕組み

集合：値を集めた袋

集合は重複のない値の集まりです。テストで「可能な入力をすべて」列挙するときに使います。

記号	読み方	例	TypeScript では
`{a, b, c}`	a、b、cからなる集合	`Auth = {false, true}`	`const auth = [false, true]`
`x ∈ A`	xはAに属する	`768 ∈ Width`	`A.includes(x)`
`A ⊆ B`	AはすべてBに含まれる	`S ⊆ Ω`	`A.every((x) => B.includes(x))`
`A × B`	AとBから一つずつ選ぶ全ての組	`Width × Auth`	二重の `for` または `flatMap`
`{x ∈ A ∣ C(x)}`	AのうちCを満たすもの	不可能な組合せを除く	`A.filter(C)`
`A ∪ B`	和集合：どちらかにある	領域を結合	`new Set([...A, ...B])`
`A ∩ B`	積集合：両方にある	重なる領域を確認	`A.filter((x) => B.includes(x))`
`∅`	要素が一つもない集合	重なりなし	`[]`
`∣A∣`	Aの要素数	`∣Auth∣ = 2`	`A.length`

×（直積）はテスト空間を作るときに最もよく使います。

Auth \times Permission = \{(false, viewer), (false, editor), \dots, (true, admin)\}

個数は掛け算で増えます。∣A × B∣ = ∣A∣ × ∣B∣ なので、2 × 3 は6組です。軸を一つ足すたびにテスト空間が乗算で大きくなる理由です。

const omega = widths.flatMap((width) =>
  auths.flatMap((auth) => roles.map((role) => ({ width, auth, role }))),
);

{x ∈ A ∣ C(x)} は条件付き内包表記と呼びます。縦棒 ∣ の左は「どこから選ぶか」、右は「どんな条件で選ぶか」です。filter と同じ形です。

Ω（オメガ）や P₁ は特別な記号ではなく、集合につけた名前です。下付き文字は番号です。Ω₀ と Ω₁ は最初の空間と次の版の空間を表します。

論理結合子：真偽を結ぶ接着剤

命題は真か偽のどちらかに決まる文です。「768は767より大きい」は命題ですが、「ボタンをきれいにしよう」は命題ではありません。結合子は複数の命題をつないで新しい命題を作ります。

記号	名前	読み方	TypeScript
`¬P`	否定	Pではない	`!p`
`P ∧ Q`	論理積	PかつQ	`p && q`
`P ∨ Q`	論理和	PまたはQ（両方でもよい）	`p \|\| q`
`P ⇒ Q`	含意	PならばQ	`!p \|\| q`
`P ⇔ Q`	同値	PとQが同時に真、または同時に偽	`p === q`

真（T）と偽（F）の全組合せは次の通りです。これを真理値表と呼びます。

P	Q	`P ∧ Q`	`P ∨ Q`	`P ⇒ Q`	`P ⇔ Q`
T	T	T	T	T	T
T	F	F	T	F	F
F	T	F	T	T	F
F	F	F	F	T	T

⇒ が直感に反して見えます。P ⇒ Q が偽になるのは、Pが真でQが偽の一場合だけです。Pが偽なら、Qが何であっても真です。

約束だと考えると分かりやすいでしょう。「雨なら傘を持つ」と言ったのに雨が降らなかった場合、傘を持っていてもいなくても約束違反ではありません。破る機会がなかったからです。TypeScript では !p || q になります。

この性質がテストで**空虚な真（vacuous truth）**を生みます。「ログイン済みなら編集可能」を検査しても、ログイン済みの入力が一つもなければ全テストが通ります。条件が一度も真になっていないからです。

含意を逆にするときの注意

P ⇒ Q から派生する命題は三つありますが、元の命題と同じ意味なのは一つだけです。

名前	形	元と同じ意味か
元の命題	`P ⇒ Q`	基準
対偶	`¬Q ⇒ ¬P`	同じ
逆	`Q ⇒ P`	異なる
裏	`¬P ⇒ ¬Q`	異なる

「未ログインなら無効」（¬Auth ⇒ ¬Enabled）の対偶は「有効ならログイン済み」（Enabled ⇒ Auth）です。両者は全く同じ法則なので、テストしやすい方を使えます。

裏も異なります。「未ログインなら無効」から「ログイン済みなら有効」は導けません。viewer はログインしていても無効かもしれません。禁止の法則だけを書き、逆向きまで保証したと誤解すると、何もしない実装もテストを通ってしまいます。

`⇔` は双方向をまとめる

(P \iff Q) \equiv (P \Rightarrow Q) \land (Q \Rightarrow P)

≡ は「二つの式が常に同じ真偽を持つ」という意味です。つまり一つの ⇔ には二つの法則が入っています。

Enabled \iff Auth \land CanEdit \land Wide

この一行を分解すると次の通りです。

⇒ 方向：有効なら三条件すべてが真です。対偶を取ると「一つでも偽なら無効」となり、禁止法則L1〜L3が得られます。
⇐ 方向：三条件すべてが真なら有効です。これが義務法則L4です。

仕様を ⇔ で書けば禁止と義務を同時に固定できます。⇒ だけなら半分が抜けます。

優先順位

括弧がなければ ¬、∧、∨、⇒、⇔ の順で先に結びます。掛け算が足し算より先なのと同じです。

\neg P \land Q \Rightarrow R \quad\equiv\quad ((\neg P) \land Q) \Rightarrow R

迷ったら括弧を付けるのが安全です。括弧が多すぎて間違いになる仕様はありません。

量化子：「すべて」と「ある」

結合子だけでは一つの入力についてしか語れません。「すべての入力について」と言うには量化子が必要です。

記号	名前	読み方	TypeScript
`∀x ∈ A, P(x)`	全称量化子	AのすべてのxでP(x)が真	`A.every(P)`
`∃x ∈ A, P(x)`	存在量化子	AにP(x)を満たすxが少なくとも一つある	`A.some(P)`

∀ は All の A に似ており、∃ は Exists の E を反転した形です。

P(x) のように入力を受けて真偽を返すものを述語と呼びます。TypeScript では (x) => boolean 関数です。

反例は `∀` の否定

\neg\, \forall x,\ P(x) \iff \exists x,\ \neg P(x)

「全員がPである」が偽ということは、「Pでないものが少なくとも一つある」という意味です。その一つが反例です。

テストと証明のできることは異なります。

∀ が真だと示すにはすべてのケースを調べます。空間が有限で小さければ列挙し、無限または大きければ証明が必要です。
∀ が偽だと示すには反例一つで十分です。プロパティベーステストの道具が探すのはこの反例です。

1,000回のテストが通ったことは次のように書けます。

\forall x \in S,\ P(x) \qquad S \subseteq \Omega,\ \ \lvert S \rvert = 1000

S が Ω 全体でなければ、∀x ∈ Ω, P(x) はまだ不明です。通過したテストと証明の違いは記号で一行に表せます。

空集合上の `∀` は常に真

\forall x \in \varnothing,\ P(x)

Pが何であってもこの命題は真です。確認する要素がなく、違反する要素もないからです。JavaScript でも [].every(() => false) は true です。条件が矛盾して入力が0件なのに「すべて通過」と報告される事故はここから起きます。∀ を調べるときは、条件を満たす入力が実際にあるか、対になる ∃ も確認しましょう。

量化子の順序を変えると意味が変わる

\forall x\, \exists y,\ Mother(y, x) \qquad\text{vs}\qquad \exists y\, \forall x,\ Mother(y, x)

左は「すべての人には母がいる」です。右は「すべての人の母である一人がいる」です。二つの記号の順序を変えただけで主張は全く変わります。

テストも同じです。「すべてのユーザーには使える役割がある」と「全ユーザーが使える一つの役割がある」は別の要求です。

関数表記

表記	意味	例
`f(x)`	fにxを入れた結果	`I(x)`：実装に入力xを渡した結果
`f: A → B`	Aの値を受け取りBの値を返す関数	`π: Result → Bool`
`f(g(x))`	先にg、その結果にf	`U(U(s, p), p)`：同じ更新を二度適用
`π`	射影：必要な部分だけ選ぶ	`π(result) = result.enabled`

ここでの π は円周率ではなく、射影（projection）から取った名前です。「何を見て等しいと判断するか」を決める関数です。

実務での適用

長い式は外側から内側へ読む

defining-done-for-ai-code では「完全な実装」を次のように書いています。

Perfect(I) \iff \forall x \in \Omega,\quad P\big(x,\ \pi(I(x))\big)

外側から一層ずつ剥がします。

Perfect(I) ⇔ …：実装Iが完全であることは右辺と同じ意味です。
∀x ∈ Ω：空間Ωのすべての入力xについて
I(x)：実装にxを渡し
π(…)：結果から見る部分だけを選び
P(x, …)：入力とともに法則Pへ渡すと真です。

コードにすると一行です。

const perfect = omega.every((x) => P(x, pi(I(x))));

Bend 構文との対応

証明言語 Bend 2 はこの記号をコードで書きます。Bend ガイドは「命題は型であり、証明はその型のdef」と説明します。この対応をカリー＝ハワード対応と呼びます。

論理記号	Bend構文	説明
`∀x ∈ T`	`for x: T`	lawの束縛子。証明defでは引数になる
`∃z ∈ C`	`exs z: C`	証人 `(z, proof)` の組を返す必要がある
`a = b`	`{a == b : T}`	等式命題
`a ≠ b`	`{a != b : T}`	`{a == b : T} -> Empty` の短縮形
`P ⇒ Q`	`P -> Q` または追加の `for h: P`	Pの証明を受けQの証明を返す関数
偽	`Empty`	値が一つもない型

P ⇒ Q の証明が関数である点が重要です。「Pの証拠をくれればQの証拠を作る」という約束だからです。仮定が引数になり、目標が仮定と同じ形になれば、その引数を返すだけで証明が終わります。

law wide_editor_is_enabled:
  for width: Nat
  for wide: {Nat.is_ge(width, 768n) == True{} : Bool}
  {E.enabled(True{}, E.Editor{}, width) == True{} : Bool}

def Laws.wide_editor_is_enabled(width, wide):
  wide

{==} は反射律、つまり「両辺を計算すると同じ」として等式を証明します。≠ が -> Empty なのも同じ原理です。「等しい証拠をくれれば不可能なものを作れる」ので「等しくない」になります。

仕様を記号に移す手順

Width = {320, …, 3840} のように、範囲と単位も含めて入力軸ごとに集合を書きます。
軸を × で結んで空間 Ω を作ります。除く組合せがあれば {x ∈ Ω ∣ C(x)} と書き、Cの根拠を記録します。
まず法則を ⇔ で書きます。⇒ だけで十分か、逆向きも必要かが見えます。
先頭に ∀x ∈ Ω を付け、対として ∃x ∈ Ω（条件を満たす入力が実在するか）も確認します。
各記号を TypeScript の every、some、filter に移し、小さな空間で実行します。

トレードオフ

記号は短く曖昧さがありませんが、初めて読む人には障壁です。仕様書では記号のすぐ下に平易な説明を置きましょう。
正確な記号で書いた仕様も、間違った仕様なら間違ったまま正確です。境界を1000と誤記すれば、その誤りも正確に伝わります。形式化は曖昧さをなくすだけで、要求が正しいかは別途確認が必要です。
無限集合上の ∀ は列挙で確認できません。証明が必要で、証明はテストよりずっと高価です。

使わない方がよい場合

正解が複数ある領域です。レイアウトの微調整、文言、推薦順を一行の ⇔ に固定すると、通常の変更で仕様が壊れます。
何を作るか決まっていないプロトタイプです。空間と法則を書く費用が実装費用を上回ります。
チームの大半が記号を読めないのに、平易な説明なしで記号だけを残す場合です。誰もレビューできない仕様は仕様ではありません。

よくある間違い

⇒ を因果関係と読む。 P ⇒ Q は「PがQを起こす」ではなく、「Pが真でQが偽のケースがない」という意味です。
裏を元の命題と取り違える。 「未ログインなら無効」から「ログイン済みなら有効」は導けません。
空の空間で ∀ を確認する。 条件が矛盾すると入力は0件ですがテストは全通過します。∃ と対にして確認します。
∈ と ⊆ を混同する。 ∈ は一つの要素が集合に属すること、⊆ は集合全体が別の集合に含まれることです。768 ∈ Width、{767, 768} ⊆ Width。
量化子の順序を不用意に変える。 ∀∃ と ∃∀ は別の主張です。
∀x ∈ S を ∀x ∈ Ω と報告する。 テストで確認したのはSに入れた入力だけです。