5
$\begingroup$

Is there a model of Intuitionistic Higher-Order Logic in which the following axiom is true?

Covering Axiom: Any true statement of the form $\forall x \in A, \exists y \in B, \phi(x,y)$ gives rise to an open covering of $A$, and a continuous mapping from each set in the covering to $B$, such that $\phi(x,f(x))$ is true.

I understand that there are difficulties finding "nice enough" categories of topological spaces that behaves like toposes.

The motivation for the axiom above is that it contradicts Weak Countable Choice, and seems to suggest that the set $[0,1]\subset\mathbb R$ may be "weakly countable" under it. By weakly countable, I mean the negation of uncountable.

It isn't shown below, but I have a way of extending the argument from $[0,1]$ to $\mathbb R$.

enter image description here

Improve this question
$\endgroup$
8
  • $\begingroup$ The axiom feels like it's missing half a sentence. Is there any supposed relation between the $\forall\exists$ statement and the continuous functions? Perhaps that the pair $(a,f(a))$ satisfies the statement? $\endgroup$
    – Wojowu
    Nov 26, 2019 at 12:40
  • $\begingroup$ @Wojowu Any true statement of the form $\forall x \in A, \exists y \in B, \phi(x,y)$ gives rise to an open covering of $A$, and a continuous mapping from each set in the covering to $B$, such that $\phi(x,f(x))$ is true. I'm not sure if that's clearer... $\endgroup$
    – wlad
    Nov 26, 2019 at 12:41
  • $\begingroup$ It definitely is clearer, since now you indicate the relation between the two! $\endgroup$
    – Wojowu
    Nov 26, 2019 at 12:42
  • $\begingroup$ @Wojowu I've added the clarification $\endgroup$
    – wlad
    Nov 26, 2019 at 13:01
  • 2
    $\begingroup$ It's known that the reals are "weakly countable" in the topos of sheaves over the real numbers (see the appendix of cs.au.dk/~spitters/obs.pdf ). I imagine an argument similar to the one you gave works in the internal logic, but there are a few things to check. E.g. defining compact in terms of finite subcovers is usually too strong constructively and countable products of compact spaces aren't always compact. Also, the statement of the covering axiom seems very strong because it's stated for arbitrary topological spaces. $\endgroup$
    – aws
    Nov 26, 2019 at 19:24

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.