Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorYimingXu
   • CommentTimeDec 9th 2020
   • (edited Dec 11th 2020)
   • PermaLink
   Author: YimingXu
   Format: MarkdownItexIt is well-known that we can do proof by induction in a topos using the natural number object, I am interested in proving the strong induction principle, and I am attempting to translate this proof here https://math.ou.edu/~nbrady/teaching/f14-2513/LeastPrinciple.pdf ( (I) $\to$ (SI) ) into an abstract version, so it works for the natural number object in a category satisfies ETCS (In particular, the topos satisfies well-foundedness, and every subobject has complement, therefore, this is a Boolean topos). The $\le$ relation is given as the pullback of $o: 1\to N$, as the element $0$ of natural number, along the map truncated subtraction $-: N\times N \to N$, as in Sketch of an elephant by Johnstone (page 114, A2.5). I think the statement of strong induction to prove is as the following. For a subobject $p: P \to N$, if for an arbitary element $n: 1 \to N$ of the NNO, "all member $n_0: 1\to N$ such that $- \circ \langle n_0, n\rangle = o$ factorises through $P$" implies "$s \circ n: 1 \to N \to N$ factors through P", then $P\cong N$. I am not sure what to do with the $Q$ though, and I am not sure if constructing such a $Q$ need the comprehension axiom for ETCS, and hence have trouble translating the proof in the link to also work for NNO. I think if we translate the proof, then we should reduce the task of $P\cong N$ into the task of proving $Q \cong N$. I am now asking about how to construct such a $Q$, which corresponds to the predicate $Q$ in the link. Any help, please? p.s. The problem that I am actually interested in is proving the well-foundedness of natural number object (explicitly, every non-empty set has a minimal element), but the "material set theoretic proof" using strong induction. Therefore I think I should get strong induction principle for NNO. It will also be great if we can directly prove the well-ordered principle for NNO. (Have searched online for well-orderedness and strong induction for NNO, but nothing helpful is found. Is there any material to read about them?)

   It is well-known that we can do proof by induction in a topos using the natural number object, I am interested in proving the strong induction principle, and I am attempting to translate this proof here https://math.ou.edu/~nbrady/teaching/f14-2513/LeastPrinciple.pdf ( (I) $\to$ (SI) ) into an abstract version, so it works for the natural number object in a category satisfies ETCS (In particular, the topos satisfies well-foundedness, and every subobject has complement, therefore, this is a Boolean topos).

   The $\le$ relation is given as the pullback of $o: 1\to N$, as the element $0$ of natural number, along the map truncated subtraction $-: N\times N \to N$, as in Sketch of an elephant by Johnstone (page 114, A2.5).

   I think the statement of strong induction to prove is as the following.

   For a subobject $p: P \to N$, if for an arbitary element $n: 1 \to N$ of the NNO, “all member $n_0: 1\to N$ such that $- \circ \langle n_0, n\rangle = o$ factorises through $P$” implies “$s \circ n: 1 \to N \to N$ factors through P”, then $P\cong N$.

   I am not sure what to do with the $Q$ though, and I am not sure if constructing such a $Q$ need the comprehension axiom for ETCS, and hence have trouble translating the proof in the link to also work for NNO. I think if we translate the proof, then we should reduce the task of $P\cong N$ into the task of proving $Q \cong N$. I am now asking about how to construct such a $Q$, which corresponds to the predicate $Q$ in the link. Any help, please?

   p.s. The problem that I am actually interested in is proving the well-foundedness of natural number object (explicitly, every non-empty set has a minimal element), but the “material set theoretic proof” using strong induction. Therefore I think I should get strong induction principle for NNO. It will also be great if we can directly prove the well-ordered principle for NNO. (Have searched online for well-orderedness and strong induction for NNO, but nothing helpful is found. Is there any material to read about them?)

2. • CommentRowNumber2.
   • CommentAuthormartinescardo
   • CommentTimeDec 10th 2020
   • (edited Dec 10th 2020)
   • PermaLink
   Author: martinescardo
   Format: MarkdownItexStrong induction (or course-of-values induction) holds in any elementary topos with NNO. However, the "p.s." problem doesn't, because if every non-empty set of natural numbers had a least element, then excluded middle would hold, but excluded middle holds only in boolean toposes. To see this, consider an arbitrary proposition P, and the set consisting of the natural numbers n such that n is 0 and P holds, or n is 1 and P fails. This set is non-empty, because if it were empty then both P and "not P" would fail, which is impossible (from "not P" and "not not P" we get a contradiction). If this set has a least element, then it is either zero or it isn't, because the natural numbers have decidable equality. If it is zero, then P holds. If it isn't, then P fails. Hence P is decidable for arbitrary P, which means that excluded middle holds if every non-empty set of natural numbers has a least element.

   Strong induction (or course-of-values induction) holds in any elementary topos with NNO. However, the “p.s.” problem doesn’t, because if every non-empty set of natural numbers had a least element, then excluded middle would hold, but excluded middle holds only in boolean toposes. To see this, consider an arbitrary proposition P, and the set consisting of the natural numbers n such that n is 0 and P holds, or n is 1 and P fails. This set is non-empty, because if it were empty then both P and “not P” would fail, which is impossible (from “not P” and “not not P” we get a contradiction). If this set has a least element, then it is either zero or it isn’t, because the natural numbers have decidable equality. If it is zero, then P holds. If it isn’t, then P fails. Hence P is decidable for arbitrary P, which means that excluded middle holds if every non-empty set of natural numbers has a least element.

3. • CommentRowNumber3.
   • CommentAuthorYimingXu
   • CommentTimeDec 11th 2020
   • (edited Dec 13th 2020)
   • PermaLink
   Author: YimingXu
   Format: MarkdownItexThanks for replying! 1.Therefore, does well-foundedness hold if we are working in a boolean topos? There is an ETCS axiom saying that the topos we have is well-pointed, therefore, by sheaves in geometry and logic proposition 7 on chapter 6 (A well-pointed topos E is both two-valued and Boolean), we do have a boolean topos. In particular, any subobject has a complement. The axioms can be viewed in this document http://www.tac.mta.ca/tac/reprints/articles/11/tr11.pdf . 2. It is great to hear strong induction holds. May I please ask for a proof of it, or just some hint from the place I am stucked on?

   Thanks for replying!

   1.Therefore, does well-foundedness hold if we are working in a boolean topos? There is an ETCS axiom saying that the topos we have is well-pointed, therefore, by sheaves in geometry and logic proposition 7 on chapter 6 (A well-pointed topos E is both two-valued and Boolean), we do have a boolean topos. In particular, any subobject has a complement. The axioms can be viewed in this document http://www.tac.mta.ca/tac/reprints/articles/11/tr11.pdf .

   1. It is great to hear strong induction holds. May I please ask for a proof of it, or just some hint from the place I am stucked on?
4. • CommentRowNumber4.
   • CommentAuthorDavidRoberts
   • CommentTimeDec 11th 2020
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItexMy understanding is that in a constructive setting, one uses axioms that give induction directly, rather than classical well-foundedness then proving induction theorems. Just like the definition of constructive ordinals is not "every nonempty set has a least element" (and, of course, the natural numbers are an ordinal, classically, though I'm not sure about constructively)

   My understanding is that in a constructive setting, one uses axioms that give induction directly, rather than classical well-foundedness then proving induction theorems. Just like the definition of constructive ordinals is not “every nonempty set has a least element” (and, of course, the natural numbers are an ordinal, classically, though I’m not sure about constructively)

5. • CommentRowNumber5.
   • CommentAuthorYimingXu
   • CommentTimeDec 11th 2020
   • (edited Dec 11th 2020)
   • PermaLink
   Author: YimingXu
   Format: MarkdownItexThanks for commenting! It is good to know that these things should be axioms if we want to do it constructively. I am not such ambitious that want to prove this principle constructively though :-) . Things are tricker if the topos is not Boolean, but I am now only working within a category satisfies the axioms in Lawvere's axioms, so our life is easier! We can use excluded middle for the proof, as well as well-pointedness. I will edit the question to make it clearer.

   Thanks for commenting! It is good to know that these things should be axioms if we want to do it constructively. I am not such ambitious that want to prove this principle constructively though :-) . Things are tricker if the topos is not Boolean, but I am now only working within a category satisfies the axioms in Lawvere’s axioms, so our life is easier! We can use excluded middle for the proof, as well as well-pointedness. I will edit the question to make it clearer.

6. • CommentRowNumber6.
   • CommentAuthormartinescardo
   • CommentTimeDec 11th 2020
   • (edited Dec 11th 2020)
   • PermaLink
   Author: martinescardo
   Format: MarkdownItexThis proof of strong induction https://proofwiki.org/wiki/Second_Principle_of_Mathematical_Induction can be adapted to (the internal language of) any elementary topos.

   This proof of strong induction https://proofwiki.org/wiki/Second_Principle_of_Mathematical_Induction can be adapted to (the internal language of) any elementary topos.

7. • CommentRowNumber7.
   • CommentAuthormartinescardo
   • CommentTimeDec 11th 2020
   • (edited Dec 11th 2020)
   • PermaLink
   Author: martinescardo
   Format: MarkdownItexIf you want to avoid excluded middle, you can prove in the internal language of any elementary topos with NNO that every decidable, inhabited subset of the natural numbers has a least element. From this constructive result, excluded middle immediately implies the result you want, because (1) by excluded middle, every non-empty subset is inhabited, and (2) by excluded middle, every subset is decidable. The constructive result is easy: we use the assumed inhabitant as a bound for trying each natural number at a time until we reach the bound, answering the first natural number we find in this process. Making this argument formal can give you headaches. I don't have such a formal argument written down in the internal language of a topos, but I do have it in the closely related language of Martin-Loef type theory, expressed in Agda notation. It is [here](https://www.cs.bham.ac.uk/~mhe/TypeTopology/NaturalsOrder.html#9447) if you want to see it, where a decidable subset is called detachable. But I don't expect this to be understandable without training in MLTT and Agda. In any case, the formal argument is straightforward but laborious, and this is what I want to indicate by providing this link, with emphasis on "laborious".

   If you want to avoid excluded middle, you can prove in the internal language of any elementary topos with NNO that every decidable, inhabited subset of the natural numbers has a least element. From this constructive result, excluded middle immediately implies the result you want, because (1) by excluded middle, every non-empty subset is inhabited, and (2) by excluded middle, every subset is decidable. The constructive result is easy: we use the assumed inhabitant as a bound for trying each natural number at a time until we reach the bound, answering the first natural number we find in this process. Making this argument formal can give you headaches. I don’t have such a formal argument written down in the internal language of a topos, but I do have it in the closely related language of Martin-Loef type theory, expressed in Agda notation. It is here if you want to see it, where a decidable subset is called detachable. But I don’t expect this to be understandable without training in MLTT and Agda. In any case, the formal argument is straightforward but laborious, and this is what I want to indicate by providing this link, with emphasis on “laborious”.

8. • CommentRowNumber8.
   • CommentAuthorYimingXu
   • CommentTimeDec 12th 2020
   • (edited Dec 12th 2020)
   • PermaLink
   Author: YimingXu
   Format: MarkdownItexThank you for outlining this hint! I have received training in HoTT and other theorem provers (HOL4 and Lean), so the code basically makes sense to me. I will try to work out if I can prove the result in the internal lauguage (hopefully this is not too far away from a "translation"), and post here if I can get it.

   Thank you for outlining this hint! I have received training in HoTT and other theorem provers (HOL4 and Lean), so the code basically makes sense to me. I will try to work out if I can prove the result in the internal lauguage (hopefully this is not too far away from a “translation”), and post here if I can get it.

9. • CommentRowNumber9.
   • CommentAuthormartinescardo
   • CommentTimeDec 13th 2020
   • PermaLink
   Author: martinescardo
   Format: MarkdownItexIn that case, if you are familiar with HoTT, in the same file I linked above there is a constructive proof that the natural numbers are well-founded, as you probably noticed, which amounts to strong induction.

   In that case, if you are familiar with HoTT, in the same file I linked above there is a constructive proof that the natural numbers are well-founded, as you probably noticed, which amounts to strong induction.