« first day (1200 days earlier)      last day (1283 days later) » 

09:35
@F.Zer If you can't figure it out I can give you more details.
I'm not actually surprised that you didn't know the 'best' proof of the quadratic equation, because from my experience I know there are lot of such gaps in high-school mathematics education, almost everywhere. But it's slightly surprising that even wikipedia didn't have the version of the proof I prefer...
 
2 hours later…
11:16
@user21820 Yes, please. Give me more details. Inside the case: "If 2·a·x+b = 0:", I reached: "0 = b^2−4·a·c".
Could you first explain how do you complete the square ?
@user21820 I've read many step-by-step explanations but it never stuck with me.
 
1 hour later…
12:32
@F.Zer Why do you have such a case? I didn't mention such a case, nor did you in the related proof.
@F.Zer I did that part for you already. Just look at the algebraic manipulations I did, and fill in the (easy) intermediate steps. In case you didn't get the first step, it's simply multiplying by 4·a.
@F.Zer I don't think there is a need to 'learn' about "completing the square", since the entire technique is already contained in this very algebraic manipulation I gave you. As long as you understand every step, and see how the steps make the final equation only have a single occurrence of "x", that is essentially all there is to completing the square.
Here is an outline. Fill in all the blanks.
∀x∈ℝ[≥0] ( sqrt(x)∈ℝ[≥0] ∧ sqrt(x)^2 = x ).  [property of square-root]
Given x,y∈ℝ:
	If x^2 = y:
		...
		y ≥ 0.
		...
		(x−sqrt(y))·(x+sqrt(y)) = 0.
		...
		[follow the same argument as in your own proof earlier]
Given x∈ℝ:
	If a·x^2+b·x+c = 0:
		...
		(2·a·x)^2+4·a·b·x+4·a·c = 0.
		...
		(2·a·x+b)^2 = b^2−4·a·c.
		...
		[use the above lemma]
		2·a·x+b = ... ∨ 2·a·x+b = ... .
		...
		x = ... ∨ x = ... .
	If b^2−4·a·c ≥ 0 ∧ ( x = ... ∨ x = ... ):
		...
		a·x^2+b·x+c = 0.
 
1 hour later…
13:58
@user21820 Yes, you didn't mention that case. However, I was trying a few things.
@user21820 Yes, I noticed you used some kind of "completing the square". It's good that there is not need to learn about it. Your algebraic manipulation was very clear to me. I wondered about your thoughts on it.
@user21820 Thank you for the outline ! I will fill the blanks.
If ∀x∈G∀y∈G∀z∈G(x*(y*z)=(x*y)*z)∧∀x∈G∀y∈G(x*i(x)=y*i(y))∧∀x∈G(x*(x*i(x))=x)
    ∀x∈G∀y∈G∀z∈G(x*(y*z)=(x*y)*z)
	∀x∈G∀y∈G(x*i(x)=y*i(y))
	∀x∈G(x*(x*i(x))=x)
	Given a∈G
	     Given b∈G
		      a*(a*i(a))=a
			  a*i(a)=i(a)*i(i(a))
			  a*(i(a)*i(i(a)))=a
			  (a*i(a))*i(i(a))=a
			  (i(a)*i(i(a)))*i(i(a))=a

			  i(i(a))*(i(i(a))*i(i(i(a))))=i(i(a))
			  i(i(a))*i(i(a))=i(i(a))*i(i(a))
			  i(i(a))*i(i(a))=(i(i(a))*(i(i(a))*i(i(i(a)))))*i(i(a))

			  (i(a)*i(i(a)))*i(i(a))=a
			  i(a)*i(i(a))=i(i(a))*i(i(i(a))
@user21820 This is how far I was able to get with (Q9) .And I feel like I have hit a dead end. Can you show a hint?
@Prithubiswas The idea behind solving (Q9) is to make use of the given conditions to simplify the proof search.
The first condition (which you know is associativity) means that we can drop all brackets involving the operation ✻.
The second condition implies that we can consider anything of the form "t✻i(t)" as equal.
The third condition should be used as a reduction, namely x✻x✻i(x) → x, which by the second condition generalizes to x✻y✻i(y) → x.
So the first thing we should try is to find a term that can be reduced in different ways to get some new fact.
Obviously, we would need a term with 4 subterms or more, so try 4 first!
Can you find such a term?
14:17
@user21820 That sort of feels like brute-forcing. Or is it intuitive?
Well, you could say it is brute-forcing, but the answer pops out very fast because the canonicalization technique is used to its fullest potential.
14:42
@user21820 This is the proof of the lemma, I think.
I made a typo. Will fix
∀x,y∈ℝ ( x^2 = y ⇒ x = sqrt(y) ∨ x = –sqrt(y) ) [lemma]
  ∀x∈ℝ[≥0] ( sqrt(x)∈ℝ[≥0] ∧ sqrt(x)^2 = x ).  [property of square-root]
  Given x,y∈ℝ:
    If x^2 = y:
      If x ≠ 0:
        x^2 > 0 [lemma]
        y > 0
        y ≥ 0
      If x = 0:
        x·0 = 0 [lemma]
        x·x = 0
        y = 0
        y ≥ 0
      y ≥ 0.
      sqrt(y)∈ℝ[≥0] ∧ sqrt(y)^2 = y
      x·sqrt(y) ∈ ℝ
      x^2+x·sqrt(y) = y+x·sqrt(y)
      x^2+x·sqrt(y)–x·sqrt(y)–y = 0
      (x+sqrt(y))·(x–sqrt(y)) = 0.
      If ¬( x = sqrt(y) ∨ x = –sqrt(y) ):
@user21820 I fixed the proof. Could you tell me what do you think ?
@F.Zer Well you're supposed to have proven ∀x∈ℝ ( x^2 ≥ 0 ) first, instead of always doing it again. I think this is the second time you did it, and you shouldn't do anything twice. =)
Similarly, you could alternatively just use LEM to split-cases on x = sqrt(y), instead of basically repeating the LEM proof. If x = sqrt(y), then conclusion. If x ≠ sqrt(y), then x−sqrt(y) ≠ 0 so x+sqrt(y) = (x+sqrt(y))·(x–sqrt(y))·(1/(x–sqrt(y))) = 0·(1/(x–sqrt(y))) = 0, and then conclusion.
But as a proof it is correct.
15:01
@user21820 Oh, I did prove it. Forgot to tag it as [lemma].
∀x,y∈ℝ ( x^2 = y ⇒ x = sqrt(y) ∨ x = –sqrt(y) ) [lemma]
  ∀x∈ℝ[≥0] ( sqrt(x)∈ℝ[≥0] ∧ sqrt(x)^2 = x ).  [property of square-root]
  Given x,y∈ℝ:
    If x^2 = y:
      x^2 ≥ 0 [lemma]
      y ≥ 0.
      sqrt(y)∈ℝ[≥0] ∧ sqrt(y)^2 = y
      x·sqrt(y) ∈ ℝ
      x^2+x·sqrt(y) = y+x·sqrt(y)
      x^2+x·sqrt(y)–x·sqrt(y)–y = 0
      (x+sqrt(y))·(x–sqrt(y)) = 0
      If x = sqrt(y):
        x = sqrt(y) ∨ x = –sqrt(y)
      If x ≠ sqrt(y):
        x–sqrt(y) ≠ 0
        x+sqrt(y) = (x+sqrt(y))·1 = (x+sqrt(y))·(x–sqrt(y))·(1/(x–sqrt(y))) = 0·(1/(x–sqrt(y))) = 0
@user21820 Those are great ideas. Are you using the contrapositive of this lemma: "∀ x,y ( x–y = 0 ⇒ x = y)" when deriving "x–sqrt(y) ≠ 0" ?
@F.Zer Oh good.
@F.Zer Yes, that's right. It's just two steps so no point having a lemma here.
After all, the goal is to skip all the steps that you know 100% well how to fill in, but leave the core logical structure and the key steps.
@user21820 Thank you. That seems like a fantastic mindset in the long run. Otherwise, the proof of simple facts would be 10 pages long.
I will work on the quadratic proof and come back.
Sure. See you!
See you !
If ∀x∈G∀y∈G∀z∈G(x*(y*z)=(x*y)*z)∧∀x∈G∀y∈G(x*i(x)=y*i(y))∧∀x∈G(x*(x*i(x))=x)
   ∀x∈G∀y∈G∀z∈G(x*(y*z)=(x*y)*z)
   ∀x∈G∀y∈G(x*i(x)=y*i(y))
   ∀x∈G(x*(x*i(x))=x)
   Given a∈G
      a*(a*i(a))=a
      a*i(a)=i(a)*i(i(a))
      a*(i(a)*i(i(a)))=a
      (a*i(a))*i(i(a))=a
      (i(a)*i(i(a)))*i(i(a))=a

      i(i(a))*(i(i(a))*i(i(i(a))))=i(i(a))
      i(i(a))*i(i(a))=i(i(a))*i(i(a))
      i(i(a))*i(i(a))=(i(i(a))*(i(i(a))*i(i(i(a)))))*i(i(a))

      (i(a)*i(i(a)))*i(i(a))=a
      i(a)*i(i(a))=i(i(a))*i(i(i(a))
@user21820 attempt at Q9.
15:16
@Prithubiswas That's fast, did you find the answer using my hints or via another method?
I haven't checked yet, so I'm just asking first.
Can you first check first? By the way I did not use your method.
@Prithubiswas Oh ok. Well it certainly looks longer than it should be.
Typing error at "(i((a))*i(i(i(a)))*i(i(a))=a".
15:32
So if you do what I said above and furthermore write i(t) as t', what you did in the first part was nothing more than:
a''a'' = a''a''a'''a'' = a''a'a''a'' = a''aa'a'' = a''aaa' = a''a.
a'a'' = a'a'a''a'' = a'a'a''a = a'a.
a'aa = a'a''a = aa''a'' = a.
And of course after that it is easy.
If you used my method instead, it would only take one try:
The shortest 4-part term that has two reductions yields yx = yxx'x'' = yx''. To maximize the use of the second condition, we apply it to y = x', yielding x'x = x'x'' = xx'. And then after that it is equally easy.
So, you managed to solve it by brute-force, though the goal of that exercise was to learn how to search efficiently via canonicalization.
I haven't ever heard of the word "canonicalization".
@Prithubiswas Then it's time for you to learn it! It is an extremely powerful technique that can be used in all areas of mathematics. It basically means to define canonical forms and use them to represent all cases.
What I told you above is an example:
2 hours ago, by user21820
The first condition (which you know is associativity) means that we can drop all brackets involving the operation ✻.
2 hours ago, by user21820
The second condition implies that we can consider anything of the form "t✻i(t)" as equal.
The first means that we don't consider "x✻(y✻z)" and "(x✻y)✻z" as different, even though they are different. Why can we do that? Because of the first condition.
The second does the same for terms of the form "t✻i(t)".
When we search for a term that can be reduced via the third condition:
2 hours ago, by user21820
The third condition should be used as a reduction, namely x✻x✻i(x) → x, which by the second condition generalizes to x✻y✻i(y) → x.
The notion of "reduction" is based on canonicalization as well. The idea is that we want to reduce all cases to a "canonical form". Sometimes we do it by equivalences (as in the first two). Other times we do it via reduction to a simpler form (as in the third).
And because of the second condition, this reduction can be generalized as I stated.
This reduction needs a 3-part term, and reduces it to 1 part. So if we want two different results we need a 4-part term, and it must be of the form y✻x✻i(x)✻i(i(x)).
Because we want to be able to reduce the first 3 parts, and also the last 3 parts.
Choosing "y" in front is to make it as general as possible, to cover as many cases as possible. (And if you think about it, it's the only 4-part term that we need to try.)
The two reductions yield yx = yxx'x'' = yx''. (I'm lazy to type the operation.)
So after that the rest is easy.
@Prithubiswas: For another example of canonicalization that you might be familiar with even without understanding it, think of how you prove trigonometric identities in high-school.
Mar 7 at 10:16, by user21820
For example, if to prove a high-school trigonometric identity you can firstly replace all "tan" by "sin/cos" and "cot" likewise, and then convert to polynomial in terms of sin,cos and then use the angle-sum identities and so on, all with the goal of 'meeting in the middle'. The very action of eliminating "tan" and "cot" is part of the canonicalization mindset.
Mar 7 at 9:37, by user21820
This is an instance of the canonicalization technique, which you should learn to employ whenever possible; canonicalization just means to restrict your attention to some kind of canonical form that you can reduce every other case to. Of course, you have to figure out what is suitable to be the canonical form, but the point is to have the correct mindset in the first place.
Mar 7 at 9:38, by user21820
That is, you should already think about the useful canonical forms for anything you come across even before you face problems involving them. For instance, you came across fractions of polynomials. According to this mindset, you should have already thought about what canonical forms are convenient. One of them is what I described above, which is useful not just here but also when you want to integrate via partial fractions.
There are a lot of examples, but think through these two examples first.
 
5 hours later…
20:40
@user21820 After working on this, I have a question. I have never seen a proof like this one. You have a case: "If a·x^2+b·x+c = 0:" and then another case "If b^2−4·a·c ≥ 0 ∧ ( x = ... ∨ x = ... ):". Could you explain what is going on, here ? I do not understand what am I trying to prove. Is the last step inside the case "If a·x^2+b·x+c = 0:" used as one of the premises in the second case ?
Making a case "b^2−4·a·c ≥ 0" is sensible. The discriminant can't be less than zero.
Seems like the case "b^2−4·a·c ≥ 0" should be nested below "If a·x^2+b·x+c = 0:".
Oh, this is a biconditional !!
The outline I wrote was clearly not for a proof of an equivalence. It's up to you if you want to add stuff to make it a proof of equivalence.
And I also forgot the condition that a ≠ 0.
@user21820 Then, I do not understand which proof structure you are using.
@user21820 Wondered about that :-)
@F.Zer A proof does not have to be of anything. It's just a proof!
Given x,a,b,c∈ℝ:
	If a·x^2+b·x+c = 0 ∧ a ≠ 0:
		...
		(2·a·x)^2+4·a·b·x+4·a·c = 0.
		...
		(2·a·x+b)^2 = b^2−4·a·c.
		...
		[use the above lemma]
		2·a·x+b = ... ∨ 2·a·x+b = ... .
		...
		x = ... ∨ x = ... .
	If b^2−4·a·c ≥ 0 ∧ ( x = ... ∨ x = ... ):
		...
		a·x^2+b·x+c = 0.
Here is the updated outline.
@user21820 Oh, I think I understand. You are deriving two facts at once. Something like P ⇒ Q ∧ R ⇒ S. Of course, you are using quantifiers.
Yes ( P ⇒ Q ) ∧ ( R ⇒ S ). Precedence rules make the brackets necessary...
If you truly want an equivalence, one possibility is to move the "a ≠ 0" outside, say ∀x,a,b,c∈ℝ ( a ≠ 0 ⇒ ( a·x^2+b·x+c = 0 ⇔ ... ) ).
20:50
@user21820 Noted.
Ok I got to go.
@user21820 Thank you for the help ! See you !
@user21820 That's good.
@user21820 Sorry. Without brackets...would you read it as "P ⇒ (Q ∧ R) ⇒ S" ?
@F.Zer Don't omit brackets when you have two "⇒". There is a logician convention, but it's right-to-left, so not good.
@user21820 Sure. It makes a lot of sense. But where does a machine put brackets in "P ⇒ Q ∧ R ⇒ S" using your precedence rules ?
[infix operations],[relations including =],¬,∧,∨,{⇒,⇔}
@F.Zer If I make the parser, for pedagogical purposes I would reject it.
21:00
@user21820 Ahh. Understood. That wouldn't be a WFF for your parser.
Just know that logicians read implications from right-to-left, so that A ⇒ B ⇒ C ≡ A ∧ B ⇒ C.
21:17
@user21820 You said this twice and that is a question I have since a long time ago. Could you tell me what do you mean by "read implications from right-to-left" ? How do I read an operator ? Sorry for the really basic question.

« first day (1200 days earlier)      last day (1283 days later) »