Return to Answer

Assuming the law of excluded middle internally your formulation of Zorn's lemma is equivalent to the axiom of choice by the usual argument. Now there are Boolean Grothendieck topos in which the axiom of choice fails. Hence they don't satisfies Zorn lemma either.

I think the simplest example of this is to take $G$ to be a non-discrete but pro-discrete localic/topological group (typically $G = \mathbb{Z}_p$ the group of p-addic integer) and consider $\mathcal{T}$ the topos of sets endowed with a continuous (hence smooth) action of $G$ (that is the stabilizer of each point is an open subgroup)

Assuming LEM in the base, $\mathcal{T}$ is clearly boolean (sub-object are $G$-stable subsets and set theoretic complement preserve subobject).

But $\mathcal{T}$ doesn't satisfies either internal nor external choice. For exemple for $G = \mathbb{Z}_p$ the infinite product of all the $\mathbb{Z}/p^k\mathbb{Z}$ with their canonical action is the initial object. (more generally, the product of the $G/U$ for $U$ in a fundamental system of open subgroup is empty unless $G$ is discrete).

Edit: However it should be noted that, assuming Zorn lemma in the base topos, an appropriate version of Zorn lemma is known to holds in every Localic Grothendieck topos (but the topos mentioned above is not localic of course). This is proved as Proposition D4.5.14 in Sketches of an elephant.

More precisely, one take the Zorn lemma to be the statement: "every inductie poset has a maximal element" but where "inductive" is defined as the internal statement "every chain as an upper bound". More precisely prop D4.5.14 shows that if P is an (internally) inductive poset in a localic topos, then it has an (internally) maximal element given by a global section. In particular, it proves the statement "there exists a maximal element".

One has the stronger version of the internal Zorn Lemma where the quantification over "all inductive poset" is interpreted internally using the Stack semantics, because every slice of a localic topos is localic, and we can apply D4.5.14 in each slice.

The paper by Bell linked in Peter Lumsdain comment, also prove a similar result but for an (at least in appearance) weaker version of Zorn lemma where "inductive" is taken as "every chain has a least upper bound" instead of an upper-bound. Bell explicitly says that he doesn't know how to prove the stronger version of Zorn lemma, but looking at the proof of D4.5.14 it seems to me that the whole point is that both version of Zorn lemma are constructively equivalent: given any poset the poset of chains ordered by inclusion is inductive in Bell's stronger sense, so assuming Bell's version of ZL one get a maximal chain in every poset and an upper bound for a maximal chain has to be a maximal element.

Assuming the law of excluded middle internally your formulation of Zorn's lemma is equivalent to the axiom of choice by the usual argument. Now there are Boolean Grothendieck topos in which the axiom of choice fails. Hence they don't satisfies Zorn lemma either.

I think the simplest example of this is to take $G$ to be a non-discrete but pro-discrete localic/topological group (typically $G = \mathbb{Z}_p$ the group of p-addic integer) and consider $\mathcal{T}$ the topos of sets endowed with a continuous (hence smooth) action of $G$ (that is the stabilizer of each point is an open subgroup)

Assuming LEM in the base, $\mathcal{T}$ is clearly boolean (sub-object are $G$-stable subsets and set theoretic complement preserve subobject).

But $\mathcal{T}$ doesn't satisfies either internal nor external choice. For exemple for $G = \mathbb{Z}_p$ the infinite product of all the $\mathbb{Z}/p^k\mathbb{Z}$ with their canonical action is the initial object. (more generally, the product of the $G/U$ for $U$ in a fundamental system of open subgroup is empty unless $G$ is discrete).

Edit: However it should be noted that, assuming Zorn lemma in the base topos, an appropriate version of Zorn lemma is known to holds in every Localic Grothendieck topos (but the topos mentioned above is not localic of course). This is proved as Proposition D4.5.14 in Sketches of an elephant.

More precisely, one take the Zorn lemma to be the statement: "every inductie poset has a maximal element" but where "inductive" is defined as the internal statement "every chain as an upper bound". More precisely prop D4.5.14 shows that if P is an (internally) inductive poset in a localic topos, then it has an (internally) maximal element given by a global section. In particular, it proves the internal statement "there exists a maximal element" is valid.

One also have the stronger version of the internal Zorn Lemma where the quantification over "all inductive poset" is interpreted internally using the Stack semantics, because every slice of a localic topos is localic, and we can apply D4.5.14 in each slice.

The paper by Bell linked in Peter Lumsdain comment, also prove a similar result but for an (at least in appearance) weaker version of Zorn lemma where "inductive" is taken as "every chain has a least upper bound" instead of an upper-bound. Bell explicitly says that he doesn't know how to prove the stronger version of Zorn lemma, but looking at the proof of D4.5.14 it seems to me that the whole point is that both version of Zorn lemma are constructively equivalent: given any poset the poset of chains ordered by inclusion is inductive in Bell's stronger sense, so assuming Bell's version of ZL one get a maximal chain in every poset and an upper bound for a maximal chain has to be a maximal element.

Assuming the law of excluded middle internally your formulation of Zorn's lemma is equivalent to the axiom of choice by the usual argument. Now there are Boolean Grothendieck topos in which the axiom of choice fails. Hence they don't satisfies Zorn lemma either.

I think the simplest example of this is to take $G$ to be a non-discrete but pro-discrete localic/topological group (typically $G = \mathbb{Z}_p$ the group of p-addic integer) and consider $\mathcal{T}$ the topos of sets endowed with a continuous (hence smooth) action of $G$ (that is the stabilizer of each point is an open subgroup)

Assuming LEM in the base, $\mathcal{T}$ is clearly boolean (sub-object are $G$-stable subsets and set theoretic complement preserve subobject).

But $\mathcal{T}$ doesn't satisfies either internal nor external choice. For exemple for $G = \mathbb{Z}_p$ the infinite product of all the $\mathbb{Z}/p^k\mathbb{Z}$ with their canonical action is the initial object. (more generally, the product of the $G/U$ for $U$ in a fundamental system of open subgroup is empty unless $G$ is discrete).

Edit: However it should be noted that, assuming Zorn lemma in the base topos, an appropriate version of Zorn lemma is known to holds in every Localic Grothendieck topos (but the topos mentioned above is not localic of course). This is proved as Proposition D4.5.14 in Sketches of an elephant.

More precisely, one take the Zorn lemma to be the statement: "every inductie poset has a maximal element" but where "inductive" is defined as the internal statement "every chain as an upper bound". More precisely prop D4.5.14 shows that if P is an (internally) inductive poset in a localic topos, then it has an (internally) maximal element given by a global section. In particular, it proves the statement "there exists a maximal element".

One has the stronger version of the internal Zorn Lemma where the quantification over "all inductive poset" is interpreted internally using the Stack semantics, because every slice of a localic topos is localic, and we can apply D4.5.14 in each slice.

The paper by Bell linked in Peter Lumsdain comment, also prove a similar result but for an (at least in appearance) weaker version of Zorn lemma where "inductive" is taken as "every chain has a least upper bound" instead of an upper-bound. Bell explicitly says that he doesn't know how to prove the stronger version of Zorn lemma, but looking at the proof of D4.5.14 it seems to me that the whole point is that both version of Zorn lemma are constructively equivalent: given any poset the subset of chains is inductive in Bell's stronger sense, so assuming Bell's version of ZL one get a maximal chain in every poset and an upper bound for a maximal chain has to be a maximal element.

Assuming the law of excluded middle internally your formulation of Zorn's lemma is equivalent to the axiom of choice by the usual argument. Now there are Boolean Grothendieck topos in which the axiom of choice fails. Hence they don't satisfies Zorn lemma either.

I think the simplest example of this is to take $G$ to be a non-discrete but pro-discrete localic/topological group (typically $G = \mathbb{Z}_p$ the group of p-addic integer) and consider $\mathcal{T}$ the topos of sets endowed with a continuous (hence smooth) action of $G$ (that is the stabilizer of each point is an open subgroup)

Assuming LEM in the base, $\mathcal{T}$ is clearly boolean (sub-object are $G$-stable subsets and set theoretic complement preserve subobject).

But $\mathcal{T}$ doesn't satisfies either internal nor external choice. For exemple for $G = \mathbb{Z}_p$ the infinite product of all the $\mathbb{Z}/p^k\mathbb{Z}$ with their canonical action is the initial object. (more generally, the product of the $G/U$ for $U$ in a fundamental system of open subgroup is empty unless $G$ is discrete).

Edit: However it should be noted that, assuming Zorn lemma in the base topos, an appropriate version of Zorn lemma is known to holds in every Localic Grothendieck topos (but the topos mentioned above is not localic of course). This is proved as Proposition D4.5.14 in Sketches of an elephant.

More precisely, one take the Zorn lemma to be the statement: "every inductie poset has a maximal element" but where "inductive" is defined as the internal statement "every chain as an upper bound". More precisely prop D4.5.14 shows that if P is an (internally) inductive poset in a localic topos, then it has an (internally) maximal element given by a global section. In particular, it proves the statement "there exists a maximal element".

One has the stronger version of the internal Zorn Lemma where the quantification over "all inductive poset" is interpreted internally using the Stack semantics, because every slice of a localic topos is localic, and we can apply D4.5.14 in each slice.

The paper by Bell linked in Peter Lumsdain comment, also prove a similar result but for an (at least in appearance) weaker version of Zorn lemma where "inductive" is taken as "every chain has a least upper bound" instead of an upper-bound. Bell explicitly says that he doesn't know how to prove the stronger version of Zorn lemma, but looking at the proof of D4.5.14 it seems to me that the whole point is that both version of Zorn lemma are constructively equivalent: given any poset the poset of chains ordered by inclusion is inductive in Bell's stronger sense, so assuming Bell's version of ZL one get a maximal chain in every poset and an upper bound for a maximal chain has to be a maximal element.

Assuming the law of excluded middle internally your formulation of Zorn's lemma is equivalent to the axiom of choice by the usual argument. Now there are Boolean Grothendieck topos in which the axiom of choice fails. Hence they don't satisfies Zorn lemma either.

I think the simplest example of this is to take $G$ to be a non-discrete but pro-discrete localic/topological group (typically $G = \mathbb{Z}_p$ the group of p-addic integer) and consider $\mathcal{T}$ the topos of sets endowed with a continuous (hence smooth) action of $G$ (that is the stabilizer of each point is an open subgroup)

Assuming LEM in the base, $\mathcal{T}$ is clearly boolean (sub-object are $G$-stable subsets and set theoretic complement preserve subobject).

But $\mathcal{T}$ doesn't satisfies either internal nor external choice. For exemple for $G = \mathbb{Z}_p$ the infinite product of all the $\mathbb{Z}/p^k\mathbb{Z}$ with their canonical action is the initial object. (more generally, the product of the $G/U$ for $U$ in a fundamental system of open subgroup is empty unless $G$ is discrete).

Edit: However it should be noted that, assuming Zorn lemma in the base topos, an appropriate version of Zorn lemma is known to holds in every Localic Grothendieck topos (but the topos mentioned above is not localic of course). This is proved as Proposition D4.5.14 in Sketches of an elephant.

More precisely, one take the Zorn lemma to be the statement: "every inductie poset has a maximal element" but where "inductive" is defined as the internal statement "every chain as an upper bound". More precisely prop D4.5.14 shows that if P is an (internally) inductive poset in a localic topos, then it has an (internally) maximal element given by a global section. In particular, it proves the statement "there exists a maximal element".

One has the stronger version of the internal Zorn Lemma where the quantification over "all inductive poset" is interpreted internally using the Stack semantics, because every slice of a localic topos is localic, and we can apply D4.5.14 in each slice.

The paper by Bell linked in Peter Lumsdain comment, also prove a similar version result but for an apparently weaker version of Zorn lemma where "inductive" is taken as "every chain has a least upper bound" instead of an upper-bound.

Assuming the law of excluded middle internally your formulation of Zorn's lemma is equivalent to the axiom of choice by the usual argument. Now there are Boolean Grothendieck topos in which the axiom of choice fails. Hence they don't satisfies Zorn lemma either.

I think the simplest example of this is to take $G$ to be a non-discrete but pro-discrete localic/topological group (typically $G = \mathbb{Z}_p$ the group of p-addic integer) and consider $\mathcal{T}$ the topos of sets endowed with a continuous (hence smooth) action of $G$ (that is the stabilizer of each point is an open subgroup)

Assuming LEM in the base, $\mathcal{T}$ is clearly boolean (sub-object are $G$-stable subsets and set theoretic complement preserve subobject).

But $\mathcal{T}$ doesn't satisfies either internal nor external choice. For exemple for $G = \mathbb{Z}_p$ the infinite product of all the $\mathbb{Z}/p^k\mathbb{Z}$ with their canonical action is the initial object. (more generally, the product of the $G/U$ for $U$ in a fundamental system of open subgroup is empty unless $G$ is discrete).

Edit: However it should be noted that, assuming Zorn lemma in the base topos, an appropriate version of Zorn lemma is known to holds in every Localic Grothendieck topos (but the topos mentioned above is not localic of course). This is proved as Proposition D4.5.14 in Sketches of an elephant.

More precisely, one take the Zorn lemma to be the statement: "every inductie poset has a maximal element" but where "inductive" is defined as the internal statement "every chain as an upper bound". More precisely prop D4.5.14 shows that if P is an (internally) inductive poset in a localic topos, then it has an (internally) maximal element given by a global section. In particular, it proves the statement "there exists a maximal element".

One has the stronger version of the internal Zorn Lemma where the quantification over "all inductive poset" is interpreted internally using the Stack semantics, because every slice of a localic topos is localic, and we can apply D4.5.14 in each slice.

The paper by Bell linked in Peter Lumsdain comment, also prove a similar result but for an (at least in appearance) weaker version of Zorn lemma where "inductive" is taken as "every chain has a least upper bound" instead of an upper-bound. Bell explicitly says that he doesn't know how to prove the stronger version of Zorn lemma, but looking at the proof of D4.5.14 it seems to me that the whole point is that both version of Zorn lemma are constructively equivalent: given any poset the subset of chains is inductive in Bell's stronger sense, so assuming Bell's version of ZL one get a maximal chain in every poset and an upper bound for a maximal chain has to be a maximal element.