スピノザ『エチカ』の依存グラフをつくった

スピノザの『エチカ』は ordine geometrico demonstrata — 幾何学的秩序にしたがって証明された、という副題がついている。読んでみるとその通りで、8つの定義と7つの公理を最初に置いて、そこから36の命題を一つずつ導いていく。各命題の証明には「定義3と定義5より明らか」のように、参照先が全部書いてある。

この構造は判決文に近い。裁判官は条文を引用し、事実を認定し、「第3条および上記事実により、〇〇が成立する」と結論する。前に確定したことだけを根拠にして積み上げる。

ただ、判決文と違って一直線ではない。命題14は命題11と命題5と定義6を同時に使っているし、命題29は6つの先行命題を参照している。複数の論証が合流して一つの結論になる。上から順に読んでいると、この分岐と合流の構造が見えない。

なのでグラフにした。約60ノード、約100本のエッジ。ノードをクリックすると上流が赤、下流が青になる。

描いてみて驚いたのは、D6 — 「神」の定義 — がどれだけ多くの命題に効いているかだった。9回直接参照されていて、間接参照を含めるとほぼ全域に及ぶ。P11 (神の存在証明) と P14 (神以外の実体の否定) は巨大なハブで、ここを通らないと後半に進めない。逆に A2 (自己認識の公理) は第1部では一度も使われていない。

テキストで読んでいたときは36の命題が等しく並んでいるように感じていたが、グラフにすると地形が見える。定義の置き方で全体が決まっている。

Proof Debugger もつくった。命題を選ぶと、その証明が依存している命題・定義・公理をたどっていける。