Apartness and the elimination of strong forms of extensionality
Logic
2023-10-26 v1
Abstract
We introduce a new version of arithmetic in all finite types which extends the usual versions with primitive notions of extensionality and extensional equality. This new hybrid version allows us to formulate a strong form of extensionality, which we call converse extensionality. Inspired by Brouwer's notion of apartness, we show that converse extensionality can be eliminated in a way which improves on results from our previous work. We also explain how standard proof-theoretic interpretations, like realizability and functional interpretations, can be extended to such hybrid systems, and how that might be relevant to proof-mining.
Keywords
Cite
@article{arxiv.2310.16493,
title = {Apartness and the elimination of strong forms of extensionality},
author = {Benno van den Berg},
journal= {arXiv preprint arXiv:2310.16493},
year = {2023}
}