Basic Mathematics - 2021-10-25

« first day (1266 days earlier) ← previous day next day → last day (923 days later) »

4:23 PM

Hi @user21820 ! How are you ? I've spent 10 to 20 minutes per day, two or three times per week with Cosmic Express. It was fun and useful. I've completed the first 20 levels. Thank you for the recommendation !

user21820

@F.Zer Nice going!

I'm fine but really busy.

F. Zer

I'm glad you're fine. If you have a moment, could you tell me whether my outline heads in the right direction. I'll keep working on it.

Prove Well-ordering from Strong induction:
  For any property P on ℕ, we can prove:
    If ∃k∈ℕ ( P(k) ):
      Let m ∈ ℕ such that P(m)
      If ¬∃m∈ℕ ( P(m) ∧ ∀k∈ℕ ( P(k) ⇒ k≥m ) ):
        ∀m∈ℕ ( P(m) ⇒ ∃k∈ℕ ( P(k) ∧ k<m ) )
        P(m) ⇒ ∃k∈ℕ ( P(k) ∧ k<m )
        ∃k∈ℕ ( P(k) ∧ k<m )
        ...
      ∃m∈ℕ ( P(m) ∧ ∀k∈ℕ ( P(k) ⇒ k≥m ) )
  For any property P on ℕ, ∃k∈ℕ ( P(k) ) ⇒ ∃m∈ℕ ( P(m) ∧ ∀k∈ℕ ( P(k) ⇒ k≥m ) ). [Well-ordering]

I should find a suitable Q.

I pasted and realized that :-)

user21820

4:49 PM

@F.Zer Um you used "m" in a quantifier after you have declared it in an ∃elim. That is invalid. If you fix that, then you have shown that from P(m) for some m∈ℕ you can get P(k) for some k < m. But you're not going to get anywhere with that because you're back in the same situation as before. To get anywhere you have to try small cases...

And then based on the reasoning for small cases you can figure out what property Q to use strong induction on.

F. Zer

@user21820 You mean this quantifier ¬∃m∈ℕ ( P(m) ∧ ∀k∈ℕ ( P(k) ⇒ k≥m ) ) ?

user21820

Yes.

F. Zer

@user21820 I forgot that detail. What did we do to avoid that problem ?

user21820

@F.Zer What problem? You could easily have used some other variable name...

F. Zer

@user21820 Like Let a ∈ ℕ such that P(a) ?

I can't remember which rule is blocking what I just did in my proof skeleton.

Specifically this: you used "m" in a quantifier after you have declared it in an ∃elim.

user21820

4:57 PM

@F.Zer Well the syntax rules. "¬∃m∈ℕ ( P(m) ∧ ∀k∈ℕ ( P(k) ⇒ k≥m ) )" is simply syntactically invalid because "m" is already used.

@F.Zer Yes.

F. Zer

@user21820 I I can't find the specific rule. Is it in your post, or in the repository ?

user21820

Sep 26 at 20:10, by user21820

A : bool ⊢ ¬A : bool
A,B : bool ⊢ A∧B : bool
A,B : bool ⊢ A∨B : bool
A,B : bool ⊢ A⇒B : bool
A,B : bool ⊢ A⇔B : bool
Given x∈S ⊢ x∈S : bool
( Given x∈S ⊢ A : bool ) ⊢ ∀x∈S ( A ) : bool
( Given x∈S ⊢ A : bool ) ⊢ ∃x∈S ( A ) : bool
[v is a used variable] ⊢ v : term
t,u : term ⊢ t=u : bool
t[1],...,t[k] : term ; [f is a k-input function-symbol] ⊢ f(t[1],...,t[k]) : term
t[1],...,t[k] : term ; [Q is a k-input predicate-symbol] ⊢ Q(t[1],...,t[k]) : bool

F. Zer

I was looking at exactly this. It wasn't far :-)

user21820

But you don't really need to see the rule to know that you shouldn't do it; if "m" is already used to refer to something, its value is fixed in the current context and it doesn't make sense to use it in a quantification.

F. Zer

Sure. Thank you ! But I am trying to see the smallest part where it goes wrong. Is it ∀k∈ℕ ( P(k) ⇒ k≥m ) ?

user21820

5:05 PM

No. You simply cannot conclude that what you wrote is a boolean statement, because you can't create a ∀subcontext using a used variable!

So you can't use the syntax rule ( ( Given x∈S ⊢ A : bool ) ⊢ ∃x∈S ( A ) : bool ) to get what you want because the ∀subcontext you would need is blocked by the condition on ∀sub.

F. Zer

@user21820 Oh, I didn't understand that rule, then. If you can, I'll appreciate a real world example of this rule. I have to go out of my house. I'll keep thinking and come back. Thank you for your help and see you !

user21820

Jul 24 at 17:14, by user21820

All these deductions should never be written out explicitly, but it should be how you think of the syntax rules if you want to be precise. Note that the ∀sub rule ensures you cannot have nested quantification of the same variable. For example you cannot do:

Jul 24 at 17:15, by user21820

Given x∈S:
  Given x∈T:  [forbidden!]
    Q(x) : bool
  ∃x∈T ( Q(x) ) : bool
∀x∈S ( ∃x∈T ( Q(x) ) ) : bool

Forbidden by the ∀sub rule.

The point is, if you want to use the ⇒sub rule to write "If A:", it requires a boolean statement, meaning that you must deduce "A : bool". But in your case, you can't, because you cannot use the ∀sub rule to write "Given m∈ℕ:".

4 hours later…

F. Zer

8:53 PM

@user21820 Awesome explanation. Thank you so much.

« first day (1266 days earlier) ← previous day next day → last day (923 days later) »

all rooms