Skip to main content
edited body
Source Link
Andrej Bauer
  • 48.8k
  • 11
  • 131
  • 239

Let us call an object $A$ infinite if there is a monomorphism $\mathbb{N} \to A$. Your question then asks whether $A$ or $B$ must be infinite in order for $A \times B$ to be infinite.

From now on we argue in the internal language of a topos. I am going to show that the Lesser Limited Principle of Omniscience (LLPO), which does not hold in all toposes and is a particular instance of the Law of excluded middle, follows from the statement

For all subobjects $A, B \subseteq \mathbb{N}$, if $A \times B$ is infinite then $A$ or $B$ is infinite.

LLPO can be stated as follows: given two infinite binary sequences such that not both of them contain a 1, then one or the other does not contain a 1.

So assume the statement and suppose $f, g : \mathbb{N} \to \lbrace 0, 1 \rbrace$ are sequences as in the premise of LLPO. Define the sets $A$ and $B$ by $$A = \lbrace n \in \mathbb{N} \mid \forall k < n . f(k) = 0 \rbrace$$ and $$B = \lbrace n \in \mathbb{N} \mid \forall k < n . g(k) = 0 \rbrace$$ We claim that $A \times B$ is infinite. Define the sequences $a : \mathbb{N} \to A$ and $b : \mathbb{N} \to B$ by $$a_n = \begin{cases} n, & \forall k < n . f(n) = 0\\\\ k, & k < n \land f(k) = 1 \land \forall j < k . f(j) = 0 \end{cases}$$$$a_n = \begin{cases} n, & \forall k < n . f(k) = 0\\\\ k, & k < n \land f(k) = 1 \land \forall j < k . f(j) = 0 \end{cases}$$ and $$b_n = \begin{cases} n, & \forall k < n . g(n) = 0\\\\ k, & k < n \land g(k) = 1 \land \forall j < k . g(j) = 0 \end{cases}$$$$b_n = \begin{cases} n, & \forall k < n . g(k) = 0\\\\ k, & k < n \land g(k) = 1 \land \forall j < k . g(j) = 0 \end{cases}$$ Notice that $a_m = a_n$ and $m \neq n$ imply that $f(k) = 1$ for some $k \leq \min(m,n)$, and a similar observation holds for the other sequence. The sequence $n \mapsto (a_n, b_n)$ clearly takes values in $A \times B$. It is injective because $(a_m,b_m) = (a_n, b_n)$ and $m \neq n$ imply that both $f$ and $g$ contain a 1, contrary to the premise of LLPO. Therefore, $A \times B$ is infinite and by the statement $A$ or $B$ is infinite. If $A$ is infinite then $f$ does not contain a 1, and if $B$ is infinite then $g$ does not contain a 1.

In summary, the answer to your question is negative because the statement implies LLPO, which is not valid in every topos. In particular, LLPO is violated in the effective topos.

I do not know (yet) whether LLPO implies the statement.

An obvious question to ask is whether we can positively violate the statment, i.e., can we produce two non-infinite objects $A$ and $B$ such that $A \times B$ is infinite. I would search for such objects in the effective topos, where the question will take on a recursion-theoretic flavor.

Let us call an object $A$ infinite if there is a monomorphism $\mathbb{N} \to A$. Your question then asks whether $A$ or $B$ must be infinite in order for $A \times B$ to be infinite.

From now on we argue in the internal language of a topos. I am going to show that the Lesser Limited Principle of Omniscience (LLPO), which does not hold in all toposes and is a particular instance of the Law of excluded middle, follows from the statement

For all subobjects $A, B \subseteq \mathbb{N}$, if $A \times B$ is infinite then $A$ or $B$ is infinite.

LLPO can be stated as follows: given two infinite binary sequences such that not both of them contain a 1, then one or the other does not contain a 1.

So assume the statement and suppose $f, g : \mathbb{N} \to \lbrace 0, 1 \rbrace$ are sequences as in the premise of LLPO. Define the sets $A$ and $B$ by $$A = \lbrace n \in \mathbb{N} \mid \forall k < n . f(k) = 0 \rbrace$$ and $$B = \lbrace n \in \mathbb{N} \mid \forall k < n . g(k) = 0 \rbrace$$ We claim that $A \times B$ is infinite. Define the sequences $a : \mathbb{N} \to A$ and $b : \mathbb{N} \to B$ by $$a_n = \begin{cases} n, & \forall k < n . f(n) = 0\\\\ k, & k < n \land f(k) = 1 \land \forall j < k . f(j) = 0 \end{cases}$$ and $$b_n = \begin{cases} n, & \forall k < n . g(n) = 0\\\\ k, & k < n \land g(k) = 1 \land \forall j < k . g(j) = 0 \end{cases}$$ Notice that $a_m = a_n$ and $m \neq n$ imply that $f(k) = 1$ for some $k \leq \min(m,n)$, and a similar observation holds for the other sequence. The sequence $n \mapsto (a_n, b_n)$ clearly takes values in $A \times B$. It is injective because $(a_m,b_m) = (a_n, b_n)$ and $m \neq n$ imply that both $f$ and $g$ contain a 1, contrary to the premise of LLPO. Therefore, $A \times B$ is infinite and by the statement $A$ or $B$ is infinite. If $A$ is infinite then $f$ does not contain a 1, and if $B$ is infinite then $g$ does not contain a 1.

In summary, the answer to your question is negative because the statement implies LLPO, which is not valid in every topos. In particular, LLPO is violated in the effective topos.

I do not know (yet) whether LLPO implies the statement.

An obvious question to ask is whether we can positively violate the statment, i.e., can we produce two non-infinite objects $A$ and $B$ such that $A \times B$ is infinite. I would search for such objects in the effective topos, where the question will take on a recursion-theoretic flavor.

Let us call an object $A$ infinite if there is a monomorphism $\mathbb{N} \to A$. Your question then asks whether $A$ or $B$ must be infinite in order for $A \times B$ to be infinite.

From now on we argue in the internal language of a topos. I am going to show that the Lesser Limited Principle of Omniscience (LLPO), which does not hold in all toposes and is a particular instance of the Law of excluded middle, follows from the statement

For all subobjects $A, B \subseteq \mathbb{N}$, if $A \times B$ is infinite then $A$ or $B$ is infinite.

LLPO can be stated as follows: given two infinite binary sequences such that not both of them contain a 1, then one or the other does not contain a 1.

So assume the statement and suppose $f, g : \mathbb{N} \to \lbrace 0, 1 \rbrace$ are sequences as in the premise of LLPO. Define the sets $A$ and $B$ by $$A = \lbrace n \in \mathbb{N} \mid \forall k < n . f(k) = 0 \rbrace$$ and $$B = \lbrace n \in \mathbb{N} \mid \forall k < n . g(k) = 0 \rbrace$$ We claim that $A \times B$ is infinite. Define the sequences $a : \mathbb{N} \to A$ and $b : \mathbb{N} \to B$ by $$a_n = \begin{cases} n, & \forall k < n . f(k) = 0\\\\ k, & k < n \land f(k) = 1 \land \forall j < k . f(j) = 0 \end{cases}$$ and $$b_n = \begin{cases} n, & \forall k < n . g(k) = 0\\\\ k, & k < n \land g(k) = 1 \land \forall j < k . g(j) = 0 \end{cases}$$ Notice that $a_m = a_n$ and $m \neq n$ imply that $f(k) = 1$ for some $k \leq \min(m,n)$, and a similar observation holds for the other sequence. The sequence $n \mapsto (a_n, b_n)$ clearly takes values in $A \times B$. It is injective because $(a_m,b_m) = (a_n, b_n)$ and $m \neq n$ imply that both $f$ and $g$ contain a 1, contrary to the premise of LLPO. Therefore, $A \times B$ is infinite and by the statement $A$ or $B$ is infinite. If $A$ is infinite then $f$ does not contain a 1, and if $B$ is infinite then $g$ does not contain a 1.

In summary, the answer to your question is negative because the statement implies LLPO, which is not valid in every topos. In particular, LLPO is violated in the effective topos.

I do not know (yet) whether LLPO implies the statement.

An obvious question to ask is whether we can positively violate the statment, i.e., can we produce two non-infinite objects $A$ and $B$ such that $A \times B$ is infinite. I would search for such objects in the effective topos, where the question will take on a recursion-theoretic flavor.

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

Let us call an object $A$ infinite if there is a monomorphism $\mathbb{N} \to A$. Your question then asks whether $A$ or $B$ must be infinite in order for $A \times B$ to be infinite.

From now on we argue in the internal language of a topos. I am going to show that the Lesser Limited Principle of Omniscience (LLPO), which does not hold in all toposes and is a particular instance of the Law of excluded middle, follows from the statement

For all subobjects $A, B \subseteq \mathbb{N}$, if $A \times B$ is infinite then $A$ or $B$ is infinite.

LLPO can be stated as follows: given two infinite binary sequences such that not both of them contain a 1, then one or the other does not contain a 1.

So assume the statement and suppose $f, g : \mathbb{N} \to \lbrace 0, 1 \rbrace$ are sequences as in the premise of LLPO. Define the sets $A$ and $B$ by $$A = \lbrace n \in \mathbb{N} \mid \forall k < n . f(k) = 0 \rbrace$$ and $$B = \lbrace n \in \mathbb{N} \mid \forall k < n . g(k) = 0 \rbrace$$ We claim that $A \times B$ is infinite. Define the sequences $a : \mathbb{N} \to A$ and $b : \mathbb{N} \to B$ by $$a_n = \begin{cases} n, & \forall k < n . f(n) = 0\\\\ k, & k < n \land f(k) = 1 \land \forall j < k . f(j) = 0 \end{cases}$$ and $$b_n = \begin{cases} n, & \forall k < n . g(n) = 0\\\\ k, & k < n \land g(k) = 1 \land \forall j < k . g(j) = 0 \end{cases}$$ Notice that $a_m = a_n$ and $m \neq n$ imply that $f(k) = 1$ for some $k \leq \min(m,n)$, and a similar observation holds for the other sequence. The sequence $n \mapsto (a_n, b_n)$ clearly takes values in $A \times B$. It is injective because $(a_m,b_m) = (a_n, b_n)$ and $m \neq n$ imply that both $f$ and $g$ contain a 1, contrary to the premise of LLPO. Therefore, $A \times B$ is infinite and by the statement $A$ or $B$ is infinite. If $A$ is infinite then $f$ does not contain a 1, and if $B$ is infinite then $g$ does not contain a 1.

In summary, the answer to your question is negative because the statement implies LLPO, which is not valid in every topos. In particular, LLPO is violated in the effective topos.

I do not know (yet) whether LLPO implies the statement.

An obvious question to ask is whether we can positively violate the statment, i.e., can we produce two non-infinite objects $A$ and $B$ such that $A \times B$ is infinite. I would search for such objects in the effective topos, where the question will take on a recursion-theoretic flavor.