こちらの復習編。時間の都合上 -導入則まで。
規則一般についての注意
等式（等号）
4つ目の規則である等式の規則は、（必ずしも）カノニカルでない要素間の等しさを定めているものと思われる。カノニカルな要素間の等しさは導入則で定められている。除去則はちょっとわからない。
最後の段落
... we cannot further analyse them, but only explain them. However, in the end, no explanation can substitute each individual's understanding.
この一節がよくわからないという話になった。"indivisual"とはなんなのか。私は、どう説明するよりも個々人の理解のほうが重要だということだと受け取った。"substitute"とか"indivisual"とか論理学用語っぽい語が使われているのは一種のシャレではないかと。
集合族のデカルト積
4つの判断と4つの規則の関係とは？
〜 という判断には"〜"のカノニカルな要素と等しさの規定を与える必要がある。それをやっているのは導入則なので、ひとつの判断の形式に二つの規則が関わっていると思う。
Π導入則
と
、
と
の違いはなんなのかという話である。まず、
は仮定付判断ではないというのがある。それと
は
の名前だということが書いてある。「名前（name）」というのがテクニカルタームなのかそうでないのかはよくわからない。識別子とか。あと
演算子みたいなのとか。しかし、
は束縛変数の名前を変えてもよさそうなので、そう考えると名前っぽいのではないかということに。となると
もそうなる。
we cannot generate inductively all the elements
予習編で躓いたところである。前回やったようなカテゴリーと集合の区別があるが、集合はカテゴリーよりは扱いやすいが帰納的に全要素を生成できるほど強いものではないのだと思われる。そしてその上で量化を走らせるのに帰納的に全要素を生成できるという条件まではいらないのだろう。
これは直観主義数学をガチでやっている人にとっては重要なのかもしれない。帰納的に全要素を生成できるような集まりだけを認めるとするとさすがに数学を実行するには弱すぎるのではないか、と。
形成則2の正当化
この議論はフォーマルな話とインフォーマルな話が入り組んでいてけっこうわかりづらい。ちゃんとテクニカルな教科書を読むべし。
