場面
5世紀のアレクサンドリア。地中海沿いの図書館都市は、すでに往年の輝きを失いつつあったが、神学者たちの議論は逆に熱を帯びていた。
偽ディオニュシオス・アレオパギテス——後世にそう呼ばれることになる人物——は羊皮紙の上でペンを止めた。彼が抱えていた問題は、一見シンプルだが考えれば考えるほど深みにはまるものだった。神をどうやって記述するか。
「全知」と書けば、人間の知識を神に当てはめているに過ぎない。「善」と書けば、倫理という人間の尺度を神に押しつけている。「永遠」と書けば、時間という概念の否定を借りて何かを語ろうとしているだけだ。どんな肯定的な属性も、どこかで嘘をついている。神はあらゆるカテゴリーを超越しているのに、カテゴリーを使って語ろうとする矛盾。
この問いはディオニュシオスよりずっと前からあった。プロティノスは3世紀に「一者（ト・ヘン）」について同じ袋小路に入った。さらに遡れば、プラトンの『パルメニデス』が「一者とは何でないか」を延々と論じていた。
そして出てきた答えが「否定神学（アポファティック神学）」、あるいはラテン語で「via negativa（否定の道）」だ。神が何であるかを語るのをやめる。神が何でないかを語る。有限でない。無知でない。悪でない。部分を持たない。変化しない。こうして否定を積み重ねることで、肯定では決して到達できない真実の輪郭に近づいていく。
時は流れて1934年のウィーン。アドルフ・ヒトラーが首相になった翌年、ウィーン学団が論理実証主義の絶頂にあった時代、カール・ポパーという若い哲学者が一冊の本を出版した。『科学的発見の論理（Logik der Forschung）』。彼の問いは神学からは遠かったが、構造は驚くほど似ていた。
科学的な命題とは何か。「神は愛である」という文と「白鳥はすべて白い」という文の違いは何か。ポパーの答えは鮮やかだった。原則的に反証可能であること。誤りである可能性がある文だけが科学的命題たりうる。「白鳥はすべて白い」は黒い白鳥を一羽見つければ覆せる。だから科学だ。「神は愛である」は何があっても覆せない。だから科学ではない。
via negativaは世俗化された。神の定義から科学的真理の定義へ。「何でないか」という問いが、知識のありかを特定する技法になった。
答え
否定による定義（via negativa）は、肯定による定義よりしばしば正確で誠実だ。「何であるか」の列挙は常に不完全で、現実はその隙間から逃げ出す。しかし「何でないか」の体系は、境界を外側から精密に刻む。過剰な主張をせずに、真実の輪郭を浮かび上がらせる。
CSへの翻訳
ポパーの反証可能性がソフトウェアに入ったのは、テストという概念を通じてだ。
テストは「このコードは正しく動く」を証明しない。テストは「このコードはこれこれの条件で失敗しない」ことを確認する。常にパスするテスト——例えばモックが何を渡しても成功を返す状態——はテストではない。失敗する可能性がないテストは、反証可能性を持たない命題と同じで、何も言っていない。
1999年、ハスケルの世界からもっと過激な実装が来た。Koen ClassenとJohn Hughesが発表した「QuickCheck」だ。プロパティベーステスト（Property-based testing）と呼ばれるこのアプローチは、via negativaを自動化する。
従来のテスト：「関数fにinput Xを与えたらoutput Yが返る」（肯定的な主張）。 QuickCheckのテスト：「関数fが絶対にoutput Zを返してはいけない、というプロパティを定義せよ。そして何千ものランダムな入力を生成して、そのプロパティを破る反例を探せ」（否定的な主張）。
たとえばソート関数なら：出力の長さは入力と同じでなければならない。出力の各要素は入力に含まれていなければならない。出力の連続する二要素の間でa[i] <= a[i+1]が成立しなければならない。これらは「ソートとは何でないか」の列挙だ。このプロパティ群が破れないなら、その関数は実質的にソートしている。
型システムにも否定の論理が入っている。TypeScriptのnever型は「この値は絶対にここに到達しない」という否定的な主張だ。ユニオン型の絞り込みで全ケースを処理した後に残るneverは、「これ以上ここに来るものはない」ということを型として表現している。Rustの!型（never type）も同様だ。これらは「この型は何でないか」を明示する構文だ。
第4話のラッセル＝型理論の流れを思い出すと、型システムは元来「禁止」の道具として生まれた——自己参照を禁止することで矛盾を排除する。never 型はその系譜の現代的な末裔で、「ここに到達する値はない」という型レベルの否定神学だ。switch 文で全ケースを尽くしたあと、残った経路の型が never になっていれば、コンパイラはあなたの代わりに「ここから先は神でない」と告げてくれている。
type ScreeningStage = '書類選考' | '一次面接' | '最終面接' | '内定';
function nextStage(stage: ScreeningStage): ScreeningStage | null {
switch (stage) {
case '書類選考': return '一次面接';
case '一次面接': return '最終面接';
case '最終面接': return '内定';
case '内定': return null;
default:
// ここに来た時点で stage の型は never
// 新しい段階が追加されたら、コンパイルエラーで気づく
const exhaustive: never = stage;
throw new Error(`未対応のステージ: ${exhaustive}`);
}
}「ここには絶対に来ない」を型として表明することで、未来の変更（新しいステージの追加）が起きたときコンパイラが警告する。via negativa が型システムの中で動いている。
要件定義でも否定が力を発揮する。「システムは24時間以上前のリクエストを処理してはならない」は、「システムは有効なリクエストを正しく処理する」よりずっと精密だ。後者は「有効」と「正しく」の定義問題を含んでいる。
設計への示唆
コードレビューでvia negativaの問いを持つと、目線が変わる。「このコードは意図した通りに動くか？」ではなく、「このコードが意図せずやってしまうことは何か？」。前者は正しい入力のことしか考えていない。後者はエッジケース、副作用、予期しない呼び出しパターンを探す。
要件定義でも同じ転換が使える。
❌ 肯定的な仕様（曖昧）
「決済システムはすべての有効な支払いを正確に処理する」
「有効」とは何か？ネットワークエラー中は？残高が境界値のときは？「正確に」とは何か？どこで確認する？この仕様はテスト不可能だ。反証できない。
✅ 否定的な仕様（具体的で反証可能）
「決済システムは同一トランザクションで顧客に二重請求してはならない」
これは反証可能だ。同じトランザクションIDで二回チャージされたレコードが存在すれば、この仕様は破られている。テストが書ける。監査ログで確認できる。
テストスイートの「脆弱感」が抜けないとき、こう問い直してみる。各テストは失敗し得るか？失敗するとしたら、何が起きたときか？その失敗シナリオは実際に起こりうるか？これらの問いに答えられないテストはvia negativaを欠いている——何かを排除しているようで、実は何も主張していない。
否定神学者たちが発見したのは、真実は肯定ではなく排除によって近づくことがあるという逆説だった。ソフトウェアのテスト設計も同じ逆説の上に立っている。バグを見つけるのは「このコードは正しい」という信念ではなく、「このコードはここで間違うかもしれない」という疑いだ。
graph TB
subgraph "❌ 肯定的仕様のアプローチ"
PS[仕様：「正しく処理する」] --> PA[テスト：正常系入力 → 期待出力]
PA --> PB[問題：「正しい」の定義が曖昧]
PB --> PC[エッジケースが仕様に含まれない]
end
subgraph "✅ 否定的仕様のアプローチ via negativa"
NS[仕様：「二重請求してはならない」] --> NA[プロパティ定義：違反条件の明文化]
NA --> NB[テスト：違反条件を破る反例を自動生成]
NB --> NC[反例が見つかれば即バグ確定]
NC --> ND[反例が見つからなければ信頼性が上がる]
end
style PS fill:#ffcccc
style NS fill:#ccffccvia negativaの最も強い形は、いまプロパティベーステストの中に生きている。「この関数が絶対に破ってはいけない性質は何か」を列挙して、コンピュータに何千回も試させる。人間が思いつく肯定的なテストケースより、コンピュータが見つける否定的な反例の方が、しばしば鋭いバグを捕まえる。
偽ディオニュシオスが神学で発見し、ポパーが科学哲学で洗練させたvia negativaは、21世紀のソフトウェアエンジニアのテスト戦略として、今日も動き続けている。
問い：あなたの仕様書に「システムは〜してはならない」という文はいくつあるか。「システムは〜すべきだ」の数と比べてみてほしい。後者だけで埋まっているなら、via negativaがまだ使われていない。