0

Is there a constructive proof of the division algorithm that doesn't invoke the well ordering principle?

apricity
  • 101
  • 2
  • You mean for integers? – Zelos Malum Nov 21 '15 at 05:40
  • @Zelos Malum Yes, for integers. – apricity Nov 21 '15 at 05:42
  • 1
    To show that for any $b\ge 0$ and $a\gt 0$ there is a $q$ and $r$ such that $\dots$, do an induction on $b$. Very constructive, albeit a slow construction. – André Nicolas Nov 21 '15 at 06:08
  • 1
    It depends on what you mean by not using the well-ordering principle. Does using induction count? If so, there's basically nothing you can prove about the integers without using induction. (Related question: are you more interested in the "constructive" part or in the "not using well-ordering" part?) – Qiaochu Yuan Nov 21 '15 at 06:09
  • My curiosity began with "Oh, WOP is nonconstructive, I wonder if I can get rid of it" So I'm more interested in a constructive proof than just getting rid of WOP. Most constructivists allow proof by induction, no? – apricity Nov 22 '15 at 00:06

0 Answers0