Given k ∈ ℕ: [1]
	P(n) ≡ ¬∃q∈ℕ ( 1 < q < n ∧ q | n ) [n is prime] [2]
	Q(n) ≡ n > 1 ⇒ ∃p∈ℕ ( p > 1 ∧ p | n ∧ P(p) )  [3]
	If ∀i∈ℕ ( i<k ⇒ Q(i) ): [4]
		[Prove Q(k) ] [5]
		If k > 1: [6]
			[Prove ∃ p ∈ ℕ ( p > 1 ∧ p | k ∧ P(p) ) ] [7]
			P(k) ⋁ ¬P(k) [k is prime or ¬k is prime] [8]
			If P(k): [9]
				k > 1 ∧ k | k ∧ k is prime [10]
				∃ p ∈ ℕ ( p > 1 ∧ p | k ∧ ¬∃ q ∈ ℕ ( 1 < q < p ∧ q | p ) ) [k has at least one prime divisor > 1 (itself)] [11]
			If ¬P(k): [12]
				[k is composite ≡ (k = m · n, for some m,n ∈ ℕ ∧ 1 < m < k ∧ 1 < m < n )] [13]

@user21820 Thank you, @user21820. My proof was wrong. I corrected the mistake at line 15.

@shintuku Yes, you already got an answer, but technically that answer is wrong. Expressions do not have a domain. You didn't specify any domain, so there isn't one. Also, if you had been precise, you wouldn't have had the question, because the properties for logarithms come with explicit conditions. Try stating them for me without looking them up:

> ln(a·b) = ln(a)+ln(b) for every ... a,b such that ...

> ln(a^r) = r·ln(a) for every ... a,r such that ...

> ln(exp(a)) = a for every ...

> exp(ln(a)) = a for every ...

Fill in the blanks.

@Prithubiswas Yes that would be enough.

@user21820, Hi ! Could you tell me if my latest proof is correct, please ?

@F.Zer Wait a moment. I want to answer the other questions first.

@user21820 Sure ! Thank you.

@shintuku Your original approach is correct, but you're missing the phrase "for some constant C" at the first point you introduced it. Don't leave out such important details. Also, at this point you would have restrictions on the constant depending on the permitted range of values of your variables. In particular, it may be that C∈ℝ in some applications, or C∈ℂ in others.

am reading your second comment, thank you so much for answering!

@shintuku Exactly, I'm glad you see clearly how the conditions for (1) force you to be unable to reach the problem. Though your answers for (2) and (3) are in fact wrong...

Your (2) is false for (a,r) = (−1,2).

Your (3) is ill-defined, because "is defined" is ill-defined. You need to explicitly state the possible values allowed for a. Such as a∈ℂ.

argh! for (2) you're right, the logs can only take positive values, so a>0. for (3), there is no restriction on a, since e^a is defined if a is a number, I think, so $a \in \mathbb{R}$ (can't tell for complex number, haven't done any complex analysis yet!)

@shintuku If you've not come to complex numbers yet, then sure a∈ℝ. Don't just say "a number" as it is as ill-defined as "a mathematical object".

alright! and I've read your second comment, also noted. thank you very much!

Same for (2). Valid for reals a,r such that a>0.

@shintuku Your later idea of anyhow using a multiplicative constant k to replace the e^C is actually a bit problematic if you got it without properly deriving it, or think it works for every possible constant k. In the original approach, we have that given real variables x,y satisfying 1/y·dy/dx = 1/x, we have ∫ 1/y dy = ∫ 1/x dx + c for some constant c∈ℝ, and so ln(|y|) = ln(|x|)+c, and so |y| = |x|·exp(c) = |x|·k where k = exp(c).

You do not know, from this alone, which k would give you an actual solution to the original problem.

So you need to check. First note that x,y ≠ 0 because that's required for the differential equation to be meaningful.

Also, dy/dx existing everywhere on the curve you're interested in implies that x,y are continuously varying so each of them is either always positive or always negative.

So from the earlier conclusion we can further deduce that y = k·x or y = −k·x.

And then we need to check to see whether each of those k yields a valid solution. Note that k = exp(c) can attain every positive real. And all of them do yield valid solutions.

thank you so much for taking the time!

i've added all of this to my notes

it's crazy how missing a little piece of reasoning makes everything else ambiguous

Note that the above solution actually shows that k ≠ 0. This feature of the above solution is not a necessary phenomenon, but it is actually what I expect, since usually the rigorous solution will typically reveal or hint the boundary of valid solutions.

you'd think all it takes is the big picture, but that really isn't enough

@user21820 right

i'm a bit new to analysis so still working on rigour, so I will note these tips duly

If you remember, I linked you to a post with a complicated differential equation which non-rigorous solutions are likely to get wrong. You may be interested in looking at a simpler example first: x·dy/dx = y. The immediate itch that people who 'know separable equations' have is to write 1/y·dy/dx = 1/x, which is what you had in your latest question!

If the latter form was how it was given to you, it is an example of how textbook writers or university lecturers purposely give only a 'form' that doesn't cause the 'separable technique' to fail badly.

Notice that the former form "x·dy/dx = y" is satisfied if y = 0 for every x≤0 and y = x^2 for every x≥0.

i've begun using the two-theorem technique you wrote above, it's not that complicated to use once you get used to it

actually gets you to skip the separation step hehe, so it's faster

Sorry I made a mistake in my example lol.

Should have been x·dy/dx = 2y.

Edited to fix it again hahaha..

This example is supposed to show that the incorrect division by x and y that many people will do to separate the variables results in wrong answers. In particular, if you start from ∫ 1/y dy = ∫ 2/x dx + c for some constant c, then you get ln(|y|) = 2·ln(|x|) + c, and so |y| = |x|^2·k = k·x^2 where k = exp(c). This turns out to be one solution, but the method is completely bogus because it's not valid at x = 0 or y = 0, so you're not even supposed to be able to conclude anything at those points.

@user21820 Ordinary induction comes from one of the peano axioms , right?

And strong induction principal can be proved from ordinary induction , correct?

@shintuku: And as I mentioned above, there are also solutions that totally fail to be found by the incorrect 'separating variable technique'. One might wonder whether you can just arbitrarily piece together two solutions, by having one constant k for the left and one for the right, and by nonsensically assuming that we can allow k = 0 because "why not?". This nonsense does yield the right solution set for this simple example, and that is why I used a more complicated example in my linked post.

In the example in the linked post, there is absolutely no way you can pull the correct solution set out of thin air if you don't use a rigorous approach.

@Prithubiswas @F.Zer showed (after fixing a small error) that PA− plus Induction can prove Strong Induction. The axioms of PA− are given here under "Peano Arithmetic". The original induction in Peano's axioms was useless, but at that time mathematicians were extremely unclear about logic.

@user21820 wait , why PA + induction , doesn't the peano axioms have an axiom schema for induction ?

@Prithubiswas I didn't say what you said. Please quote me exactly.

@user21820 you said " PA− plus Induction can prove Strong Induction". But cant we just say " PA can prove Strong Induction" because PA already has an axiom schema for induction ?

@Prithubiswas Yes, we can. I asked you to quote me exactly because you implied that I said "PA + induction" (which would be silly), but I did not. The reason I wrote what I wrote instead of just "PA proves Strong Induction" is that PA− plus Strong Induction proves Induction.

So we have an equivalence of two axiom schemas over PA−. Similarly for equivalence of Induction and Well-ordering. I showed one direction. The other direction is easy.

@user21820 And what did you exactly meant by "The original induction in Peano's axioms was useless" ? was there a different kind of induction axiom back in the day?

@Prithubiswas Yes, the original Peano's induction, which is still popularized by uninformed people including many mathematics textbooks involves sets.

@user21820 Can you show me that ?

Well it was just ∀S⊆ℕ ( 0∈S ∧ ∀k∈ℕ ( k∈S ⇒ k+1∈S ) ⇒ ∀k∈ℕ ( k∈S ) ). This axiom is useless if you do not have axioms to govern what sets can be constructed.

And if you do have set-theoretic axioms, you no longer have just PA.

@user21820 Like ZFC?

Yes, such as ZFC. But it is also extremely misleading to teach this set induction axiom as "induction", even if you want to talk about induction in a set theory like ZFC, because it gives the false impression that you must be able to construct a set in order to invoke induction.

@Prithubiswas You can prove the structural induction that is typically used from normal induction, in any reasonable foundational system. I don't really like wikipedia for not giving proper explanation of that.

You can see the following post (also linked from my profile) for an English rendering of this typical structural induction:

A simple symbolic form is:

"You can prove the structural induction that is typically used from normal induction, in any reasonable foundational system" , can you give me an example of such a foundational system ?

> Structural induction: ∀f∈S→ℕ ( ∀x∈S ( ∀y∈S ( f(y)<f(x) ⇒ Q(y) ) ⇒ Q(x) ) ⇒ ∀x∈S ( Q(x) ) ), for every set S and property Q on S.

@Prithubiswas The one I linked earlier gives a deductive system with axioms that has equal strength to ZFC but is more user-friendly. In particular, it has an induction rule under "Set Theory", rather than an 'infinity axiom' in typical formalizations of ZFC. It is easy to prove the above statement of structural induction in that system.

@user21820 Ok I will go now.

@Prithubiswas Sure. See you later.

@F.Zer Firstly, note that P(n) ≡ ( n is prime ∨ n ≤ 1 ). So you made a mistake once you wrote "k is prime" in your proof instead of "P(k)". Secondly, you are still pulling things out of thin air. Go through each line one by one and check whether you actually derived it or you simply wrote it from guesswork or intuition or something else.

And I want to emphasize (as I said before) that the idea is correct but the proof is wrong.

@user21820 I thought "¬∃q∈ℕ ( 1 < q < n ∧ q | n )" and n is prime had the same truth value. Is that wrong ?

I will have to check my understanding of prime numbers, then.

@F.Zer 0 and 1 are not prime. But that isn't the real concern. The real concern is that you are not doing formal logical deduction in your proof. It isn't necessary to write down every little step, but you actually need to do every deductive step mechanically (even if mentally).

@user21820 Of course, 0 and 1 are not prime. Isn't "¬∃q∈ℕ ( 1 < q < n ∧ q | n )" sufficient enough to mean "n is prime" ?

@F.Zer It implies "n is prime". I try not to use the word "mean" as it means something else.

But again, that's not the main concern.

Good. But why did you re-define "P(n) ≡ ( n is prime ∨ n ≤ 1 )" ?

I should note my main goal is doing every deductive step mechanically. However, it seems I am not accomplishing it :(

Oh, so "P(n) ≡ ( ¬∃q∈ℕ ( 1 < q < n ∧ q | n ) ∨ n ≤ 1 )"

@F.Zer I didn't redefine. When I don't say "define", I do not mean "define".

Understood.

I was just telling you that your P(n) was equivalent to ( n is prime ∨ n ≤ 1 ).

The symbol for that is "≡". It's different from the internal "iff" represented by "⇔".

Got it.

I should think how can I symbolise n is prime, then.

@F.Zer But why? You're just making it unnecessarily complicated by using the popular notion of "prime".

Your P was good enough.

Good.

I'll follow your advice.

> Go through each line one by one and check whether you actually derived it or you simply wrote it from guesswork or intuition or something else.

@user21820 Perfect. I'm doing exactly that.

Good!

@user21820 Wow. I had many blatant errors. I wonder how I missed those. Here is the revised proof.

Given k ∈ ℕ:
	P(n) ≡ n is prime ⋁ n ≤ 1
	Q(n) ≡ n > 1 ⇒ ∃p∈ℕ ( p > 1 ∧ p | n ∧ ¬∃ q ∈ ℕ ( 1 < q < p ∧ q | p ))
	If ∀i∈ℕ ( i<k ⇒ Q(i) ):
		[Prove Q(k) ≡ k > 1 ⇒ ∃p∈ℕ ( p > 1 ∧ p | k ∧ ¬∃ q ∈ ℕ ( 1 < q < p ∧ q | p ) ) ]
		If k > 1:
			[Prove ∃ p ∈ ℕ ( p > 1 ∧ p | k ∧ ¬∃ q ∈ ℕ ( 1 < q < p ∧ q | p ) ) ]
			P(k) ⋁ ¬P(k) [LEM]
			If P(k):
				k is prime ⋁ k ≤ 1
				If k is prime:
					k > 1 ∧ k | k ∧ ¬∃ q ∈ ℕ ( 1 < q < k ∧ q | k )
					∃ p ∈ ℕ ( p > 1 ∧ p | k ∧ ¬∃ q ∈ ℕ ( 1 < q < p ∧ q | p ) ) [k has at least one prime divisor > 1 (itself)]

@F.Zer I don't like the new version, even though I noticed some errors disappeared. Why did you not use your original P even though I said it was good enough, and even though I said using the notion of "prime" makes it unnecessarily complicated?

Did you really have to phrase it in terms of "prime" and "composite", and moreover use a claimed relation between them without proof?

@user21820 Oh, I was sure a number only could be prime or composite. Should I prove that or follow another path ?

@user21820 Oh, I mis-read you ! I am so sorry ! You said "unnecesarily complicated".

@F.Zer I know you were sure, and I know you were doing that. But I told you to stick to the deductive rules and not to use "guesswork or intuition or something else", so I really don't know why you kept doing it. =|

Just use your original P, and use the deductive rules to patch all the gaps in your proof.

And then simplify it as much as you can. There is no harm in using intuition to find a proof, but there is also benefit in shortening it afterward.

@user21820 I am trying to follow your advice 100% !! I thought prime or composite was an obvious step. Sorry.

@user21820 Good.

@F.Zer It's not an axiom in my deductive system, and not a previous lemma or theorem or exercise, so not allowed!

@user21820 Fully understood :-)

Point is, if you want to build mathematics from scratch, better build it all yourself!

@user21820 That's excellent. I think that comment should be starred :-)

@F.Zer Alright.

I can safely say that the average person can, after a few months of work (of the sort you're doing so far), grasp PA and go beyond. After a year, it should not be a problem to then rebuild large portions of undergraduate mathematics formally enough that there will be no doubt of correctness (excepting careless mistakes).

@user21820, just to clarify something. In our previous chapter, we pushed a little bit with things like "If there is no monochromatic triangle". There were no axioms regarding that and that's why I though about doing LEM on "prime or composite". Perhaps, we had a different goal back then, and in PA I should only use axioms and previously proved theorems ? If I am misunderstanding, I apologise.

@user21820 That's amazing.

@user21820 I'll do exactly that.

@F.Zer Actually we didn't step beyond the system in the end. I kept emphasizing that you needed to eventually formalize the intuitive proof, not just stop there. Also, there would be nothing wrong with defining Prime(n) ≡ whatever you want, and then using Prime and ¬Prime, but that's not what you did. You didn't define "composite", and yet you wrote down a claim about it from nowhere.

@user21820 Ohh ! I perfectly understood what's happening. Thank you !

Of course, eventually you will be able to immediately identify with almost 100% accuracy whether some intuitive argument can be formalized or not, at which point the formal system would be more of an unconscious tool. Believe it or not, some professional mathematicians never get to that point, and that is why they always have to ask their logic colleagues to tell them whether an argument uses something or not (e.g. axiom of choice). And I've seen this a number of times...

For a semi-serious guide to formality:

The Fitch-style deductive system I gave you is almost at the top, being in theory "absolutely formal" just that I didn't write a program to verify such proofs.

As you improve in your understanding of logic, you will ironically be able to climb down that hierarchy, meaning to write less and less formal proofs that actually prove correct theorems...

All those comments are very interesting and expand my horizon. (I've just added that link to my reading list and will carefully read it.)

@user21820, I will first prove the case P(k):

Given k ∈ ℕ:
	P(n) ≡ ¬∃q∈ℕ ( 1 < q < n ∧ q | n )
	Q(n) ≡ n > 1 ⇒ ∃p∈ℕ ( p > 1 ∧ p | n ∧ P(p) )
	If ∀i∈ℕ ( i<k ⇒ Q(i) ):
		[Prove Q(k) ]
		If k > 1:
			[Prove ∃ p ∈ ℕ ( p > 1 ∧ p | k ∧ P(p) ) ]
			P(k) ⋁ ¬P(k)
			If P(k):
				k > 1
				k | k
				P(k)
				k > 1 ∧ k | k ∧ P(k)
				∃ p ∈ ℕ ( p > 1 ∧ p | k ∧ ¬∃ q ∈ ℕ ( 1 < q < p ∧ q | p ) )

You're going to continue, right?

@user21820 Of course ! Doing the other case.

Ok. Was just checking just in case you were waiting for my response.

Good.

If ¬P(k):
	P(n) ≡ ¬∃q∈ℕ ( 1 < q < n ∧ q | n )
	Q(n) ≡ n > 1 ⇒ ∃p∈ℕ ( p > 1 ∧ p | n ∧ P(p) )
	∃q∈ℕ ( 1 < q < k ∧ q | k )
	Let q' ∈ ℕ such that 1 < q' < k ∧ q' | k
	q' < k ⇒ Q(q')
	q' < k
	Q(q')
	q' > 1 ⇒ ∃p∈ℕ ( p > 1 ∧ p | q' ∧ P(p) )
	q' > 1
	∃p∈ℕ ( p > 1 ∧ p | q' ∧ P(p) )
	Let p' ∈ ℕ such that p' > 1 ∧ p' | q' ∧ P(p')
	p' | q' ∧ q' | k ⇒ p' | k
	p' | q' ∧ q' | k
	p' | k
	p' > 1 ∧ p' | k ∧ P(p')
	∃ p ∈ ℕ ( p > 1 ∧ p | k ∧ ¬∃ q ∈ ℕ ( 1 < q < p ∧ q | p ) )

@user21820, just did the other case. This is as formal as I could get :-)

@F.Zer I've never said you could write "P(n) ≡ ¬∃q∈ℕ ( 1 < q < n ∧ q | n )" inside a formal proof as an assertion. You can define a property by saying "Define P(n) ≡ ... , for each n∈ℕ.". But you cannot just copy part of the definition elsewhere!

@user21820, I see. Where am I allowed to define it ?

Outside the main proof ?

Or perhaps should I use Let inside the main proof ?

@F.Zer Formally, that's the easiest way to handle it. But it's okay to do definitions halfway through a proof, just that you should use proper syntax to make it clear. According to what I said previously, to define a property you say "define" and use the "≡" symbol to indicate that it is an external definition of a new predicate-symbol, and when you use it in a proof you need the internal "⇔" symbol to state the equivalence.

But you don't even need to state the equivalence; simply use "P(n)" as if it is identical to "¬∃q∈ℕ ( 1 < q < n ∧ q | n )".

Nobody wants to waste time using ⇔elim and ⇔intro, after all.

@F.Zer "Let" is only for ∃elim; don't go and use it for something else.

Anyway, let me check the rest of both parts of your proof.

If y=1+(dy/dx)+1/2! (dy/dx)^2+..... 1/n! (dy/dx)^n is an nth degree differential equation, but if n tends to infinity dy/dx=lny making it 1st degree.....Why does this seem weird?

@F.Zer Ok both cases are correct. The syntax for definitions and using them is something you need to fix for next time, but it doesn't affect the correctness of your argument.

@user21820 I will do it just once to be sure I understand and then omit those steps. Could you tell me if you like this ?

Define P(n) ≡ ¬∃q∈ℕ ( 1 < q < n ∧ q | n ), for every n∈ℕ.
Define Q(n) ≡ n > 1 ⇒ ∃p∈ℕ ( p > 1 ∧ p | n ∧ P(p) ), for every n∈ℕ.
Given k ∈ ℕ:
	 P(k) ⇔ ¬∃q∈ℕ ( 1 < q < k ∧ q | k )
	Q(k) ⇔ n > 1 ⇒ ∃p∈ℕ ( p > 1 ∧ p | n ∧ P(k) )
	If ∀i∈ℕ ( i<k ⇒ Q(i) ):

However, you need to convince me you know how to prove "p' | q' ∧ q' | k ⇒ p' | k". Do you?

@user21820 Thanks for checking !

@user21820 I'll try.

@F.Zer Yes that's indeed what I meant. In practice, you would do exactly that mentally but not write down those lines with "⇔".

Excellent. Thank you.

Since "P(n) ≡ ¬∃q∈ℕ ( 1 < q < n ∧ q | n ), for every n ∈ ℕ", I can use Universal Elimination and get "P(k) ⇔ ¬∃q∈ℕ ( 1 < q < k ∧ q | k )" since k ∈ ℕ, I presume.

@user21820 I will prove it.

@F.Zer Yes, as I said the full formalization of defining new predicate-symbols is by the rule that simply says you can write the appropriate ∀-statement anywhere, using a fresh predicate-symbol. The reason I don't ask you to do that is, of course, because it looks unnatural to suddenly see a random ∀-statement pop up from nowhere. That's why we ease it in by saying "define ..." and using "≡" to make clear what is being defined as what.

For example if we had predicate-symbols P,Q on S we might define R(x) ≡ P(x)⇔Q(x), for each x∈S.

It would be confusing and not very logical to mix the "≡" symbol and its meaning with the "⇔" symbol, even though only the latter needs to be used in the full formalization of this notion of defining new predicate-symbols!

@user21820 Great. When you say "it looks unnatural to suddenly see a random ∀-statement pop up from nowhere", do you mean something like: "∀ x ∈ S ( R(x) ≡ P(x)⇔Q(x) )" ?

@F.Zer Exactly, except you're using the wrong symbol there.

The rule only needs to let you suddenly write "∀ x ∈ S ( R(x) ⇔ ( P(x)⇔Q(x) ) )" where "R" is a fresh predicate-symbol, anywhere in a proof.

@user21820 Oh, we can't mix "≡" and "⇔" inside the proof. I see.

That makes sense. There are no inference rules concerning "≡".

@F.Zer Exactly. So if you did write "∀ x ∈ S ( R(x) ⇔ ( P(x)⇔Q(x) ) )" out of the blue, it is technically how on-the-fly definitorial expansion works, but humans prefer to read some comment on where that comes from.

The "define ..." statement I use and tell you to use is precisely this kind of commentary.

Great.

Similarly, we haven't needed it yet, but you can define function-symbols as well. But it's not so obvious what is allowed.

Maybe you can take a look again at this post:

Just focus on the three points for now.

(3) first.

It may seem funny, because it essentially is the ∃elim rule!

The reason why it is in that post is that other systems for FOL don't have the same ∃elim rule as my system.

@user21820 Excellent. I will read it !

Next is (1), which we just talked about.

The defining of new function-symbols is (2).

Not so trivial, so it's okay if you don't understand it at first glance.

Besides, maybe we haven't even talked about "∃!"...

That's good. I'll let you know in case some question arises.

@user21820 No :-)

@user21820 I am proving this one:

Lemma:
	Prove ∀ x,y,z ( x | y ∧ y | z ⇒ x | z )
	(infix) | : ℕ^2→Bool is defined via ∀x,y∈ℕ ( x | y ⇔ ∃d∈ℕ ( y = x · d ) )
	Given x,y,z ∈ ℕ:
		If x | y ∧ y | z:
			∃ d ∈ ℕ ( y = x · d )
			∃ d ∈ ℕ ( z = y · d )
			Let a ∈ ℕ such that y = x · a
			Let b ∈ ℕ such that z = y · b
			z = (x · a) · b
			z = x · ( a · b )
			∃ d ∈ ℕ ( z = x · d )
			x | z
	∀ x,y,z ( x | y ∧ y | z ⇒ x | z )

@F.Zer Right!

"∃!x∈S ( Q(x) )" is defined as short-form for "∃x∈S ( Q(x) ∧ ∀y∈S ( Q(y) ⇒ x=y ) )". In English, "there is some unique x in S satisfying Q", meaning "there is some x in S that satisfies Q, and every y∈S that satisfies Q is equal to that x".

@user21820 Good ! Full proof, here:

Define P(n) ≡ ¬∃q∈ℕ ( 1 < q < n ∧ q | n ), for every n∈ℕ.
Define Q(n) ≡ n > 1 ⇒ ∃p∈ℕ ( p > 1 ∧ p | n ∧ P(p) ), for every n∈ℕ.
Given k ∈ ℕ:
	P(k) ⇔ ¬∃q∈ℕ ( 1 < q < k ∧ q | k )
	Q(k) ⇔ n > 1 ⇒ ∃p∈ℕ ( p > 1 ∧ p | n ∧ P(k) )
	If ∀i∈ℕ ( i<k ⇒ Q(i) ):
		[Prove Q(k) ]
		If k > 1:
			[Prove ∃ p ∈ ℕ ( p > 1 ∧ p | k ∧ P(p) ) ]
			P(k) ⋁ ¬P(k)
			If P(k):
				k > 1
				k | k
				P(k)
				k > 1 ∧ k | k ∧ P(k)
				∃ p ∈ ℕ ( p > 1 ∧ p | k ∧ P(p) )
			If ¬P(k):
				P(n) ≡ ¬∃q∈ℕ ( 1 < q < n ∧ q | n )
				Q(n) ≡ n > 1 ⇒ ∃p∈ℕ ( p > 1 ∧ p | n ∧ P(p) )

@user21820 Very clear.

@F.Zer Good! Now you have the other task, which is to prove (PA3) using well-ordering. There are actually two possible approaches. One is similar to the strong induction approach; if (PA3) is false then there is a counter-example, so by well-ordering there is a minimal counter-example, but that means that everything below it works, so the inner part of your above proof applies, yielding contradiction.

I want you to try the other approach:

You want to prove "∀k∈ℕ ( k > 1 ⇒ ∃p∈ℕ ( p > 1 ∧ p | k ∧ ¬∃q∈ℕ ( 1 < q < p ∧ q | p ) )". So you might try starting with:

Given k∈ℕ:
  If k > 1:
    ...
    [here notice that you already have k > 1 and k | k]
    [so you can prove ∃p∈ℕ ( p > 1 ∧ p | k )]
    [now apply well-ordering!]

@user21820 Thank you ! I will start with your outline and try to prove PA3.

@user21820 Could you please clarify "if (PA3) is false then there is a counter-example, so by well-ordering there is a minimal counter-example, but that means that everything below it works, so the inner part of your above proof applies, yielding contradiction." ? I can't do many mental leaps so fast, yet :-)

Where does the inner part start ?

@F.Zer Your inner part shows that if the claim holds for everything less than k then it holds for k. The point is, if there is a counter-example in ℕ, then well-ordering generates a minimal counter-example, and then your inner part shows that it is impossible.

@user21820 Wow. I understood more. I will digest it a bit.

@user21820 This is my first attempt:

Given k∈ℕ:
	If k > 1:
		k > 1
		k | k
		∃ p ∈ ℕ ( p > 1 ∧ p | k )
		∃ m ∈ ℕ ( m > 1 ∧ m | k ∧ ∀ n ∈ ℕ ( P(n) ⇒ n ≥  m ) )
		Let m' ∈ ℕ such that m' > 1 ∧ m' | k ∧ ∀ n ∈ ℕ ( P(n) ⇒ n ≥  m' )
		∀ n ∈ ℕ ( n > 1 ∧ n | k ⇒ n ≥ m' )
		k > 1 ∧ k | k ⇒ k ≥ k

I used well-ordering at line 6.

I should reach a contradiction, I think.

I should note "∀k∈ℕ ( P(k) ⇒ k≥m )" is equivalent to "¬∃k∈ℕ ( P(k) ∧ k<m )"

@F.Zer No you didn't.

@user21820 Sorry ! I will fix it.

I didn't define P.

Again, you're not following the deductive rules mechanically. Try to improve your accuracy. So far, almost every attempt of yours has errors. This is not acceptable in the long run.

@user21820 Yes, I see what you're referring to. I was asked to do many non-rigourous at my course and never developed that habit. I will work hard on that.

As I said, when you want to use something COPY and PASTE the whole statement and substitute mechanically. You cannot copy half a line (which is what I think you did) and expect not to make mistakes at your current level.

Understood.

After you paste and substitute also check that you didn't have variable clash.

@user21820 I was thinking about that :-)

Given k∈ℕ:
	If k > 1:
		k > 1
		k | k
		∃ p ∈ ℕ ( p > 1 ∧ p | k )
		∃ m ∈ ℕ ( m > 1 ∧ m | k ∧ ∀ n ∈ ℕ ( n > 1 ∧ n | k ⇒ n ≥  m ) )

@user21820 This should be good, now. What do you think ?

@F.Zer That's correct.

Good.

Ok I'm off now. Bye!

@user21820 Thank you so much for your amazing explanations ! See you !