>>924
>枝葉末節的な議論のように見えて
>実はそうでないものがあるらしい

巡回ご苦労さまです

>>925
>型理論では
>ラッセルのパラドックスを回避すべく
>∈の左右を厳密に区別しますので
>x∈xはそもそも論理式にしません

まあ、そういうことですが
要するに、集合に”型”という付加的な情報を与えて
集合演算を制限することで
ラッセルパラドックスを抑制する

さて
望月氏の∧∨議論を見た 物理屋さんが
「ショルツェは、余剰次元を分っていない」
と ネットに感想を書いていた

”型”という付加情報→”ラベル”という付加情報
と読み替えれば 良いだろう
ラッセルパラドックスの抑制と同じような効果が
”ラベル”という付加情報でも 期待できる