Good!

@F.Zer: So you can proceed now. To summarize, we chose minimum x∈ℕ such that k·x ≥ m, and let r∈ℕ such that k·x = m+r, and used minimality of x to show that r < k, since otherwise k·x ≥ m+k and so k·x' ≥ m where x'∈ℕ and x'+1 = x. This is a very typical usage of well-ordering to decompose things in number theory.

Great.

Also, the goal, which is to find x,r∈ℕ such that k·x = m+r where 0 ≤ r < k, is itself a typical instance of the canonicalization technique. In this case, we are finding the closest multiple of k that is at least m, where "the" is justified because it exists (by well-ordering) and is unique. Why do I consider this a canonicalization? Because we are basically decomposing m in a determinate manner into a big and small piece.

It is similar to decimal representation, where we represent each natural number as sum of powers of 10, using as big powers as possible.

What you just proved is a very very simple representation, like only having tens and ones.

Analogously with decimals, where the number of ones is from 0 to less than 10, due to taking out as many tens as possible, in your case r is from 0 to less than k.

I'll think about this. Thank you.

@F.Zer: So you can continue with the rest of that proof. The above explanation is just to explain why we want to do what I did to begin with.

Good.

@user21820, So, I will appreciate if you can answer a couple of questions: do you assign meaning to a statement like k·x = m+r to better recall it ? Do you keep a separate sheet with only derived statements ? As an aside, I noticed that knowing x was the minimum was an aid for me; but what happens with k, m and r ? How do you keep track of what's being said about them ? Do those entities mean something for you or perhaps you developed an intuitive sense when manipulating them ?

@F.Zer Good question. Concerning state in a proof, if you truly work within the proof, at the indented level, you won't lose track of the governing contexts, because it's simply impossible.

But concerning remembering what every variable is for, it's both syntactic and semantic. When dealing with number theory, of course you shouldn't aim to design proofs without using any techniques. That's why I mentioned the canonicalization technique, which tells you to use well-ordering in that particular manner.

When you view x,r as related to k,m via that notion of canonical representation (of m in relation to copies of k plus a remainder), you won't easily forget what x (number of copies) and r (remainder) stand for.

@user21820 Oh, thank you. I ask because you previously pointed out that I'd missed the restriction on k,m being coprime. In that particular case, I was looking at my proof and that particular restriction was "above my screen", so I couldn't see it. It would be good to see (at a glance) every line in the current context (and governing contexts). But sometimes that context is long and doesn't fit in the screen. Any advice regarding that ? Not sure I've explained myself.

@F.Zer I don't have any advice for that. I use a small enough font size so that I have 35 lines on my screen, and typically that's enough for me.

Oh, interesting. I counted them and I have 24 lines in my screen. I will experiment using a smaller font.

@user21820 When you say: "Also, the goal, which is to find x,r∈ℕ such that k·x = m+r where 0 ≤ r < k, is itself a typical instance of the canonicalization technique." The canonicalization techinque was explained by you: "means to restrict your attention to some kind of canonical form that you can reduce every other case to". Where does "0 ≤ r < k" fit in this concept and how did you find it ?

Or, perhaps you are using that technique in a different way, here ?

@F.Zer There are many ways you can express a number as a sum.

One way is base representation, such as decimal.

But even simpler than that, and actually the underlying mechanism for base representation, is of the sort you just proved.

@user21820 Very nice.

See how it corresponds to decimal, in that you can express m as a sum of copies of tens plus ones. There are many ways you can do it, but a canonical way is to ask for the number of tens being as large as possible, which forces the number of ones to be from 0 to less than 10.

In this case, we aren't writing m as a sum of k·x plus r. However, we are writing k·x = m+r, which is nearly the same, just "on the other side".

Starting to understand, I think.

You can do the same thing with decimal. 13 can be written as 10·2−7, instead of 10·1+3.

@user21820 So, I can express 5 as 2+3. That is one way of representing 5. Are you simply choosing a form that helps you in the proof ?

It seems the ability of rewriting an expression is very important, here. And choosing one that helps. Is that right ?

@F.Zer Yes, that's precisely the point. Taking away the closest multiple of k from m (from one side) is to canonicalize m to make its 'form' closer to the desired conclusion.

You want k·x = m·y+1. If k < m (the case we are in now), then k·1 might be very far from m so you can't hope to get close to m·y+1.

So the closest we can get in one intuitive step is to get the closest multiple of k to m.

And see what's left.

Good. I understand more, now. So, I missed one thing. Could you back up a bit how we found the closest multiple of k to m ? Is the expression "Let x ∈ ℕ be the minimum such that k·x ≥ m" representing that ?

@F.Zer Yes that is the formal method. The intuition is simply "I want the closest multiple. Now how can I get it using well-ordering?"

@user21820 Excellent.

I'll continue with the proof.

r < k.
r < m.
k+r < k+m = n.
Q(r+k).
r+k = r+k ⇒ ( k > 1 ∧ ¬∃d∈ℕ ( d > 1 ∧ d | r ∧ d | k ) ⇒ ∃x,y∈ℕ ( r·x = k·y+1 ) )
r+k = r+k
k > 1 ∧ ¬∃d∈ℕ ( d > 1 ∧ d | r ∧ d | k ) ⇒ ∃x,y∈ℕ ( r·x = k·y+1 )
If ∃d∈ℕ ( d > 1 ∧ d | r ∧ d | k ):
	...
	⊥
¬∃d∈ℕ ( d > 1 ∧ d | r ∧ d | k ).
If k = 1:
	...

@user21820, so I am assuming r and k are coprime.

Are not coprime. That was a typo.

@F.Zer: I don't know what you're doing. It doesn't look like you're working within the outline I gave you.

@user21820 Yes, I am filling the dots. I expanded the definition of Q(r + k).

And instantiated the universal with r,k ∈ ℕ

Does that make sense ?

I see. Well, I always put "..." for what you need to fill in to obtain what comes after.

So the next goal is supposed to be "¬∃d∈ℕ ( d > 1 ∧ d | r ∧ d | k )".

You will of course use Q(r+k), but not now.

Thank you. I see what you mean.

In particular, "Let p,q∈ℕ such that r·p = k·q+1." later comes from Q(r+k) and other lines that I have explicitly written down, including "¬∃d∈ℕ ( d > 1 ∧ d | r ∧ d | k )".

That's also the reason for the case-split.

r < k.
r < m.
k+r < k+m = n.
Q(r+k).
If ∃d∈ℕ ( d > 1 ∧ d | r ∧ d | k ):
	Let d' ∈ ℕ such that d' > 1 ∧ d' | r ∧ d' | k
	...
¬∃d∈ℕ ( d > 1 ∧ d | r ∧ d | k ).

@user21820 Which case split ?

@F.Zer Right, and it shouldn't be hard to fill it in.

@F.Zer Why did you think there was "If k > 1:"? Because of what Q(r+k) wants.

@user21820 Yes, thank you. Fortunately, in one of my earlier drafts I wrote "If k = 1:" without looking at your outline :-)

@user21820 Isn't k > 1 the end goal ?

Aren't you trying to prove it ?

That's why I am assuming "If k = 1:" and reaching a contradiction. To derive k > 1 from "k ≥ 1" and "k ≠ 1".

@F.Zer Yes, but that doesn't contradict what I said. You earlier complained that you have no idea where all my steps come from. I just gave an explanation of why I did "If k > 1:", which is because I cannot use Q(r+k) without having that, and that forces me to do a case-split to handle the other case, which is "If k = 1:".

I don't claim that my approach is the best, but it's the most well-motivated I could find. I know a dozen ways to prove this theorem, but the really simplest one to me is actually not formalizable in PA, so I can't use it.

@user21820 Oh, I see. Thank you. I saw you did two assumptions, using trichotomy, and discarding the case "If k < 1"; namely "If k = 1:" and "If k > 1:". I did only one: "If k = 1" and with that derived "k > 1". Does this make sense ?

Well, actually I haven't reached a contradiction, yet.

That's my goal.

@F.Zer Both ways are fine. I prefer not to invoke contradiction explicitly if it's not needed, since it makes the proof less constructive.

@user21820 Got it.

So if you look carefully at the proof outline, everything is well-motivated (by some later-stated goal), except for why we believe Q(r+k) is useful under "If k < m:" and same for Q(r+m) under "If k > m:". Canonicalization motivates these two cases as well as the well-ordering, but doesn't tell us which Q(...) would be useful. It doesn't even tell us that this kind of (strong) induction would even work.

It turns out that it works, but that's a phenomenon specific to this theorem.

I see.

Oh, very interesting.

But it would be no surprise if you can't see why it would work, even if you can see that the proof is correct after you're done with it.

I see that information coming from "outside" the proof can be useful. Like what you showed me when proving statements involving triangles.

Using a picture, etc...

Of course, then it would be necessary to formalise that proof.

But the intuition gained could be useful.

@F.Zer I can sketch the other proof for you. It starts from wanting to compute gcd(x,y), defined as greatest common divisor. You can actually express "gcd(x,y) = d" in an FOL statement in the language of PA (feel free to try it). You can prove that gcd(x,x+y) = gcd(x,y) for every x,y∈ℕ. This allows computing gcd by repeatedly subtracting the smaller from the bigger. By induction, this must terminate because the sum gets smaller on each step (this is also why I used strong induction on k+m).

The termination condition is when one of them becomes 0.

function gcd(x,y) { if( x<y ) return gcd(y,x); if( y==0 ) return x; return gcd(x-y,x); }

The above shows that this procedure terminates on all input x,y∈ℕ, and returns the (actual) gcd(x,y).

I'll give a shot.

Wait, I'm not done.

And I'm not asking you to write a formal proof, because as I said it cannot be formalized in PA. After all, you can't talk about procedures.

If x,y are nonzero and gcd(x,y) = 1, then we can analyze what happened in the recursion. Every procedure call is on inputs each of which is a linear combination of x,y. This can be proven by induction. Observe that gcd(x,y) returns one of the inputs of some procedure call in the recursion, which must be a linear combination of x,y and must also be 1. Therefore x·p−y·q = 1 for some integers p,q.

In my opinion, this explanation is the true reason why (PA5) is true. Of course, the statement of (PA5) is slightly adjusted so that it stays within ℕ.

Anyway, I got to go.

Good. I'll look into it. Now, for the other proof:

@user21820 I leave that there.

I forgot to say r = d'·a and k = d'·b for some a,b ∈ ℕ.

@user21820, see you !

@F.Zer Yes that's the idea. If b | k,r then b | m, and you just have to (like before) simulate the subtraction within PA.

@user21820 Yes, I see. Thank you. I will formalise that into PA.

Since d' divides both k and r and the equality k·x = m + r holds, then d' divides m.

@user21820, I think I've found the proof. What do you think ?

If ∃d∈ℕ ( d > 1 ∧ d | r ∧ d | k ):
	Let d' ∈ ℕ such that d' > 1 ∧ d' | r ∧ d' | k
	Let a ∈ ℕ such that r = d'·a
	Let b ∈ ℕ such that k = d'·b
	[Rewrite d'·(b·x - a) = m within PA]
	If a ≥ b·x:
		d'·a ≥ d'·(b·x)
		d'·a ≥ (d'·b)·x
		r ≥ k·x
		⊥
	a < b·x
	∀x,y∈ℕ ( x≤y ⇒ ∃z∈ℕ ( x+z = y ) ) [Lemma]
	a + z' = b·x
	k·x = m + r
	(d'·b)·x = m + d'·a
	d'·(b·x) = m + d'·a
	d'·(a + z') = m + d'·a
	d'·a + d'·z' = m + d'·a
	d'·z' = m
	d' | m
	d' > 1 ∧ d' | k ∧ d' | m
	∃d∈ℕ ( d > 1 ∧ d | k ∧ d | m )
	⊥
¬∃d∈ℕ ( d > 1 ∧ d | r ∧ d | k ).