@F.Zer I do not believe that you understand.

@F.Zer Even what you just wrote is not what you really think. You did not think, at the time you wrote that line, that "blah and blah and blah and blah implies P(3)", where each "blah" is of the form "if blah then blah".

You did not do what you are claiming you did. What truly is going on in your head? If you don't believe me, just introspect and see what you are thinking as you continue on to P(10).

@user21820 Yes, you're right. I do not understand. I am just posting my attempts, so you can see my process.

@F.Zer The problem is that you are not actually describing your thoughts. Do it until P(10) and observe your own thoughts. Don't add stuff that didn't actually pass through your head.

@user21820 Good. I'll do that.

Actually I don't understand why you can't do it. Just write down the exact words that go through your mind when you are convincing yourself. Certainly, it is not symbols, and even if the words are replaced by symbols it would be nothing like what you wrote above.

@user21820 An attempt using words: I get P(0). Then, from P(0) and P(0) ⇒ P(1) I get P(1). So, from P(0) ∧ P(1) and P(0) ∧ P(1) ⇒ P(2), I get P(2)...

Yes, which is completely different from what you wrote above.

Explain this actual pattern that went on in your head.

@user21820 Good. I'll do that.

@user21820 I see this pattern: Then, from "X and X ⇒ Y I get Y".

Uh? Again you're not faithfully describing your thoughts. Why do you keep trying to turn your original thoughts into something abstract, which ends up being different?

@user21820 Ok, so I did not understand your request. I tried to see what's the general pattern without using P(i), with i ∈ ℕ.

@F.Zer What you wrote is not even the general pattern.

That's the point. You keep trying to turn your thoughts into something else, and it turns them wrong.

@user21820 I see. Well, that's the risk of doing a translation. The original could be correct, but the translation could be wrong :-)

No it's not about translation. Take a step back and observe that all the way before this you failed to describe your actual thinking, simply because you were too eager to convert it into symbols (but which was a failed conversion).

I kept asking you what each line asserted, what "all previous lines" meant, even prompting you to admit you assert P(0), but you never once said "I get P(1)" until just now.

I see. I'll try again.

Why? Because you were not actually describing your thinking. You were trying to force it into symbols, including using the "⇒" symbol.

@user21820 Yes, that could be the reason.

Explain it exactly as it happened. Nothing more and nothing less.

What you wrote has a "...". That does not represent the pattern you held in your head. Instead, that "..." avoided talking about it.

@user21820 In each line, I see previous line and previous line ⇒ ???. It's really hard for me to see the actual pattern.

@F.Zer What line? I asked you to convince yourself that something is true. If that involves writing stuff down in lines, why are you not describing that? Your attempt using words 16 min ago did not use any lines.

@user21820 I get P(0). Then, from P(0) and P(0) ⇒ P(1) I get P(1). So, from P(0) ∧ P(1) and P(0) ∧ P(1) ⇒ P(2), I get P(2). From P(0) ∧ P(1) ∧ P(2) and P(0) ∧ P(1) ∧ P(2) ⇒ P(3), I get P(3). And from P(0) ∧ P(1) ∧ P(2) ∧ P(3) and P(0) ∧ P(1) ∧ P(2) ∧ P(3) ⇒ P(4), I get P(4).

That's correct, but it stops at P(4). It explains why you are convinced that P(0) to P(4) are true, but does not explain anything else.

@user21820 This is probably non-sense, but perhaps the general case is: from P(k) and P(k) ⇒ P(k+1), I get P(k+1). That is probably wrong. I'll try to follow your recent advice.

What? Did you even look at what you wrote in your second-last comment? It does not even look like what you wrote in your last comment!!

@user21820 That's why I said it is probably non-sense.

If you knew it didn't match what you just wrote, it doesn't make sense to say "probably non-sense".

Yes, I should've said it is non-sense :-)

@user21820 From ∀ i ∈ ℕ ( i < k ⇒ P(i) ) and ∀ i ∈ ℕ ( i < k ⇒ P(i) ) ⇒ P(k) I get P(k).

Yes that's correct. But then what? What has that got to do with your 4th-last comment?

That one ?

I miscounted due to the chat system not dividing consecutive lines.

@user21820 Good. So, what's your question ?

It's frustrating because you're not putting enough effort into identifying what you are doing.

What you wrote here looks nothing like what you wrote there. You always avoid saying what is happening.

@user21820 Sorry, I am putting 150% into what I am doing and I appreciate every bit of advice you've given me. It's just that I don't have much talent (like other of your students) nor logical intuition. I am sorry that is frustrating.

That's false. You have the ability, but you're not using it. First do you recognize that what you wrote 11 min ago already went through your head yesterday?

@user21820 You're kind, and I wish that is true. And yes, that went through my head, yesterday.

So it's not that you didn't think of it. It's that you didn't make it clear to yourself. Secondly, you're actually still not saying everything that went on in your head.

You say "from P(0) ∧ P(1)", but you failed to say what went on before that.

Similarly later you say "from P(0) ∧ P(1) ∧ P(2)", again failing to explain what you were thinking when you wrote that expression.

@user21820 Can you ask me anything else ? I've just made ten attempt at explaining but failed in each one of those. Perhaps, switching the angle of the issue a bit would help. It's a good way to get out of a "stuck moment".

Prove : ∀k,m∈ℕ ( m > 1 ∧ ¬∃d∈ℕ ( d > 1 ∧ d | k ∧ d | m ) ⇒ ∃x,y∈ℕ ( k·x = m·y+1 ) ).

\\Q(n) ≡ ∀k,m∈ℕ ( k+m = n ⇒ ( m > 1 ∧ ¬∃d∈ℕ ( d > 1 ∧ d | k ∧ d | m ) ⇒ ∃x,y∈ℕ ( k·x = m·y+1 ) ) )

Given a ∈ ℕ
	If ∀i∈ℕ ( i<a ⇒ P(i) )
		Given b ∈ ℕ
			Given c ∈ ℕ
				If b + c = a
					If  c > 1 ∧ ¬∃d∈ℕ ( d > 1 ∧ d | b ∧ d | c )

						If b = c
							c > 1 ∧ c | c ∧ c | c
							c > 1 ∧ c | b ∧ c | c
							∃d∈ℕ ( d > 1 ∧ d | b ∧ d | c )
							¬∃d∈ℕ ( d > 1 ∧ d | b ∧ d | c )
							⊥
							∃x,y∈ℕ (b·x = c·y+1 ) ) )

@user21820 is this correct?

@F.Zer I'll just cut it here and tell you. But you need to figure out how to do two things: (1) Don't even try to make a proof attempt before getting a rudimentary understanding of why something is true; (2) Be more precise to yourself (e.g. your last explanation up to P(4) was much better than what you wrote yesterday, and it came naturally when you stopped trying to force your thoughts into symbols).

The reason I keep emphasizing (1) is that I noticed that every time you try a proof attempt first and it happens to be wrong, you cause all your subsequent thinking to be skewed heavily towards that proof attempt, even if I repeatedly tell you not to do that. Clear evidence of this is when you made the "probably non-sense" remark (which is clearly arising from your incorrect first proof attempt whether consciously or not) despite it having completely no relation to what I just said was correct.

So, the problem here is that although I asked you to do only PL, and you did use only PL in that last explanation up to P(4), you did not say the ∧intro step, even though it did go through your head.

And that step was the key.

So your explanation should have looked like:

> I get P(0). Then, from P(0) and P(0) ⇒ P(1) I get P(1). Then I get P(0)∧P(1). Then using P(0)∧P(1) ⇒ P(2), I get P(2). Then I get P(0)∧P(1)∧P(2). Then using P(0)∧P(1)∧P(2) ⇒ P(3), I get P(3). In general, in each step I get P(0)∧...∧P(k) and then use P(0)∧...∧P(k) ⇒ P(k+1) to get P(k+1).

The bold parts are all missing from your explanation, but observe that they did go through your head. You simply never described them.

You cannot get P(2) from P(1) alone. But you can get P(0)∧P(1)∧P(2) from P(0)∧P(1). Again, you know all this. It's just that you never wrote it down.

@F.Zer: So use what I just said in my last two comments to construct the desired proof.

@user21820 I fully appreciate your comments and I'll take the advice.

@Prithubiswas It's correct, though you can make it easier for the reader by condensing the last few lines into "v ≥ u = 1+v > v. ⊥.".

@user21820 I am now trying to see how "p < b" can be used with strong induction.But I cant see how.

@Prithubiswas If b,c have no common divisor, what about p?

You mean I should try to see which number is coprime respect to p?

Maybe? I still don't know how much hint you want me to give you.

@Prithubiswas: I mean, what to do next should be clear if you try to match the conditions for the strong induction, namely a coprime pair with a smaller sum.

But maybe saying that explicitly is too much of a hint.

@Prithubiswas @F.Zer: Anyway, I need to go now. See you both later!

@user21820 See you later !

@user21820 Well, after reading 50 times your explanation, I do not have even a remote clue. My definition could be Q(k) ≡ ∀ i ∈ ℕ ( i ≤ k ⇒ P(k) ) ⇒ P(k+1). Although, that is probably also wrong. I can devote 2 hours per day to this problem, and rest. The next day, the same. Not sure whether spending more than that time would help to reach the solution. Does that seem a sensible approach ?

In sum, perhaps at a rate of 100 hours per month maybe I reach the solution in a couple of months.

@user21820 On a second thought, I see a pattern here. I am constantly stuck when I have to use my logical intuition. Can I ask you for advice ? What would you do to improve logical intuition for FOL ? I should probably take a step back and recognise this level is too much right now. Starting to do easier exercises.

I mean, sometimes I make 500 attempts and don't improve a bit. I should be honest with myself and recognise that, in order to keep up, I am constantly pushing myself to the limit. In the long run, that's not sustainable. I did every exercise, even ℤ, ℚ and ℝ ones, but my logical intuition and explaining capabilities doesn't seem to improve. However, I know the deductive system by heart.

Proof of The Second Direction

If (A or B) and (A or C):
                                   If A:
                                         A
                                         A∨B∧C
                                   A implies Conc
                                   If B:
                                         If A:
                                               	A
                                               A∨B∧C
                                          A implies A∨B∧C
                                          If C:

I skipped many things and maybe some typos

@F.Zer The reason you are stuck is that you cannot get rid of your wrong ideas. You have repeated that wrong idea about 10 times at least so far. I've no idea how to help you do this. It's just something you have to recognize in yourself and eliminate by yourself. Nothing in the comments I told you to rely on (this and the next one) can even remotely become your attempt at finding a suitable Q.

@PaxDaga It is correct if you fix your "Conc" and "Conc follows". Continue to the next exercises.

Ok

Also note that we are using standard precedence rules. If you don't know them, they are (from highest to lowest): ¬,∧,∨,{⇒,⇔}. You must use brackets if the precedence rules are insufficient to disambiguate. For PL you must at least know that "( A and B ) and C" and "A and ( B and C )" are distinct, even though you can deduce any from the other. If you know precisely why, then it's okay to drop brackets.

The precedence rules explain why we can write "A or B and C" instead of "A or ( B and C )" because "and" has higher precedence than "or".

Where did I not use brackets?

@user21820

@PaxDaga I'm not saying you made any mistake. I'm saying that you must know exactly when we can drop brackets.

Like why you must put brackets (as you did) in "B implies (A or B) and (A or C)" and why you did not need to in "A implies A or B and C".

ok got it I knew it

Great!

Do the excercises of a particular section increase in difficulty? or remain constant?

@PaxDaga Of course they increase in difficulty. However, the PL exercises are much easier than the FOL exercises. Anyone who knows PL fully would be able to do all 7 of them in just half an hour.

@user21820 I fully appreciate your comments. I always try (but not succeed) to listen carefully to what you say, take notes, review where I went wrong, and give 100% of what I got. Since changing how I intuitively understand and explain things is not a trivial matter, I have no other choice but leave this room for some time. I really don't want to start wasting your time with me. I hope to come back someday when/if I solved this problem. I will surely miss you.

I am sure more talented students can benefit from your wonderful teachings. I will forever be grateful to you. However, I will try to leave a nice GitHub repository before leaving.

@user21820 Could you take a look at this Systems ?

@F.Zer Maybe it's my mistake to expect you to be able to introspect your reasoning. It's possible. However, I don't think you should just keep working at this strong induction on your own. It's my opinion, but I think it's better either for you to try to eliminate your erroneous translation habits under my observation or for me to simply tell you the correct Q.

If you just go off and work at it on your own, it would be satisfying when you succeed, but I personally don't like having no upper bound on the time needed.

And if you worry that it would be a lost opportunity, don't, because I can always come up with other problems that require similar reasoning.

You are very kind. Thank you.

@user21820 "I personally don't like having no upper bound on the time needed" what do you mean by that ?

@F.Zer I have no doubt that you would eventually succeed in deriving strong induction as desired. However, I don't like not knowing a specific k such that you will succeed within at most k days... I would rather tell you the solution rather than make you spend too long.

@user21820 This is not an issue about this specific proof. It's that I can't solve any problem myself. At some point, I ask you for hints. And, if you don't tell me exactly how the problem is solved, I can't do it on my own. It's time to be honest with myself and recognise that.

@F.Zer There are some indentation issues with the syntax rules, starting from after "For example we can literally do the following deduction if Q is a 1-input predicate symbol:". Not sure what happened there because the wrong indentation is in the HTML itself.

@user21820 Yes, that is very good. I will not attempt to prove it on my own. I will leave that problem for some time. Maybe there is something I should solve before doing a problem all by myself.

@F.Zer Is that really true? My memory differs on that. You can solve the easy exercises. It's the hard exercises you can't solve. That's normal. Prithu also couldn't solve some of the hard exercises.

@user21820 Sure, I solved the easier and mechanic exercises. The problem is when something is not "mechanic". Prithu solved every exercise much faster and with less hints. And I am in University and he is in High School.

@F.Zer Hey that doesn't count. He's interested in higher mathematics and logic even before entering university. I knew less than he did at that time in my life.

But I get your point. I'm not sure whether it's possible to justify or refute the claim that you cannot do "non-mechanical" exercises.

@user21820 Yes, that makes sense.

Ah I know. You remember Cosmic Express? Do you consider the puzzles to be all "mechanically solvable"?

@user21820 I mean, I now have a very good grasp of a Natural Deduction system. I know 10 times more logic than my classmates thanks to you. But, without thinking and problem solving capabilities, I can't get anywhere.

@F.Zer You know programming , and I don't.

Also

@Prithubiswas Ok. You found the only one. But you did better in almost every other.

@user21820 No, I don't consider them "mechanically solvable". But there is some way to know this. If you like, you can give me an exercise (or exercises) which only rely on intuition. I think I won't be able to solve it.

So I am quite a bad problem solver , specially I only have problem solving skill of a high school student (maybe worse). On the other hand @F.Zer has programming knowledge and @user21820 has math competition experience.

@F.Zer Don't look down on your performance, just because I have a strong tendency to make exercise lists with exponentially increasing difficulty.

@F.Zer Concerning Cosmic Express, the reason I mention it is because I also don't consider it to be mechanically solvable, and I think it gives a rough idea of pure intuitive discrete puzzle-solving skills. I myself still cannot solve a few of the hardest ones in that game.

So how far you have gotten in that game should (in my opinion) give a rough idea of how good you have gotten at discrete solving skills.

@user21820 Yes, you said that earlier. I do remember.

@user21820 I've reached level 10, I think.

I didn't play anymore since the last 5 months.

@F.Zer Ah, I suggest you do many more. =)

@user21820 I will :-)

I believe it helps!

@F.Zer In my opinion , patients is more important than ingenuity in math.

@Prithubiswas I do believe you have outstanding problem solving capabilities, especially considering you are a high school student.

@Prithubiswas Yes, that is true.

@F.Zer I personally don't believe it.

Lol.

@user21820 That's a good summary.

Everyone has outstanding problem solving capabilities. But not everyone has the knowledge of how to read and write proofs logically.

I believe that both of you can improve your problem solving skills with practically no upper bound, over time, regardless of where you started out and where you are now. (This is a better summary.) =)

You're very kind.

@F.Zer: Anyway, how about I just attempt a full analysis of what I think was in your head and the full explanation of how to get the proof of strong induction, and then you take a break from this and go and finish as many Cosmic Express levels as you can in one week. I believe it helps.

(The reason for my belief is that I attribute my problem-solving skills with my almost continuous puzzle playing throughout my life. It seems to make my brain hurt every time I hit a hard puzzle and then after that my brain gets better.)

@user21820 Yes, if you think that is a good idea then I will do it. However, since I pushed myself extremely hard in the past months, I'll have to take a break for some time after doing this. What kind of full analysis would you like ?

@user21820 PA-1 to PA4 feels quite easy. But PA5 feels very hard. :P .

@F.Zer Yes then take a break for a week before trying the Cosmic Express puzzles in the week after. No problem. I would do the analysis, and you just have to read and ask if I'm unclear.

@user21820 Good. I'll ask.

@user21820 I have to go out a moment. I'll read your full analysis when I come back. Take care.

@F.Zer Sure. Basically I feel that when you originally attempted to figure out why "∀k∈ℕ ( P(k) )" is true given "∀k∈ℕ ( ∀i∈ℕ ( i<k ⇒ P(i) ) ⇒ P(k) )", you actually already did this:

Then you condensed it into this:

It was actually correct. You really did get P(0). You also really did get P(1). From where? From P(0) and P(0) ⇒ P(1). You got P(2) from the first two lines and P(0) ∧ P(1) ⇒ P(2). In fact, you also gave a correct but imprecise explanation:

However, for some reason I don't really know, you translated your correct thinking wrongly. You replaced "X from Y" by "Y ⇒ X".

That's not correct, because you're not just saying "Y implies X". You are saying "X" itself! And you're giving the reason, which is that you got "X" from "Y".

Furthermore, when you said "use all the previous lines to get the desired conclusion" I am 100% sure that at that very moment in time you actually did mean:

> In the last line, to get the desired conclusion P(4), I should use all the previous things I got, namely P(0) and P(1) and P(2) and P(3).

> And similarly in the general case.

That's why I was very surprised when I asked:

And you answered:

(You meant " ∀ i ∈ ℕ ( i < 1 ⇒ P(i) ) ⇒ P(1) ", but that wasn't the concern here.)

The point was that you actually did (in your head) get and assert P(1), not just P(0) ⇒ P(1).

Unfortunately, I was unable to figure out how to get you to realize that you are not asserting merely an implication.

Maybe I should have just said it directly.

Anyway that's what I think went on in your head. Hopefully it is useful for you to figure out how to avoid this mistake next time.

Now to explain how to get the desired proof, let's go back to the intuition that we all have:

It may be better to see it in separate lines:

Each [✻] marks an intuitive instance of the given condition "∀k∈ℕ ( ∀i∈ℕ ( i<k ⇒ P(i) ) ⇒ P(k) )".

To formalize this pattern, we must first identify the repeating unit.

Furthermore, the reasoning in each unit only requires what you deduced in the previous unit (and the given condition).

So the natural thing to do is to make an induction predicate following the units. That is; if we can deduce the three things in a given unit, then we can deduce the three things in the next unit.

Since each [✻] can be obtained in one step from the given condition, we can ignore that. Look again at the pattern left behind:

What you get in the first unit is P(1) and P(0)∧P(1). The second unit doesn't rely on P(1) directly. It simply relies on P(0)∧P(1). And in the second unit you get P(2) and P(0)∧P(1)∧P(2). Again, the P(2) is no longer needed.

So what you actually need is just the conjunction.

From each line you can get the next using a fixed number of deductive steps.

And these lines can be expressed in the form of Q(k), with k increasing by 1 as you go down.

That is the Q you are looking for.

You have two natural choices:

Either one would work.

@Prithubiswas: If you feel any part is unclear, please ask as well!

Related, but you can ignore this remark. I just want to say that the above reasoning is supposed to be convincing enough in the sense that if PA turns out to be unable to carry out the reasoning, or worse still unable to prove strong induction, then we would actually consider PA to be flawed. Fortunately, PA can do it, via normal induction on the appropriate predicate.

b = 9

	c	p	Property
	10	8	(b,p) coprime
	11	7	(b,p) coprime
	12	6	Not allowed
	13	5	(b,p) coprime
	14	4	(b,p) coprime
	15	3	Not allowed
	16	2	(b,p) coprime
	17	1	(b,p) coprime
	18	0	Not allowed
	19	8	(b,p) coprime
	20	7	(b,p) coprime
	21	6	Not allowed
	22	5	(b,p) coprime
	23	4	(b,p) coprime
	24	3	Not allowed
	25	2	(b,p) coprime
	26	1	(b,p) coprime
	27	0	Not allowed

@user21820 I am trying to recognize a pattern. Not sure if it is useful or not .

@Prithubiswas: It turns out I gave you the wrong outline, so luckily you weren't trying to follow it. This outline is the fixed one.

@Prithubiswas And yes, if you think b,p are coprime, why not try proving it?

@user21820 That's an impressive explanation. Thank you so much. I understand a bit better, so I would like to tell you a couple of things. I think this is what I meant, is it correct ?

I will write it, here:

So, I missed something in my reasoning.

Well you can put it that way.

@user21820 Maybe my latest comment is a bit better.

Though, really, what you missed is that each of your lines directly asserted P(something), not just "something implies P(something)".

And then it got warped further during translation because you kept the "⇒" around in every single attempt haha..

Is the explanation clear enough so that you understand why the Q at the end ought to be that way?

@user21820 I couldn't understand how could I "use" previous lines, when they are meta statements.

@F.Zer I see. You didn't realize that you should just assert the P(something) and not stay in the meta-reasoning.

@user21820 Could you tell me a bit more about this ? Perhaps it is the root of the issue.

Wait. Before we analyze what you did earlier further than what I tried, do you understand the explanation up to the Q?

Or have you not read that yet?

@user21820 Yes, I've read everything twice. It really useful to see it in terms of "units". I do not understand everything, though.

@F.Zer What's the first part you don't get? I think we should clear up the correct approach first.

@user21820 The first part is: "you are not asserting merely an implication".

@F.Zer Sorry my question was unclear. I meant to ask whether you understood the explanation of the correct approach, not about my guess regarding your thoughts.

Good. I'm looking at your second outline and will ask.

@user21820 You have this instance: "∀i∈ℕ ( i<k ⇒ P(i) ) ⇒ P(k)". I am failing to see how are you satisfying "∀i∈ℕ ( i<k ⇒ P(i) )" to get P(k) in each step.

@F.Zer Which message are you referring to?

@user21820 Sorry. Take k = 3. I see how are you doing it step by step; I can't figure out how that procedure fits in the general case.

There, you are satisfying "∀ i ∈ ℕ ( i < 3 ⇒ P(i) )".

To get P(3).

That message you quoted is directly obtained from the earlier one. All I omitted were the [✻] lines, which are intuitive instances of "∀k∈ℕ ( ∀i∈ℕ ( i<k ⇒ P(i) ) ⇒ P(k) )".

If you understood the earlier message, there's nothing new in the later message.

If you didn't understand the earlier one, remember that it's just intuitive instances. There is no formal proof going on here. The given condition intuitively means something, and that's all we are using here.

The point is just to be convinced, not to have a proof (until we actually figure out Q and try to find a proof).

@user21820 Wow. That's impressive. I was going to ask you about the formal proof. Lol

So do you get the intuition?

There's no proof in the entire explanation. It's all just to figure out what Q to try.

I'll think a bit more.

You get that ∀i∈ℕ ( i<3 ⇒ P(i) ) ⇒ P(3) intuitively means P(0)∧P(1)∧P(2) ⇒ P(3), right?

That's all that we're doing at that point.

I need to go, sorry. Just continue asking anything you want, and I'll respond next time!

If ∀k∈ℕ ( ∀i∈ℕ ( i<k ⇒ P(i) ) ⇒ P(k) ):
	∀i∈ℕ ( i<0 ⇒ P(i) ) ⇒ P(0)
	∀i∈ℕ ( i<0 ⇒ P(i) )
	P(0)
	∀i∈ℕ ( i<1 ⇒ P(i) ) ⇒ P(1)
	P(0) ⇒ P(1)
	P(1)
	P(0) ∧ P(1)
	∀i∈ℕ ( i<2 ⇒ P(i) ) ⇒ P(2)
	P(0) ∧ P(1) ⇒ P(2)
	P(2)
	...

@user21820 Are you doing something like that ?

@user21820 Yes, but I will ask you about that next time.

@F.Zer Yes, that's right.

@user21820 Thank you ! See you !

See you! =)

Prove strong induction from induction
  For any property P on ℕ, we can prove:
    ∀ k ∈ ℕ ( Q(k) ⇒ P(k) ):
      [Show ∀ k ∈ ℕ ( Q(k) ) with induction]
      Define Q(k) ≡ ∀i∈ℕ ( i<k ⇒ P(i) )
      Given i ∈ ℕ:
        If i < 0:
          ⊥
          P(i)
      ∀i∈ℕ ( i<0 ⇒ P(i) )
      Q(0)
      Given k ∈ ℕ:
        If Q(k):
          [Show ∀i∈ℕ ( i<k+1 ⇒ P(i) )]
          Given i ∈ ℕ:
            If i<k+1:
              i+1 ≤ k+1 [discreteness]
              i ≤ k
              If i < k:
                ∀i∈ℕ ( i<k ⇒ P(i) )

@user21820 I was reviewing my notebook, and looked at the last five lines of the proof by mistake. So, that is my current proof (except those five lines that came from the previous attempt).