最近のAIは能力がすごいことになっているので、文献をあさる前に聞いて知識を入れてしまった方が早いことに気づいた。ハルシネーションで間違ったことを教えられる可能性もあるが、とりあえず、筋の通った話を聞かせてくれるので、嘘でもいいので物事を覚えるには良い。
質問１：Martin-Löfの構成的型理論とはどういうものですか？
自分でまとめた要約
Per Martin-Löf（ペール・マルティン＝レーフ）の構成的型理論（Constructive Type Theory: CTT）は、数理論理学と計算機科学の基盤を結びつける、現代で最も影響力のある形式体系の一つである。
直観主義数学（構成的数学）の基礎づけとして提案されましたが、現在では「強力な型システムを持つプログラミング言語」および「定理証明支援系の理論的基盤」として広く知られている。
カリー＝ハワード同型対応（Propositions-as-Types）
命題を型に対応させるというアイディアを基盤にしている。
依存型（Dependent Types）
カリー＝ハワード同型対応は、命題と型の対応だけしか言えない。述語に対応するものがない。Martin-Löfの最大の功績は、（カリー＝ハワード同型対応を拡張して？）述語に対応する依存型（Dependent Types）を導入したこと。
その他
「構成的」型理論と呼ばれるのは、排中律を認めない直観主義論理をベースとしている理論であるため。
構成的数学において、ある命題が存在する（$\exists x. B(x)$）と言えるためには、その
x を実際に計算（構成）する方法を示さなければならない。「存在しないと仮定すると矛盾する（背理法）」だけでは、証明として認められない。が、LEANではやや異なるものもある（たとえば、選択公理）。
応用
定理証明支援系（Lean, Coq, Agda） これらはMartin-Löfの型理論（またはそれを拡張した「インダクティブ型構成の計算（CIC）」など）を直接のプログラミング言語・論理基盤として実装しています。数学の定理の厳密なチェックや、バグが絶対に許されない航空宇宙・金融の基礎ソフトウェアの検証に使われています。
質問２：カリー＝ハワード同型対応は命題と型の対応だけを表しています。また、依存型を導入することで、述語と依存型の対応というものが言えると思います。これはつまり、カリー＝ハワード同型対応を拡張していることになりませんか？
自分でまとめた要約
そのとおり
質問３：構成的型理論が、一階述語論理のカリー＝ハワード同型対応させた対応物であるならば、構成的型理論は一階述語論理の派生物、ほとんど同じものということですか？
自分でまとめた要約
構成的型理論（CTT）は第一階述語論理（FOL）とは異なる。FOLよりもはるかに凌駕する表現力を有している。具体的には以下の点である。
- 計算（アルゴリズム）
- 高階（Higher-order）の表現力
これらを最初からシステム内部に完全に融合させている点が異なる。
質問４：構成的型理論における判断（Judgement）とはなんですか？
自分でまとめた要約
判断（Judgement）は、構成的型理論における超基本概念で最も躓きやすい点。
判断とはシステムの側から下される客観的な議論の余地のない事実の宣言のこと。
命題と型がどのようにして異なるのかと言う話につながる概念。
判断とは？
通常論理学においては、命題はそれが真か偽かどうかを論じるための対象であるが、構成的型理論においては、命題がある（型がある）ということと、その命題が正しい（証明されている）ということは区別される。
Martin-Löfは、哲学者カントの言葉を引いてこう説明している、そうである。
「命題を知ること」と「それが真であると判断すること」は別である。
例えば、「明日は雨が降る」というのは単なる命題（型）だが、「『明日は雨が降る』は正しい」と確信して宣言することが「判断」である。