About: 直観主義型理論

直観主義型理論（ちょっかんしゅぎかたりろん、英: intuitionistic type theory）とは、数学の代替基盤を目指して論理学・哲学者のペール・マルティン＝レーフによって開発された型理論を言う。構成的型理論（constructive type theory）、またはマルティン＝レーフの型理論（Martin-Löf's type theory）とも呼ばれる。1972年に最初のバージョンが発表された。直観主義型理論には複数のバージョンがある。 マルティン＝レーフは当初非可述的な定義が可能な型理論を構築していたが、ジャン＝イヴ・ジラール（Jean-Yves Girard）によってパラドックスを起こすことが指摘され一時頓挫した（）。その後、パラドックスを起こさない可述的なバージョンが発表された。ただし、すべてのバージョンは、依存型を使用した構成的論理のコア設計を維持している。