On Jun 22, 12:51 am, Jan Burse <janbu...@fastmail.fm> wrote: > > Sort of. Let me try and write the proof for the Euclid theorem I > > wrote in my original post. Do you know where I can find a natural > > language version of the proof? I lost my original source. > > Depends where you begin, how do you see natural numbers? > Peano? Or is it a more general result in algebra?
Well I guess we can assume that in the "number_theory" module we will have the usual primitive results of: - integer addition - integer subtraction - integer multiplication - even/odd - relatively prime - gcd - etc
plus I guess "number_theory" might be using other modules that give us more basic classical first-order logic, set theory and the Peano axioms.
If I could get a sketch of the proof for the theorem using any of the above in natural language that would be great. Once I see how the proof works, and what it depends on, I will have a better idea where to put stuff. -Andrew.