A $j$-translation with Kripke forcing relation
In this paper, we introduce a translation that combines the $j$-translation with Kripke forcing in the internal logic of an elementary topos. First, we show that our translation is sound for intuitionistic first-order logic and Heyting arithmetic. Furthermore, its interpretation in the effective topos provides an extension of the sheaf model of realizability introduced by de Jongh and Goodman. As an application, we systematically investigate translations for semi-classical axioms. Based on this investigation, we establish a separation result on semi-classical arithmetics, which cannot be…
Comments and reviews
No comments yet.
API
curl /api/v1/records/arxiv/2602.23218
curl -X POST /api/v1/records/arxiv/2602.23218/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2602.23218/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'