« first day (490 days earlier)      last day (1993 days later) » 

07:38
@user21820
07:57
@Secret In that post I precisely stated what was meant by "reason about programs". I think you don't understand it. Right now, it seems better for you to go back to the basics and learn how to use FOL properly, starting with PA.
The meta-system needed to prove the incompleteness theorems must be at least as powerful as PA (in fact slightly more), so if you don't understand how to use PA formally you won't understand the incompleteness theorems.
@yh05 Solving a system of equations usually requires two parts: (1) Finding a sequence of deductions from the hypothesis that some variables form a solution to them, to some conclusions, which tells you what the solutions must be like (if there are any at all). (2) Checking which of the possible solutions found are actually solutions.
I thought so too, but I see on many occasions people skip(?) step (2).
Many people do not really know what they are doing when solving equations. And so it's unsurprising that they don't do (1) or (2) or both correctly. Other than a lack of logic, there is no other explanation.
For example, to solve x = x^2, some people might divide both sides by x. That is failure to do (1) correctly.
For another example, to solve |x| = x−1, many people might square both sides to get x^2 = (x−1)^2, and then wonder why they got nonsense. This is of course failure to do step (2).
What is wrong about dividing both sides of x=x^2 by x?
08:30
@yh05 What kind of inputs does / accept?
non zero
Non-zero second input, so you cannot simply divide by x.
But I can if I exclude the case x=0
Right, so doing (1) properly means something like this:
Given complex x such that x = x^2:
  If x≠0:
    1 = x.
  Therefore either x = 0 or x = 1.
Yes
08:34
Note that to do (1) and (2) correctly we must specify the type of x. In fact, to state the problem correctly as well, which many textbooks don't. (In my example I specified x as "complex".)
And doing (2) rigorously would be something like this:
Given complex x such that x = 0 or x = 1:
  x = x^2.
The reason is that completely solving a system of equations formally means proving an equivalence of the form ( Given x,...,y of type ..., [equation system here] iff [solution specification here] ).
In this case:
Given complex x:
  x = x^2 iff ( x = 0 or x = 1 ).
I agree too. But in many books, (2) is skipped. And I'm left wondering how the author knew with 100% confidence that the converse is true.
Unfortunately, it is too common that equation solving in high-school and even in university is never grounded in formal rigour. At best, the author writes "We check that all these are indeed solutions.".
Which is at least better than nothing.
For a university-level example, consider the various kinds of ODEs. The methods used to solve them are usually taught without any mention of the necessity of checking or proving that the obtained solutions are in fact solutions.
That also leads to some very bad conceptual errors, which sometimes cancel each other out and give the wrong impression that nothing is wrong!
For example, consider solving the ODE x·dy/dx = 2y for real variable y in terms of real variable x.
Can you see why the typical separating variables method is wrong from the beginning?
I've forgotten mostly everything about ODE.
=/
Well separating variables as taught in almost all high-schools or universities would do this:
1/y·dy/dx = 2/x
And then take anti-derivative both sides with respect to x and apply change-of-variables to get ∫(1/y)dy = ∫(2/x)dx + c for some real constant c.
So do you know what's wrong with the first step?
08:50
Dividing by xy? if xy=0?
Exactly.
And has any teacher ever told you that it's problematic here?
Most of the time, no.
Amusingly, and also sadly, almost everyone makes a mistake later that cancels this one out exactly. Let me show you.
The integral becomes ln|y| = 2·ln|x| + c for some real constant c. Then exponentiate both sides to get |y| = |x|^2·e^c = x^2·e^c.
And then they make the second mistake of replacing e^c by an arbitrary real constant k.
So |y| = k·x^2 for some real constant k.
Doing so allows for k = 0, which cancels out the earlier mistake quite by accident.
I see.
From this one may reasonably conclude (hand-wave) that we have y = m·x^2 for some real constant m, because y cannot suddenly switch sign otherwise dy/dx won't exist.
These two mistakes, together with the frequent silent cheating of the problem setter, who restricts to x ≥ 0, makes the answer correct!
But in fact, the full solution to the ODE is y = { k·x^2 if x ≤ 0 ; m·x^2 if x ≥ 0 } for some real constants k,m.
k and m may not be the same!
If one is more careful (no hand-waving) in the above fake solution, one would get the full solution, but still with those two mistakes in place.
I have more examples of pedagogical errors linked from my profile under "Common Oversights". One of them is "Teaching separating variables":
8
A: Whence the "everything is linear" phenomenon, and what can we do about it?

user21820I've read all the existing answers long ago but still feel that none have gotten to the heart of the issue. We obtain mathematical results through a process of reasoning. That reasoning must be logical and enough to convince anyone that our results are correct given our initial assumptions. That ...

In that post I explained how exactly to do separating variables rigorously, and there is another cute example ODE with a much more interesting full solution set.
09:03
Thanks, I'll take a look at it later.
Suffice to say that it is complicated, which is why ODEs shouldn't be taught to high-school students in my opinion...
I have another question.

I have been reading some books on elementary number theory recently. Sometimes the author draws some further conclusions from the conclusion(1) of a statement that is to be proved. And then, the converse works well 'accidentally', so the further conclusions turn out to be sufficient conditions for the conclusion(1).

Is this an actual problem solving method? I'm not comfortable with it.
@yh05 Could you give me an example?
Hold on.
In general, problem-solving involves not just rigorous reasoning but also intuitive guessing to formulate things to try to rigorously prove. There are many times where the easiest way to get an answer is to guess it and then find a way to prove it, because there is practically no way to obtain it blindly via purely rigorous methods.
While you search for your example, I can give you an example of what I mean, which incidentally clarifies why I said "usually requires two parts" above, because some equations cannot be solved in the 2-step manner.
> Solve x^(x+1)+x^2 = 2 for real x ≥ 0.
It is effectively impossible to solve this by algebraic means. Even if you have some arcane knowledge of the Lambert W-function and manage to do it, I can easily concoct arbitrarily more complicated examples. =P
The only way I know to solve this is by guessing the solution and then proving that it is the only solution using IVT.
09:26
I can't find a good example. Here's a not so good example.

Consider finding a $x$ such that it is congruent to $a_1$ modulo $b_1$ and also congruent to $a_2$ modulo $b_2$, whereby $b_1$ and $b_2$ are coprime. Let's suppose such a $x$ exists, then $x = a_1 + k_1\cdot b_1$ and $x = a_2 + k_2\cdot b_2$. Then, $a_1 - a_2 = k_1\cdot b_1 - k_2\cdot b_2$ (1). Because $b_1$ and $b_2$ are coprime, there are $k_1$ and $k_2$ that statement (1) is true. So indeed, the assumption that there is such a $x$ is correct.
@yh05 I guess you're uncomfortable with the guess-first strategy, but it's useful. The first time I came across this problem that you cite, I did essentially what you quoted in order to find the solution. Rigorously, we can express that in the 2-step format too:
Given integers k,m,a,b,x such that gcd(k,m)=1 and x%k = a and x%m = b:
  x = p·k+a = q·m+b for some integers p,q.
  p·k ≡ b−a (mod m).
  p ≡ (b−a)·k' (mod m) where k' is some integer such that k·k' ≡ 1 (mod m).
  p = c·m+(b−a)·k' for some integer c.
  x = (c·m+(b−a)·k')·k+a.
This is step (1), and for step (2) you just need to check that all the deductions above are reversible. What you quoted doesn't explicitly do that but it's relatively obvious since integer k1,k2 that satisfy (1) would also give an x that satisfies x = a1 + k1·b1 = a2 + k2·b2.
I prefer my solution, as it is more natural to me, but I know a lot of authors prefer using Bezout's lemma.
09:44
I'm really uncomfortable with the guess-first strategy =/
Heh. Try solving the equation I gave above; it's nearly impossible without guessing!
The prospect of (2) failing makes me 'reluctant' to use this strategy.
Ah, the key is to guess cleverly based on experience rather than guessing blindly. This would prevent getting lots of wrong candidate solutions.
(By the way, consider that the 4-colour theorem was originally a conjecture that essentially guessed the minimum number of colours needed to colour any planar graph. The proof took a long time in coming, and was so long as to be almost impossible to find it if mathematicians hadn't been so confident of the guess. In particular, the program that the mathematicians wrote to check the thousands of cases was based on the guess that 4 was enough!)
:O
The general idea was that to colour an arbitrary planar graph, you show that it has a certain type of vertex (I think it was with degree at most 5), and then based on the guess that 4 colours is enough, you examine all possible cases (with k neighbours there are at most 4·3^(k−1) possible neighbour colourings), and hope to find a way to modify the graph to get a smaller graph whose 4-colouring can be used to find a 4-colouring of the original.
If I remember correctly, just neighbour colourings are not enough, but the mathematicians proved that if 4 colours were enough then we only need to check a finite (but large) number of configurations, and then they made a computer do the hard work.
 
1 hour later…
11:19
What happens if (2) fails? The entire idea in (1) is discarded?

« first day (490 days earlier)      last day (1993 days later) »