Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A $j$-translation with Kripke forcing relation

Satoshi Nakata

Abstract

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 of semi-classical axioms. Based on this investigation, we establish a separation result on semi-classical arithmetics, which cannot be obtained using the usual $j$-realizability.

A $j$-translation with Kripke forcing relation

Abstract

In this paper, we introduce a translation that combines the -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 of semi-classical axioms. Based on this investigation, we establish a separation result on semi-classical arithmetics, which cannot be obtained using the usual -realizability.
Paper Structure (30 sections, 34 theorems, 99 equations)

This paper contains 30 sections, 34 theorems, 99 equations.

Table of Contents

  1. Introduction
  2. $j$-translation in proof theory and topos theory
  3. Local operator as generalized oracle
  4. A sheaf model of realizability
  5. Contributions
  6. Organization
  7. Preliminaries
  8. The internal language of a topos
  9. Other notation
  10. Arithmetic
  11. Internal $j$-translation
  12. The $j$-translation in the internal language
  13. Relationship to the associated subtopos
  14. A translation with an internal subposet of local operators
  15. Lop-frame
  16. ...and 15 more sections

Key Result

Lemma 3.3

Let $\varphi[\vec{x}]$ be an $\mathcal{L}_{\mathcal{E}}$-formula. The following implications hold.

Theorems & Definitions (92)

  • Definition 3.1
  • Remark 3.2
  • Lemma 3.3
  • Definition 3.4: $\mathcal{L}_{X}$-formula
  • Definition 3.5
  • Definition 3.6
  • Example 3.7
  • Example 3.8
  • Lemma 3.9
  • Proposition 3.10
  • ...and 82 more