曇りなき眼で見定めブログ

学生です。勉強したことを書いていく所存です。リンクもコメントも自由です! お手柔らかに。。。更新のお知らせはTwitter@cut_eliminationで

直観主義型理論

「直観主義型理論(ITT, Intuitionistic Type Theory)」勉強会ノート其ノ弐拾参「有限集合」「無矛盾性」(復習編)

こちらの復習編を簡単に。 であるが、 に添字がいるのかどうか、議論になった。 のケースを見ると機能していそうな感じはある。 除去則のオルタナティブの正当化の後半で 除去則を使えばもっと簡単だった。 型理論 (レクチャーノート/ソフトウェア学 1) 近…

「直観主義型理論(ITT, Intuitionistic Type Theory)」勉強会ノート其ノ弐拾弐「命題的な(?)等しさ(途中から)」(復習編)

こちらの復習編。 同一性の除去公理 わたくし的に気になったのは、プリンキピアでは性質に量化しているがITTではそれができないという点で、集合族を で束縛することもできるのに何故だろうと思った。しかしITTはどうも高階論理に対応するものではないので、…

「直観主義型理論(ITT, Intuitionistic Type Theory)」勉強会ノート其ノ弐拾壱「有限集合」「無矛盾性」(予習編)

直観主義型理論でごんす。 有限集合 規則 これまでの規則はすべて、ある集合(あるいは集合族)からある集合を作るものだったが、ここで導入する有限集合は前提なしに直接に与えられるものである。 によって無限個のルールがあることに注意。 形成則 前提が…

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

こちらの復習編。簡単に。 直和 は任意の集合の直和でここでは二つの集合の直和である。違いは数だけではない。 ではインデックス? ラベル? のようなものと集合族とで直和を形成したが、ここでは集合と集合からである。なので&にあった非対称性が にはない…

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

過去のシリーズはこちらから。 今回は自分の担当ではないので内容がないよう。 二つの集合の直和 数を指定しない直和は連言になって二つの集合の直和は選言になるというのはなんか凄い。 というまた新しいのが出てきた。 命題的な(?)等しさ "propositional"…

「直観主義型理論(ITT, Intuitionistic Type Theory)」勉強会ノート其ノ拾八「選択公理」「"〇〇 such that □□"みたいなやつ」(復習編)

こちらの復習編。 選択公理について ACとAC'という二つの形の選択公理が出てきた。これらの同値性は新井先生の本で証明されているが、 ITTにおいても同値になるのかどうかはまだ調べていないのでわからない… 基幹講座 数学 集合・論理と位相 作者:新井 敏康 …

「直観主義型理論(ITT, Intuitionistic Type Theory)」勉強会ノート其ノ拾七「選択公理」「"〇〇 such that □□"みたいなやつ」(予習編)

直観主義型理論シリーズ。他の回はこちらから。 選択公理 選択公理はITTでは定理になる。 選択公理の定式化 新井敏康『集合・論理と位相』を参考にする。 基幹講座 数学 集合・論理と位相 作者:新井 敏康 東京図書 Amazon 選択公理は以下のような定式化が一…

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

こちらの復習編。 左射影 p の依存型のときの論理読み(存在量化のとき)というのは、 の witness を取り出すということになろうかと。それがヒルベルトのアレになる。右射影だとその個体について成り立つ性質を取り出すことになる。 右射影 左射影と同じよ…

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

シリーズの他の回はこちらから。 &規則 はてなブログでは"&"をTeX記法でうまく表示できないという問題に直面しているがそれはさておき。 と のときと同様、 が に依存しないときに以下のようになる。 & &の規則は以下の下段である。 この前と同様 と と&の規…

「直観主義型理論(ITT, Intuitionistic Type Theory)」勉強会ノート其ノ拾四「デカルト積の応用(途中から)」「集合族の直和」「直和の応用(途中まで)」(復習編)

こちらなどの復習編 コンビネータ コンビネータの導出は普通の命題論理の自然演繹と比較するとわかりやすいのではないかとなったので、載せときます。 だいたい同じですな。 項を隠す 型付ラムダ計算で にあたるのは であろう。つまり、 という型を持ったな…

「直観主義型理論(ITT, Intuitionistic Type Theory)」勉強会ノート其ノ拾参「集合族の直和」「直和の応用(途中まで)」(予習編)

他の回はこちらから。 自分の担当ではないので緩く書こうと思ったが、緩くいこうとするととことん書くことのない回であった。 の規則もと&と並べて書くとわかりやすそうである。 EがApと比べて計算との対比がイメージしにくいがこれはなんだろう?

「直観主義型理論(ITT, Intuitionistic Type Theory)」勉強会ノート其ノ拾弐「集合族のデカルト積(途中から)」「定義による同等性」「デカルト積の応用(途中まで)」(復習編)

こちらの復習編。他の回はこちらから。 名前(name) 前回もそうだったが、プログラムの「名前(name)」というのがなんなのかよくわからない。計算機科学ではよくある言い回しなのだろうか。 名前はわかっているけど実際の計算はよくわからないようなプログ…

「直観主義型理論(ITT, Intuitionistic Type Theory)」勉強会ノート其ノ拾壱「デカルト積の応用」(予習編)

Per Martin-Löfの"Intuitionistic Type Theory"(1984)の勉強会の記録。他の回はこちらから。 今回は「デカルト積の応用」の節のみ。 登場する論理規則は以下の画像を参照。比較のために等号規則を除いた規則も載せた。 含意の定義 これは が に依存しない…

「直観主義型理論(ITT, Intuitionistic Type Theory)」勉強会ノート其ノ拾「規則一般についての注意」「集合族のデカルト積(途中まで)」(復習編)

こちらの復習編。時間の都合上 -導入則まで。 規則一般についての注意 等式(等号) 4つ目の規則である等式の規則は、(必ずしも)カノニカルでない要素間の等しさを定めているものと思われる。カノニカルな要素間の等しさは導入則で定められている。除去則…

「直観主義型理論(ITT, Intuitionistic Type Theory)」勉強会ノート其ノ九「規則一般についての注意」「集合族のデカルト積」「定義による同等性」(予習編)

他の回はこちらから。 今回は私の担当ではないのでゆるく。 規則一般についての注意 四種の規則が出てくる。 formation(形成) introduction(導入) elimination(除去) equality(等号) 導入と除去は自然演繹と同じようなものである(とマーティン=レー…

「直観主義型理論(ITT, Intuitionistic Type Theory)」勉強会ノート其ノ八「複数の仮定付の判断とコンテクスト」「集合とカテゴリー」(復習編)

こちらの復習編。他の回はカテゴリー「直観主義型理論」からどうぞ。 複数の仮定付の判断とコンテクスト B(x)の要素問題 予習編で、仮定付判断の例えば の要素は [B(a)] だが という判断もあって妙だと書いた。 の要素は何なのか。しかしこれは仮定のスコー…

「直観主義型理論(ITT, Intuitionistic Type Theory)」勉強会ノート其ノ七「複数の仮定付の判断とコンテクスト」「集合とカテゴリー」(予習編)

他の直観主義型理論勉強会シリーズはこちらから。 複数の仮定付の判断とコンテクスト 複数の仮定付の判断の解釈 コンテクスト 代入 その他の判断 集合とカテゴリー カテゴリーとは(集合との違い) 単純型理論と分岐型理論と可述性 関数はプリミティブ デー…

「直観主義型理論(ITT, Intuitionistic Type Theory)」勉強会ノート其ノ六「等号の規則」「仮定付判断と代入規則」(復習編)

お休みを挟んでこれの復習編。 等号の規則 これは導出可能規則と言ってもよさそうだけど、どうも導出体系ではないという点が重要そうなのでそうは言えない。特にカノニカルな要素を得る計算というのはあまりフォーマルに導入されていない。 が集合だと言って…

「直観主義型理論(ITT, Intuitionistic Type Theory)」勉強会ノート其ノ伍「等号の規則」「仮定付判断と代入規則」(予習編)

今回は私の担当ではないのでゆるく。 等号の規則 前回は"equality"を「同等性」とか「等しさ」と訳していたけど、今回は「等号」という訳も使う。記号と考えたほうが「規則」という概念と相性がいいかと思い。「判断の形式の解釈」の節では「カノニカルナ要…

「直観主義型理論(ITT, Intuitionistic Type Theory)」勉強会ノート其ノ四「判断の形式の解釈」「命題」(復習編)

予習編はこちら 「直観主義型理論(ITT, Intuitionistic Type Theory)」勉強会ノート其ノ参「判断の形式の解釈」「命題」(予習編) - 曇りなき眼で見定めブログ 集合は型だと思ったほうがいいかも 3つの哲学 何がカノニカルな要素か? equality カノニカル…

「直観主義型理論(ITT, Intuitionistic Type Theory)」勉強会ノート其ノ参「判断の形式の解釈」「命題」(予習編)

Per Martin-Löf, "Intuitionistic Type Theory", 1984の「判断の形式の解釈」「命題」の章を読んで訳したり考えたりしています。 判断の形式の解釈(Explanations of the forms of judgements) canonical、equality、computation 解釈とは 解釈と訳したのは…

「直観主義型理論(ITT, Intuitionistic Type Theory)」勉強会ノート其ノ弍「緒言」「命題と判断」(復習編)

「直観主義型理論(ITT, Intuitionistic Type Theory)」勉強会ノート其ノ壱「緒言」「命題と判断」(予習編) - 曇りなき眼で見定めブログ これの復習編です。 緒言 It is free from the deficiency of Russell's ramified theory of types, as regards the…

「直観主義型理論(ITT, Intuitionistic Type Theory)」勉強会ノート其ノ壱「緒言」「命題と判断」(予習編)

Per Martin-Löfの"Intuitionistic Type Theory"(1984)、通称ITT84*1の勉強会の記録でござる。今回はとりあえず、最初の2節で読んでもわからなかったところをメモっときます。 個人的な動機 緒言(Introductory remarks) ロジックと数学の関係 ラッセルの型…