Skip to main content
added 550 characters in body
Source Link
Andrej Bauer
  • 48.8k
  • 11
  • 131
  • 239

Let $\Omega_{\neg\neg} = \{p \in \Omega \mid \neg\neg p \Rightarrow p\}$ be the object of $\neg\neg$-stable truth values, and let us write $P_{\neg\neg}(A) = {\Omega_{\neg\neg}}^A$ for the object of $\neg\neg$-stable subobjects of $A$. Observe that $\Omega_{\neg\neg}$ is a complete Boolean algebra, and this fact can be shown in the internal logic of a topos.

Now, it seems to me that one can build a model of $\mathsf{PA}_\infty$$\mathsf{PA}_n$ for each $n$, by interpreting its logic in $\Omega_{\neg\neg}$, and the (higher-order) predicates as elements of the iterates of the $\neg\neg$-powersets ${P_{\neg\neg}}^k(\mathbb{N})$.

Supplemental: I initially claimed we can have a model of $\mathsf{PA}_\infty$, but Paul pointed out I was overstating the case. Indeed, to have a model of $\mathsf{PA}_\infty$ we would need a single object that encompasses all finite iterates $\neg\neg$-powersets ${P_{\neg\neg}}^k(\mathbb{N})$ at once, says something like $\coprod_{n \in \mathbb{N}} {P_{\neg\neg}}^k(\mathbb{N})$. However, in an elementary topos such an object need not exist. A counter-model is the set $V_{\omega + \omega}$ of sets of rank below $\omega + \omega$.

Let $\Omega_{\neg\neg} = \{p \in \Omega \mid \neg\neg p \Rightarrow p\}$ be the object of $\neg\neg$-stable truth values, and let us write $P_{\neg\neg}(A) = {\Omega_{\neg\neg}}^A$ for the object of $\neg\neg$-stable subobjects of $A$. Observe that $\Omega_{\neg\neg}$ is a complete Boolean algebra, and this fact can be shown in the internal logic of a topos.

Now, it seems to me that one can build a model of $\mathsf{PA}_\infty$ by interpreting its logic in $\Omega_{\neg\neg}$, and the (higher-order) predicates as elements of the iterates of the $\neg\neg$-powersets ${P_{\neg\neg}}^k(\mathbb{N})$.

Let $\Omega_{\neg\neg} = \{p \in \Omega \mid \neg\neg p \Rightarrow p\}$ be the object of $\neg\neg$-stable truth values, and let us write $P_{\neg\neg}(A) = {\Omega_{\neg\neg}}^A$ for the object of $\neg\neg$-stable subobjects of $A$. Observe that $\Omega_{\neg\neg}$ is a complete Boolean algebra, and this fact can be shown in the internal logic of a topos.

Now, it seems to me that one can build a model of $\mathsf{PA}_n$ for each $n$, by interpreting its logic in $\Omega_{\neg\neg}$, and the (higher-order) predicates as elements of the iterates of the $\neg\neg$-powersets ${P_{\neg\neg}}^k(\mathbb{N})$.

Supplemental: I initially claimed we can have a model of $\mathsf{PA}_\infty$, but Paul pointed out I was overstating the case. Indeed, to have a model of $\mathsf{PA}_\infty$ we would need a single object that encompasses all finite iterates $\neg\neg$-powersets ${P_{\neg\neg}}^k(\mathbb{N})$ at once, says something like $\coprod_{n \in \mathbb{N}} {P_{\neg\neg}}^k(\mathbb{N})$. However, in an elementary topos such an object need not exist. A counter-model is the set $V_{\omega + \omega}$ of sets of rank below $\omega + \omega$.

Source Link
Andrej Bauer
  • 48.8k
  • 11
  • 131
  • 239

Let $\Omega_{\neg\neg} = \{p \in \Omega \mid \neg\neg p \Rightarrow p\}$ be the object of $\neg\neg$-stable truth values, and let us write $P_{\neg\neg}(A) = {\Omega_{\neg\neg}}^A$ for the object of $\neg\neg$-stable subobjects of $A$. Observe that $\Omega_{\neg\neg}$ is a complete Boolean algebra, and this fact can be shown in the internal logic of a topos.

Now, it seems to me that one can build a model of $\mathsf{PA}_\infty$ by interpreting its logic in $\Omega_{\neg\neg}$, and the (higher-order) predicates as elements of the iterates of the $\neg\neg$-powersets ${P_{\neg\neg}}^k(\mathbb{N})$.