TL;DR
This paper introduces two logical systems based on dependent types that are as simple as ZFC set theory and have natural set-theoretic interpretations, aiming to bridge the gap between mathematicians and type theorists.
Contribution
It presents novel dependent type systems comparable to ZFC in simplicity, with natural set-theoretic interpretations, fostering better understanding between mathematicians and computer scientists.
Findings
Two logical systems based on dependent types are comparable to ZFC.
The systems have natural set-theoretic interpretations.
The approach aims to bridge the cultural divide between different fields.
Abstract
We present two logical systems based on dependent types that are comparable to ZFC, both in terms of simplicity and having natural set theoretic interpretations. Our perspective is that of a mathematician trained in classical logic, but nevertheless we hope this paper might go some way to bridging the cultural divide between type theorists coming from computer science.
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 · Computability, Logic, AI Algorithms · Logic, Reasoning, and Knowledge