Skip to main content
4 of 4
Fix a misspelling
Hanul Jeon
  • 3.1k
  • 2
  • 14
  • 44

This is not a full answer, but I think it is worth to mention: we can prove the theory CZF + Full separation + ¬Double complement is consistent!

The proof goes as follows: consider the Lubarsky's first model in 1. Let $\check{0}(\kappa)=\varnothing$ and $\check{1}(\kappa) = \{\check{0}\upharpoonright (\mathrm{On}\setminus\kappa)\}$. They will behave as 0 and 1 of the model. Furthermore, for each ordinal $\kappa$ define $$\check{1}_\kappa (\lambda ) = \begin{cases}\varnothing & \text{if }\kappa<\lambda\text{ and} \\ \{\check{0}\upharpoonright (\mathrm{On}\setminus\lambda)\} & \text{otherwise.}\end{cases}$$

I will claim that the element $x\in M_0$, defined by $x(\nu)=\{\check{1}\upharpoonright (\mathrm{On}\setminus\nu)\}$ for every ordinal $\nu$, has no double complement. First, it is tedious to check

$$\kappa \vDash \lnot\lnot (\check{1}_\nu \in x) \iff \forall \lambda \ge \kappa \exists \mu\ge\lambda : \mu\models \check{1}_\nu \in x$$ and the later statement holds: take any $\mu>\max(\lambda, \nu)$. Hence if $y\in M_0$ is a double complement of $x$, then it must contain every $\check{1}_\nu$, which is impossible. (In fact, we need to prove any $y\in M_\xi$ for any $\xi$ cannot be a double complement of $x$. However, its proof is not too different from my proof.)

However, my proof (if correct) has some unsatisfactory points. First, it requires the consistency of ZFC. Lubarsky proved that CZF + Full separation is equiconsistent with the second-order arithmetic [2]. I wonder CZF + Full separation + ¬Double complement is equiconsistent with Second order arithmetic. Kripke models seems not adequate to derive such kind of equiconsistency result (unless we form a Kripke model of CZF over CZF.) Second, it does not settle my original question: what happenes if we assume the axiom of power set?


(Added in Jan 24, 2019) I found that V. H. Hahanyan makes a bunch of result on the axiom of double complement over IZF (example). But most of his article is written in Russian so it is not easily accessible to me.


References

(1) Lubarsky, Robert S. "Independence results around constructive ZF." Annals of Pure and Applied Logic 132.2-3 (2005): 209-225.

(2) Lubarsky, Robert S. "CZF and Second Order Arithmetic ." Annals of Pure and Applied Logic 141.1-2 (2006): 29-34.

Hanul Jeon
  • 3.1k
  • 2
  • 14
  • 44