「直観主義型理論（ITT, Intuitionistic Type Theory）」勉強会ノート其ノ拾伍「直和の応用（途中から）」（予習編）

　シリーズの他の回はこちらから。

&規則

　はてなブログでは"&"をTeX記法でうまく表示できないという問題に直面しているがそれはさておき。

　 と のときと同様、 が に依存しないときに以下のようになる。

　&

&の規則は以下の下段である。

　この前と同様 と と&の規則を並べることで対応関係をわかりやすくしている。

&形成則

　この前は"generalization"という言葉がよくわからない意味で使われていると思っていたが、勘違いだった。& が命題だというには普通は と が命題だとわかっている必要があるが、ここでは が命題だというのは という仮定のもとでわかっていればよい、仮定なしが普通の形成則である、という意味で一般化になっている。

&導入則

　隠した証明を復元すると、& の（カノニカルな）証明は の証明 と の証明 のペア である。

&除去則

　規則の はもちろん や にできるので、よく見る除去則にすることもできる。逆にそこから今回の除去則を出すこともできる。

例：left projection

　p E

と定義し、これを の left projection（左射影）と呼ぶ。

のように、 の要素 を実行すると が得られ、Eの代入をやると （メソッド を実行すると のカノニカルな要素が得られる）が得られるので、除去則と等号則のインスタンスとして以下の左射影則が得られる（p が に依存しているので前提の は隠せない）。

論理的な解釈をすると、が真なとき を満たす の要素が得られるということを意味する（テキストの は誤植かと）。この項は唯一のものを 演算子で表したり（）なんらかのあるものを 演算子で表したりする（）が、このような演算子は直観主義的には必要ない。何故なら  が真であるのはそれが証明ができるときなので（項を指定する必要はない）。項 については困難な点がある。これは性質  に項を対応させる関数として構成されるのであって  の証明の関数ではないということである。なのでヒルベルトは上にかいたような 規則を導入した。ITTではこれは余計になる。もうひとつは後ほど。※このあたりは数学の哲学の深い話っぽい。

例：right projection

　q E

と定義し、これを の right projection（右射影）と呼ぶ。テキストにいろいろと説明があるのだが、要するに から p が得られ、除去則と等号則のインスタンスとして以下の右射影則が得られるのである。

ヒルベルトのもうひとつの 規則（テキストは誤植だと思う）は右射影のふたつめの規則があれば必要ない。また、ひとつめの規則から我々のよく知るより強い&除去則が得られる。 が に依存しないとき、証明（construction）を隠せばよい。 が に依存している場合は左射影と同様で結論部が に依存しているので前提部の は隠せない。

連言の公理とその他の応用

　私の担当ではないのでよろしく。

　やっぱり導出をかくと命題論理の自然演繹みたいになるということであろう。