「直観主義型理論（ITT, Intuitionistic Type Theory）」勉強会ノート其ノ弐拾「二つの集合の直和」「命題的な(?)等しさ（途中まで）」（復習編）

　こちらの復習編。簡単に。

直和

　 $\Sigma$ は任意の集合の直和でここでは二つの集合の直和である。違いは数だけではない。 $\Sigma$ ではインデックス？ラベル？のようなものと集合族とで直和を形成したが、ここでは集合と集合からである。なので&にあった非対称性が $\land$ にはない。

選言

　一般的な自然演繹では $A$ から規則で $A \land B$ を導くと $A$ から出てきたのか $B$ から出てきたのかという情報が落ちてしまう。しかしITTでは construction として残っている。それが良い。

　選言を含む命題論理のトートロジーの証明が例として出ている。ここで $\land$ 除去則は依存しないケースとして導入されているが、依存したらどうなるのだろう。その場合は例の途中で含意に書き換える前の全称良化の形に現れている。 $A + B$ は全称量化のドメインの直和ということになる。この述語論理と命題論理の対応はおもしろい。

internal form

　31ページに出てくる"an internal form of $=$ "というフレーズの意味がよくわからなかった。

フレーゲのパズル

　意味と意義の区別の話が出ている。ここでは sense が意味（Bedeutung）で meaning が意義"Sinn"である。また、sense とは method の value のことでもある。meaning は intentional（内包的）である。 $2^2$ と $2 + 2$ は内包が違うが値は同じ、意義は違うが意味は同じ、である。