Notes on axiomatising Hurkens's Paradox
Arnaud Spiwack
TL;DR
This paper presents an axiomatisation of Hurkens's paradox within dependent type theory, avoiding reliance on impredicative features, thereby clarifying its foundational aspects.
Contribution
It provides the first axiomatisation of Hurkens's paradox that does not depend on impredicative assumptions in dependent type theory.
Findings
Axiomatisation without impredicative assumptions
Enhanced understanding of Hurkens's paradox foundations
Potential implications for type theory consistency
Abstract
An axiomatisation of Hurkens's paradox in dependent type theory is given without assuming any impredicative feature of said type theory.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Logic, Reasoning, and Knowledge · Philosophy and History of Science