@F.Zer Exactly. "¬P(0)" was the simplest thing you could have proven. And that's what is meant by trying small cases, because you ought to try to figure out whether you can prove or disprove P(0), and then P(1), and so on.

What about P(2)?

Once you get that, you will see that without induction you can already prove "¬P(k)" for any numeral k, where a numeral is either "0" or a term of the form "1+...+1". Whenever you see such a phenomenon, and there is a systematic pattern to the proof for each numeral based on previous ones, then you know that you can use induction (or strong induction) to handle all at once.

@user21820 Thank you so much for that great explanation. Could you check this proof, please ?

Prove Well-ordering from Strong induction:
  For any property P on ℕ, we can prove:
    If ∃k∈ℕ ( P(k) ):
      Let a ∈ ℕ such that P(a)
      If ¬∃m∈ℕ ( P(m) ∧ ∀k∈ℕ ( P(k) ⇒ k≥m ) ):
        ∀m∈ℕ ( P(m) ⇒ ∃k∈ℕ ( P(k) ∧ k<m ) )
        Given k' ∈ ℕ:
          If ∀i∈ℕ ( i<k' ⇒ ¬P(i) ):
            If P(k'):
              P(k') ⇒ ∃k∈ℕ ( P(k) ∧ k<k' )
              ∃k∈ℕ ( P(k) ∧ k<k' )
              Let b ∈ ℕ such that P(b) ∧ b<k'
              b<k' ⇒ ¬P(b)
              ¬P(b)
              ⊥
            ¬P(k')

@F.Zer That's right!

Just to be precise, final conclusion is: "For any property P on ℕ, we can prove ( ∃k∈ℕ ( P(k) ) ⇒ ∃m∈ℕ ( P(m) ∧ ∀k∈ℕ ( P(k) ⇒ k≥m ) ) )."

Thank you !

I will fix that little detail in the repository.

@user21820 I just pushed two updates to the repo. Do you like them ? Any improvements ?

Q1

PA-1

@F.Zer They are fine. But the lemma for (PA−1) should probably go into the Lemmas file since you also use it in (PA−2). And since you have the inequality lemmas you might as well use them to make it cleaner: m·2 ≥ (k+1)·2 = k·2+1+1 > k·2+1.

@user21820 Great. Just pushed three updates. What do you think about them, now ?

It didn't update. I will push again.

Fixed.

@F.Zer Still not updated.

Ok. Let me check.

@user21820 PA-1

That previous link pointed to the previous version, I think. This should be fixed.

@F.Zer Oh I see. Great! Shouldn't you label lines 4 and 5 with [lemma] since you're using the inequality lemmas?

@user21820 Done :-)

Sorry for being so picky with this, but I noticed every time I am using commutativity of ">" to reach the desired conclusion. It doesn't look nice. But if there isn't any better solution, it's fine.

@F.Zer Well you should just put a note in the system PA− itself that "t > u" is defined to mean "u < t" and "t ≤ u" is defined to mean "t < u ∨ t = u", and therefore you do not have to reverse anything in any proof as they would literally mean the same thing.

It's not commutativity. It's just a matter of definition. That is, you should not bother to write "k·2+1 < m·2" after "m·2 > k·2+1", as they mean the same thing.

In mathematics, many binary relations on the same type are treated similarly, including "⊆".

Though one common exception is "|", which is visually symmetric and so nobody can reverse it... Maybe the one who came up with it should not have used a single stick.

Oh, I didn't thought about that. It's very interesting.

@user21820 Thank you. I added a note in Systems PA-.

Yea so you can start erasing all lines where you didn't do anything except to turn some inequality around.

In fact, you can see that it is always possible to use only "<"; just turn everything around if necessary. But the point of choosing a direction is to hint the thought process. It makes less sense to write "k·2+1 < k·2+1+1 = (k+1)·2 ≤ m·2" even though it is perfectly correct, because we find it by starting from "(k+1)·2 ≤ m·2".

@user21820 What do you mean by "because we find it by starting from "(k+1)·2 ≤ m·2"." ?

@F.Zer How else did you find the proof?

Maybe you can't remember. But if you start from the discreteness lemma, that's what you get first.

Oh, yes. I started from k+1 ≤ m. Why didn't you start with "(k+1)·2 ≤ m·2" ? It's the first step after discreteness.

Why do you switch it to "m·2 ≥ (k+1)·2" ?

@F.Zer But that's my point; according to what I said, I did, because that means literally the same thing.

Got it.

It's only if you think of ">" as something different that you need extra steps.

But you shouldn't; it's not supposed to be different.

@user21820 I always look at the direction of "<" in the conclusion. But what you are saying is great; you prioritize the thought process over the "direction" of "<" in the conclusion.

Yes. After all, if I ask you to evaluate 2^3 you would not tell me 8 = 4·2 = 2·2·2 = 2^3.

Since they mean the same thing, I shouldn't be doing that.

@user21820 Hahaha. Good example. It clicked :-)

Similarly with equality chains, but the difference is that "t = u" is syntactically different from "u = t". We cannot say they mean the same thing. For equality we can turn it around truly because of symmetry of equality, and not by definition.

@user21820 Mmm...Not sure I get that.

I know about symmetry of equality, though.

The basic deductive rules don't let you deduce one from the other directly. You saw that when doing the FOL exercises. But by now you have of course treated it as obvious.

And you should, even though it cannot even be defined away unlike ">" in terms of "<". At the level of PA−, there is no point fussing over any of this.

@user21820 ">" is a two place predicate; isn't "=" also a two place predicate ?

@user21820 "The basic deductive rules don't let you deduce one from the other directly." You are saying that I can't deduce "t = u" from "u = t" ?

"=" is a core logical symbol governed by the =intro/elim rules. Syntactically it may look like a 2-input predicate-symbol, but it isn't.

Got it. Thank you.

@F.Zer Not in one step. Look at the equality rules again. There's nothing wrong with doing it mentally in one step; but you need to realize that you cannot say that "u = t" means "t = u". Same reason as the other example I gave of "|".

Symbols need to be visually different if you want to define one in terms of the other!

Yes.

@user21820 That's a very interesting observation !

@user21820 I should go out of my house now. See you next time and take care !

@F.Zer Same to you!