Basic Mathematics - 2021-08-21

F. Zer

01:17

How do I read a connective, I should say.

F. Zer

08:32

@user21820 I leave the proof, here. Could you tell me what do you think ?

∀ x,a,b,c∈ℝ ( a ≠ 0 ⇒ ( a·x^2+b·x+c = 0 ⇒ ( b^2−4·a·c ≥ 0 ∧ ( x = (–b+sqrt(d))/2·a ∨ x = (–b–sqrt(d))/2·a ) ) ) ⇔ ( ( b^2−4·a·c ≥ 0 ∧ ( x = (–b+sqrt(d))/2·a ∨ x = (–b–sqrt(d))/2·a ) ) ) ⇒ a·x^2+b·x+c = 0 )
  Given x,a,b,c∈ℝ:
    If a ≠ 0:
      b^2–4·a·c ∈ ℝ
      b^2–4·a·c ∈ obj
      Let d = b^2–4·a·c [ E∈obj ⊢ y = E. [where y is a fresh variable] ]
      If a·x^2+b·x+c = 0:
        4·a·( a·x^2+b·x+c ) = 0
        4·a^2·x^2+4·a·b·x+4·a·c = 0
        (2·a·x)^2+4·a·b·x+4·a·c = 0
        4·a^2·x^2+4·a·b·x+b^2+4·a·c = 0 + b^2

user21820

15:03

@F.Zer It means that if they are at the same precedence level then the one on the right has higher precedence.

As I said, you shouldn't use such a convention.

@F.Zer There is something very wrong with your conclusion.

F. Zer

16:17

@user21820 Thank you. So, I should read it as: "A -> (B -> C)". However, I won't use that convention.

@user21820 Ohh ! I removed everything and saw the blatant error. Sorry. I will fix. What do you think, now ?

∀ x,a,b,c∈ℝ ( a ≠ 0 ⇒ ( a·x^2+b·x+c = 0 ⇔ ( b^2−4·a·c ≥ 0 ∧ ( x = (–b+sqrt(d))/2·a ∨ x = (–b–sqrt(d))/2·a ) ) ) )

Prithu biswas

@user21820 So the technique of "canonicalization" is to have a form which can be reduced in different ways. Like for example , if z is a canonical form that can be reduced in two different ways to get z=x and z=y , then we can say x=y and now we got a new fact "x=y" to use for proving our main goal. correct?

@user21820 And for proving trig identity , like x=y , We first take x and replace all "tan" and "sec" with "sin" and "cos". This gives us a canonical form z where z=x. z is a canonical form in the sense that (besides just reversing and getting to x again) it can be reduced in a different way (using trig identities involving sin and cos) to get y where z=y.So , x=z=y and x=y. correct?

user21820

@Prithubiswas The second half is correct, but it is just a consequence of the canonicalization technique rather than the technique itself.

"Canonical" simply means "standard". The canonicalization technique is simply to identify some specific cases as standard (called canonical) and identify ways to reduce other cases to those canonical cases.

Thinking in that manner encourages us to find reductions, but the initial forms are not the canonical forms.

When we reduce x✻i(x)✻i(i(x)) → x in that exercise, we are simply trying to consider "x" as the canonical form and the other as non-canonical.

The idea is that if you only have to focus on canonical forms, it is easier than dealing with all forms (including more complicated ones).

That is why we try to use the third condition as a reduction, and consider the simpler side to be "more canonical".

@Prithubiswas For trigonometric identities, indeed once you replace everything with just sin and cos, it is usually much easier to prove equality, via what you said.

In other words, we consider "tan(2x)" to be not canonical, and we would reduce it to sin(2x)/cos(2x) and then reduce further to 2·sin(x)·cos(x)/(1−2·sin(x)^2).

For reducing cos(2x) we could choose 2·cos(x)^2−1 instead, and it makes little difference because we can later eliminate any difference using cos(x)^2 + sin(x)^2 = 1.

@F.Zer It's better, but still wrong because "d" is undefined. If you look at the ∀intro rule, the "Q" must be a property in the outer context, so you can't use variables that you declared inside via ∃elim.

F. Zer

16:55

@user21820 Thank you. I will fix it.

Prithu biswas

@user21820 In this exercise:

(Q10) ∀x,y∈V ( c(x,y) ⇒ c(y,x) ) ∧ ∀x,y,z∈V ( c(x,y) ∨ c(y,z) ∨ c(z,x) ) ⇒ ∀w∈V ∃x,y,z∈V ( c(x,y) ∧ c(y,z) ∧ c(z,x) ∧ x ≠ y ∧ y ≠ z ∧ z ≠ x ) ∨ ∃v,w,x,y,z∈V ∀t∈V ( t = v ∨ t = w ∨ t = x ∨ t = y ∨ t = z ), where c : V^2→Bool.

I think there is something odd about the part:

∀w∈V ∃x,y,z∈V ( c(x,y) ∧ c(y,z) ∧ c(z,x) ∧ x ≠ y ∧ y ≠ z ∧ z ≠ x )

Because even though there is a quantifer ∀w∈V with the variable "w", there is no "w" in "c(x,y) ∧ c(y,z) ∧ c(z,x) ∧ x ≠ y ∧ y ≠ z ∧ z ≠ x".

user21820

17:11

@Prithubiswas Yes it was deliberate. If you remove the "∀w∈V", it actually becomes wrong.

Prithu biswas

@user21820 How is it wrong? Isn't ∀w∈V unnecessary?

user21820

@Prithubiswas If you remove it, the conclusion is existential, but the conditions are all universal. So it cannot be correct.

Prithu biswas

@user21820 Now I am a bit confused. In " ∀w∈V ∃x,y,z∈V ( c(x,y) ∧ c(y,z) ∧ c(z,x) ∧ x ≠ y ∧ y ≠ z ∧ z ≠ x )" , I feel like with ∀w∈V , we are quantifying over a variable w that doesn't even exist...

user21820

@Prithubiswas "∀w∈V ∃x∈V ( x = x )" is true and easily provable. But remove the ∀-quantifier and it becomes wrong. Can you see why?

Prithu biswas

I dont see how ∃x∈V (x = x) is wrong.

user21820

17:22

Really?

Prithu biswas

Yes.

user21820

V can be empty.

Prithu biswas

I guess I am missing something obvious.

empty types are allowed?

user21820

@Prithubiswas Nothing in the system requires the type to be non-empty, and the rules reflect that. You cannot prove ∃x∈V ( x = x ).

And this had better be so, because we allow any set to be a type too. If we don't allow empty types, then we would have the silly trouble of having to prove non-emptiness of a set before we can ever quantify over it. And it would be worse than silly, because we would not be able to immediately go from ∀x∈obj ( x∈S ⇒ Q(x) ) to ∀x∈S ( Q(x) ).

(But that's for later, because you haven't come to set theory yet.)

F. Zer

@user21820 I'd guess you meant P. Is this better ? Feel free to delete the other proofs, if you like.

∀ x,a,b,c∈ℝ ( a ≠ 0 ⇒ ( a·x^2+b·x+c = 0 ⇔ ( b^2−4·a·c ≥ 0 ∧ ( x = (–b+sqrt(b^2−4·a·c))/2·a ∨ x = (–b–sqrt(b^2−4·a·c))/2·a ) ) ) )
  Given x,a,b,c∈ℝ:
    If a ≠ 0:
      b^2–4·a·c ∈ ℝ
      b^2–4·a·c ∈ obj
      Let d = b^2–4·a·c [ E∈obj ⊢ y = E. [where y is a fresh variable] ]
      If a·x^2+b·x+c = 0:
        4·a·( a·x^2+b·x+c ) = 0
        4·a^2·x^2+4·a·b·x+4·a·c = 0
        (2·a·x)^2+4·a·b·x+4·a·c = 0
        4·a^2·x^2+4·a·b·x+b^2+4·a·c = 0 + b^2
        (2·a·x+b)^2 = b^2−4·a·c
        (2·a·x+b)^2 = d

user21820

17:31

@F.Zer Yea sorry. I tend to use Q in text chat to avoid confusing with P for power-set. =)

F. Zer

@user21820 Good. I used a local definition, but just before using ∀ Intro, I made use of =Elim. Is that usage sensible ?

user21820

@F.Zer Wait, you shouldn't just plug the thing back into the equation haha.. In this case you can actually follow the steps in reverse.

@F.Zer That's correct. You get rid of the variables that aren't available outside by either replacing with their definition (as in your case) or using ∃intro.

F. Zer

@user21820 Excellent.

@user21820 I will try.

user21820

In the past, you didn't face this because the exercises I gave you already tell you the desired conclusion. Here it was open-ended so you didn't realize this.

F. Zer

@user21820 Which message are you replying to ?

What's this ?

user21820

17:36

The variable problem.

F. Zer

@user21820 Oh, got it. If I have the conclusion already, there is no way to make that mistake.

user21820

From ( x = (–b+sqrt(d))/2·a ∨ x = (–b–sqrt(d))/2·a ) you can deduce 2·a·x+b = sqrt(d) ∨ 2·a·x+b = −sqrt(d), and proceed from there.

Note that the only place you would need d ≥ 0 is when you want sqrt(d)^2 = d.

F. Zer

17:49

That's great.

I am writing the modified proof.

F. Zer

18:04

If b^2−4·a·c ≥ 0 ∧ ( x = (–b+sqrt(d))/2·a ∨ x = (–b–sqrt(d))/2·a ) ):
  x = (–b+sqrt(d))/2·a ∨ x = (–b–sqrt(d))/2·a
  2·a ≠ 0
  If x = (–b+sqrt(d))/2·a:
    2·a·x+b = sqrt(d) ∨ 2·a·x+b = −sqrt(d)
  If x = (–b–sqrt(d))/2·a:
    2·a·x+b = sqrt(d) ∨ 2·a·x+b = −sqrt(d)
  2·a·x+b = sqrt(d) ∨ 2·a·x+b = −sqrt(d)
  d ≥ 0
  sqrt(d)∈ℝ[≥0] ∧ sqrt(d)^2 = d
  If 2·a·x+b = sqrt(d):
    (2·a·x+b)^2 = sqrt(d)^2
    2·a·x+b = d
    (2·a·x+b)^2 = d
    (2·a·x+b)^2 = b^2−4·a·c
    4·a^2·x^2+4·a·b·x+b^2+4·a·c = 0 + b^2

@user21820 Great. What do you think of my proof ? Did you have something similar in mind ?

user21820

@F.Zer You don't need "2·a ≠ 0", and by the way I noticed you didn't put brackets. "t/2·a" is not the same as "t/(2·a)".

Oh sorry you do need "2·a ≠ 0".

Just because of the way we set up the axioms for division.

@F.Zer You shouldn't do the same thing twice. Most of the stuff inside both cases can be factored out.

Didn't you notice that after "2·a·x+b = d" you can use ∨elim already?

Other than that, yes that's exactly the idea. You do need to check 4 ≠ 0 and a ≠ 0 so that you can do the final division, and then it's done.

F. Zer

@user21820 Yes ! I looked for ways of factoring out but couldn't find a solution.

@user21820 I can't notice that. Perhaps I am missing something.

user21820

18:21

@F.Zer It's because you did it wrong and I copied wrong too.

(2·a·x+b)^2 = d.

In both cases you get that, so why can't you use ∨elim?

Anyway I got to go.

Bye!

F. Zer

If b^2−4·a·c ≥ 0 ∧ ( x = (–b+sqrt(d))/2·a ∨ x = (–b–sqrt(d))/(2·a) ) ):
  x = (–b+sqrt(d))/(2·a) ∨ x = (–b–sqrt(d))/(2·a)
  2·a ≠ 0
  If x = (–b+sqrt(d))/(2·a):
    2·a·x+b = sqrt(d) ∨ 2·a·x+b = −sqrt(d)
  If x = (–b–sqrt(d))/2·a:
    2·a·x+b = sqrt(d) ∨ 2·a·x+b = −sqrt(d)
  2·a·x+b = sqrt(d) ∨ 2·a·x+b = −sqrt(d)
  d ≥ 0
  sqrt(d)∈ℝ[≥0] ∧ sqrt(d)^2 = d
  If 2·a·x+b = sqrt(d):
    (2·a·x+b)^2 = sqrt(d)^2
    2·a·x+b = d
    (2·a·x+b)^2 = d
  If 2·a·x+b = −sqrt(d):
    (2·a·x+b)^2 = (–sqrt(d))^2
    (2·a·x+b)^2 = (sqrt(d))^2

@user21820 I see, now ! Is that it ?

user21820

Yes.

Bye!

F. Zer

@user21820 Thank you ! Bye !

F. Zer

19:21

Finally, I made progress on this. Is this correct ? Could you tell me how can I write the final solution ?

Transcript for

♦ $Mathematics$ Basic Mathematics

Transcript for

♦ Basic Mathematics

♦ $Mathematics$ Basic Mathematics