Constructive Ackermann's interpretation
| Autor: | Hanul Jeon |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2020 |
| Předmět: | |
| Popis: | The main goal of this paper is to formulate a constructive analogue of Ackermann's observation about finite set theory and arithmetic. We will see that Heyting arithmetic is bi-interpretable with $\mathsf{CZF^{fin}}$, the finitary version of $\mathsf{CZF}$. We also examine bi-interpretability between subtheories of finitary $\mathsf{CZF}$ and Heyting arithmetic based on the modification of Fleischmann's hierarchy of formulas, and the set of hereditarily finite sets over $\mathsf{CZF}$, which turns out to be a model of $\mathsf{CZF^{fin}}$ but not a model of finitary $\mathsf{IZF}$. 16 pages |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|