ジラールのパラドックス

ジラールのパラドックス(Girard's paradox)

集合論の文脈でのパラドックスであるラッセルのパラドックス

型理論の中でのパラドックスであるジラールのパラドックス

簡略化したものがHurkensのパラドックスらしい

$ \mathrm{Type} : \mathrm{Type} のように、型$ \mathrm{Type} が型$ \mathrm{Type} に含まれてしまって矛盾を起こす

こういうものは非可述的と言われる

読む文献

Doug Howe のThe Computational Behaviour of Girard's Paradox

Thierry Coquandの An Analysis of Girard's Paradox (LICS 1986)

確認用

Q. ジラールのパラドックス