Globular探り 15：Theoremはミスリーディング

Globular探り 10：定理と証明 - 檜山正幸のキマイラ飼育記 メモ編で「定理と証明」の話をしたけど、あれは伝統的な「定理と証明」の枠組みに依拠している。ほんとのところ、Globular内では伝統的な「定理と証明」なんてありゃしない。伝統的な概念に慣れている僕らが、そう「みなしたい」という慣習的な欲望があるだけ。

有り体の事実とは、n-セル、(n+1)-セル、(n+2)-セル、…… があり、可逆セルにマークがされているだけ。「記号、項、論理式、定義、命題、定理、証明」なんて区別があるわけではない！

コマンド名がTheoremなのがミスリーディングなのだ。変なバイアスが生じる。Register（登録）とかのほうが誤解を防げたろう。

Theoremコマンドが何をするかというと、2つのセルをセルパレット（正式名称は「指標」だが、これも分かりにくい）に登録する。

1. 現在のn-ダイアグラム（ビュー領域に表示されている図形）と同じプロファイルを持つn-セル
2. 上記の新規登録されたn-セルと、n-ダイアグラムを結ぶ可逆な(n+1)-セル。

バイアスがないニュートラルな言葉として、最初のセルを（n-ダイアグラムの）サロゲートセル、二番目のセルを（n-ダイアグラムの）リライターセルと呼ぶことにする。

Theoremコマンドがなくても同じことは手動で出来る。

1. 事前に、作る予定のn-ダイアグラムと同じプロファイルのn-セルを作ってパレットに置く。これがサロゲート。
2. 今登録したセルをソースにする。
3. 目的のn-ダイアグラムを構築（build up）する。
4. n-ダイアグラムをターゲットにする。
5. (n+1)-セルが登録される。
6. 可逆指定をする。これでリライターができる。