« first day (1210 days earlier)      last day (964 days later) » 

12:13 AM
The first comment explains why fixpoint combinators like Y can't be well-typed in Haskell. The most (and only) answer shows a solution.
 
 
7 hours later…
7:40 AM
I am wondering can someone help with this simple question: math.stackexchange.com/questions/4236390/…
 
@F.Zer That's incorrect. Just because Haskell cannot do it doesn't mean it's impossible to be purely functional.
@Node.JS What you wrote is frankly meaningless. As I said:
22 hours ago, by user21820
@Node.JS I am in agreement with points (2) and (3) of the answer posted at that thread. Also, you need to learn very basic FOL first, including what precisely variables and quantifiers mean, before you even attempt to express statements about more complicated things like context-free grammars. If you learn basic FOL properly, you will never again need to ask others how to express something, regardless of which area of mathematics it is in. But if you do not, you will always be unsure how to.
The thing you wrote in your second question is not even a syntactically correct expression, much like writing "rurxfful" and asking whether it is a correct English word...
 
8:05 AM
Then please show me the right way. Please 🙏
 
@Node.JS I already said what the right way is... You need to learn basic FOL. Nothing else is the right way.
 
9:00 AM
@user21820 I dont understand this video about The Flaw in Reductio Ad Absurdum.
From the timestamp 11:11 , the author seems to conclude at the end that "everything we know and will ever know stands on pillars of salt and sand".
 
@Prithubiswas Well, I seem to recall that the author "Sen Zen" is a semi-crank, and this video only supports this judgement.
While we of course cannot non-circularly justify the axioms of PA, we can still definitively and irrefutably claim that PA seems to hold in the real world at least at human scales, under any reasonable interpretation of the symbols (e.g. by interpreting them as operations done on numbers stored in a computer built with extensible memory).
And we can certainly claim that the real world obeys classical logic (regardless of whether there is a real-world model of PA).
So it would be foolish for anyone to claim that LEM fails unless it is not a statement about the real world.
Since irrationality of sqrt(2) is trivially expressible as the arithmetical sentence (PA4) ∀k,m∈ℕ ( k·k = m·m·2 ⇒ k = 0 ), we can translate it to a claim about the real world, to which LEM certainly applies.
 
@user21820 From the timestamp , the author seems to have the following line of reasoning:

Reducio ad absurdum> liar paradox > self referential statement > classical logic doesnt work.

But I feel like the main issue here is that the author did not use symbols to express the logical statements , but instead used plain english , which I think is the reason for the "paradoxes".
 
Of course. Nobody who truly understands basic logic will think there is any paradox at all.
At the most, there can be axioms that we cannot justify, but we will never actually find a paradox.
 
9:16 AM
@user21820 wait , have I understood correctly the problem with the video?
 
@Prithubiswas Sort of. It's hard to pinpoint errors by people who do not use logical reasoning.
And there is no paradox in purely logical reasoning.
But I don't think it's a fault of English or any human language per se, but simply a fault of the author being illogical.
One can be very logical even in plain English.
2
@Prithubiswas: But perhaps you missed the fact that you cannot get the liar paradox without assuming something that doesn't exist in the first place.
It's like saying "Let P be a person who is not a person." and then telling everyone that "Mathematics is broken now."...
That's exactly what people who claim the "liar paradox" is a paradox are doing.
 
@user21820 Now it seems like the issue is much deeper than I thought. Do you have some resourses to study about this?
 
Wait why do you think it is deep? People who are illogical complain that they can say "Let U be a magical unicorn." and then find a problem, but that's because that statement was illogical because they didn't justify existence of any magical unicorn.
Similarly, they can write nonsense such as "This statement is false." but it just remains a nonsensical string and not a logically valid statement.
I also can write nonsense such as "iejfurvil". It doesn't automatically gain meaning just because I wrote it.
 
9:32 AM
@user21820 I meant "deep" to be subjective to me personally.
 
Ah.
Note that such confusion is rampant. That's why I am quite insistent on a reasonable degree of precision, including distinguishing between "1+1" and 1+1.
 
I found a MSE answer Paradoxes of yours.
Can I read it to gain some insight?
 
Sure, but I'm not sure how much of it is accessible to you right now beyond the first part.
It's because I couldn't be bothered to explain in detail why I said "Which is clearly invalid because we have not proven that such a sentence exists."..
So I went on to the stuff about provability, which isn't relevant to the original totally illogical "liar paradox".
@Prithubiswas: I guess the key point is that there are symbol strings that may appear at first glance to be meaningful statements, but may not be if one is logically careful.
"This statement is false." appears meaningful to people untrained in basic logic because it is completely grammatical.
But it is meaningless because "is false" is not a meaningful question that we can ask about "this statement".
On the other hand, people who know a good amount of mathematics (and hence vaguely know basic logic) may wrongly think that the error is in self-reference. But Quine's paradox as explained in that linked post does not have self-reference.
 
10:05 AM
@user21820 "But it is meaningless because "is false" is not a meaningful question that we can ask about "this statement" ". I did not seem to understand it.Can you elaborate it a bit more ?
 
@Prithubiswas "This unicorn is white." is of the same kind.
 
Why it is not a meaningful question? (just to clarify)
 
Because "this unicorn" is not a meaningful reference to an object that has a colour property.
 
what about "this unicorns skin"?
 
Similarly, for the liar paradox there is no way to interpret it such that "this statement" refers to an object with a boolean truth-value.
@Prithubiswas Did you miss an apostrophe?
 
10:11 AM
Yes
 
What do you think?
 
about what?
 
What do you think is the answer to your own question?
 
Oh ok. To me , "this unicorns skin" seems to be imprecise.
 
Yes but more than that. If "X" is not a meaningful reference, then how can "X's skin" be meaningful?
 
10:18 AM
Because here "X" does not exist?
Like the unicorn?
 
Yes.
The reaction to such statements (including the 'liar paradox') should all be the same: What on earth does it mean?
The "unicorn" example was just to make it as obvious as possible.
 
So , "This statement" and "this unicorn" is meaningless because we did not define it.
 
That's correct. It's not possible to define "this statement" in the 'liar paradox' such that it has a boolean truth-value.
The linked post says you can't let it be P such that P ⇔ ¬P, because obviously such P doesn't exist.
If you merely define it to be the string of symbols "This statement is false.", then you cannot justify that it has a boolean truth-value, so the "is false" part becomes meaningless.
Either way something is logically invalid.
@user21820 @F.Zer: I just realized that what I thought was an error was not at all an error... Lol!
 
11:09 AM
@F.Zer: In fact, my proof can be shortened a bit, as I realized when I posted this:
0
A: What is the shortest proof that there is an irrational number?

user21820I realized that in your case there is a better approach than Joe's answer. Since you have the full completeness axiom, you should not apply it to a set of rationals. Rather, you should apply it to $E = \{ x : x∈ℝ ∧ x^2 < 2 \}$. Then you can much more easily prove that its supremum $t$ satisfies $...

 
11:22 AM
Let S = { x : x∈ℝ ∧ x·x ≤ 2 }.
1·1 ≤ 2.
1 ∈ S.
S ≠ ∅.
Given x∈S:
	If x > 2:
		x > 0.
		2 > 0.
		x·x > x·2 > 2·2 = 4 > 2 ≥ x·x.
		⊥.
	x ≤ 2.
S ≤ 2.
Let m∈ℝ such that S ≤ m ∧ ∀u∈ℝ ( S ≤ u ⇒ m ≤ u ).  [completeness]
1 ≤ m.  [by S ≤ m]
//m ≤ 3/2.  [by ∀u∈ℝ ( S ≤ u ⇒ m ≤ u ) and S ≤ 3/2]
If m·m > 2:
	[we shall show that m is not the least upper bound for S]
	Let e = (m·m−2)/2.
	e > 0.
	e/m > 0.  [otherwise e = (e/m)·m ≤ 0·m = 0]
	m−e/m < m.
	m−e/m > 0.  [because e < e·2 < e·2+2 = m·m]
	[we shall show that m−e/m is a smaller upper bound for S than m]
 
 
1 hour later…
12:25 PM
@user21820 That's great. I'll save it for later. It would be good to return to it when I reach supremum concept.
@user21820 Yes, that's a good point. Closures are certainly possible in Haskell. The issue is that the Haskell compiler has to know types in advance. So, I don't think the application "X X" can be well-typed in a functional language that enforces strict typing. But I don't know other purely functional programming languages.
@user21820 Regarding the issue about Q10 lemma, after giving it some thought I think yours is probably the best solution. After all, axioms are available in the global context. It wouldn't be very convenient to make a big conjunction with every axiom in the antecedent :-)
 
12:44 PM
@user21820 I am hand evaluating the fixed-pointer operator. You were right; it's not above my current level. Thank you for the confidence.
@user21820 However, when I evaluate fix(F)(2), I get 2 instead of 3.
I must be doing something wrong.
Oh, it's + k, not + 1. I will try again.
Rewriting your function in this way:
const fix = F => {
    const D = X => F(
        t => X(X)(t)
    )
    return D(D)
};

const F = Y =>
    k => (k === 0) ? (
        0
    ) : Y(k - 1) + k;
I proceed with evaluation:
fix(F)(2)
= D(D)(2)
= F(t => D(D)(t))(2)
= (t => D(D)(t))(2-1) + 2
= D(D)(1) + 2
= F(t => D(D)(t))(1) + 2
= ((t => D(D)(t))(1-1) + 1) + 2
= (D(D)(0) + 1) + 2
= (0 + 1) + 2
= 3
Do you think is it something like that ?
 
1:34 PM
(1)
Given a,b,c∈ℕ
	If a<b ∨ a=b
		If a<b
			a+c<b+c
			a+c<b+c ∨ a+c=b+c
		If a=b
			a+c=b+c
			a+c<b+c ∨ a+c=b+c
		a+c<b+c ∨ a+c=b+c
	a<b ∨ a=b ⇒ a+c<b+c ∨ a+c=b+c
	a≤b⇒ a+c≤b+c
∀x∀y∀z(x≤y⇒ x+z≤y+z)

(2)
Given a,b,c∈ℕ
	If a<b ∧ (b=c ∨ b<c)
		If b=c
			a<b
			a<c
		If b<c
			a<b
			a<c
		a<c
	a<b ∧ (b=c ∨ b<c) ⇒ a<c
	a<b≤c ⇒ a<c
∀x∀y∀z(x<y≤z ⇒ x<z)

(3)
Given a,b,c∈ℕ
	If (a<b ∨ a=b) ∧ b<c
		If a<b
			b<c
			a<c
		If a=b
			b<c
			a<c
		a<c
	(a<b ∨ a=b) ∧ b<c ⇒ a<c
	a≤b<c ⇒ a<c
∀x∀y∀z(x≤y<z ⇒ x<z)   \
@user21820 Are these proofs correct?
 
1:48 PM
I believe those 4 proofs are correct, but let's wait for @user21820 opinion since I am just a novice in these things :-)
Just remember that subcontext headers end with a colon.
 
2:27 PM
@F.Zer Yes that's right.
@Prithubiswas Yes, but you could have done the 4th one faster by using one of the earlier ones.
Or collapsing the second case in your proof. You have b ≤ c, so if a = b then immediately a ≤ c.
@F.Zer So do you understand how the magic works yet?
 
3 white edges from a vertex ⇒ black triangle.
  ∀ a,x,y,z ∈ V ( ¬c(a,x) ∧ ¬c(a,y) ∧ ¬c(a,z) ∧ x ≠ y ∧ x ≠ z ∧ y ≠ z ⇒ c(x,y) ∧ c(y,z) ∧ c(z,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 )
    ∀ x,y,z ∈ V ( c(x,y) ∧ c(y,z) ∧ c(z,x) ⇒ x = y ∨ y = z ∨ z = x ) [no triangle]
    Given a,x,y,z ∈ V:
      If ¬c(a,x) ∧ ¬c(a,y) ∧ ¬c(a,z) ∧ x ≠ y ∧ x ≠ z ∧ y ≠ z:
        ¬c(y,a) ∧ ¬c(y,x)
        c(y,x)
        ¬c(z,a) ∧ ¬c(a,x)
        c(z,x)
@user21820 for k ≥ 2 ?
 
@F.Zer In general
 
@user21820 Where's the magic ?
I am not sure I found it.
Before understanding how it works, I should find where it is, I think.
There seems to be a "recursion like" pattern, there.
There is a base case that returns 0, and in every other case, the value of Y(k-1) is increased by k.
 
Well of course to fully understand it you're going to have to understand the proof I gave you.
The example is just for a crutch.
 
@user21820 Oh, I see. I will look again at the proof.
 
2:37 PM
You can observe that the example F really does satisfy (✻).
 
@user21820 How did you check that F satisfies (✻) ?
 
@F.Zer Well for now just do it mentally. The example F(Y) returns a function that only uses the input Y as a function, so of course if Y and Z have the same behaviour then F(Y) and F(Z) have the same behaviour.
 
@user21820 Perfect.
 
Tthe example evaluation you did relies on this fact when you went from (t => D(D)(t))(2-1) + 2 to D(D)(1) + 2.
Well, sort of. Hard to see it completely when it's all partly evaluated.
 
2:55 PM
@user21820 I can't think of an F, with a different definition, that would make this fail.
Assuming Y and Z both have the same behaviour, that is.
 
@F.Zer It can't happen in ordinary cases, of course. It can happen if F(Y) looks at Y itself instead of just using it as a function. JS can do that.
Like say if Y.toSource() equals something...
 
@user21820 I see.
@user21820 I would like to ask you a kindergarten question. I went to the bank, and said to the agent: "The bank is charging me 65% of taxes for this purchase". But the agent replied: "That's incorrect. We are taking 35 percent of the purchase, 30 percent of the purchase, and then adding those results. That's a different thing". What do you think ?
 
Lol?
 
@user21820 I think the agent is wrong. Could you tell me your opinion ?
They both return the same value, I think.
 
If they are really making you pay an additional 65%, why do you merely think they are wrong?
Why can't you just ask them how much tax they charge for $100?
 
3:02 PM
@user21820 Well, he is claiming 65x/100 ≠ 35x/100 + 30x/100. That would be a math mistake.
I am interested in the math aspect of it.
 
Are you being serious? You can do proofs in PA but have doubt here?
Unless you are talking about rounding, but you didn't mention that...
 
@user21820 I am confident that he is wrong. But, as he does calculations all day...
 
Well, sometimes it is okay to judge someone else as wrong even if they claim to be more competent than you.
The only difference possible is via rounding, and that's all there is.
 
No, there is no rounding. I will give you the complete picture. My country charges (in a specific kind of purchase), two kind of taxes (A and B):
- A is 30 percent of that purchase
- B is 35 percent of that purchase
I said to the agent: I am being charged 65% per purchase, in that case. He said that I was wrong.
A and B are added, of course. So, he insisted that A + B wasn't equal to 65 percent of that purchase.
 
There is rounding in real life. They don't charge fractional cents, and in cents round(A+B) may not be round(A)+round(B).
That's why...
6 mins ago, by user21820
Why can't you just ask them how much tax they charge for $100?
 
3:09 PM
@user21820 Oh, that's great. Thank you so much !
However, I can't be confident that he knows 65x/100 = 35x/100 + 30x/100.
But, your point could be the key.
 
If you have nothing better to do, you could ask him whether the difference is at most one cent. If he says "no", then you can tell him "you are wrong and illogical". If he says "don't know", then you can explain to him the mathematics.
 
@user21820 Well, that seems the solution to this issue. Asking what's the difference in cents and how much tax they charge for $100. Thank you for your insight !
@user21820 Do you think my second attempt at Q10 lemma is good ? Has it improved ?
I should go out a moment. See you and thanks for your help !
 
@F.Zer Well, it is a bad idea to just post it without the actual subcontext containing that lemma. And, no, it's wrong with multiple errors.
1 message moved to Sandbox
 
4:07 PM
@user21820 Sorry about that. Is my translation of "there is no triangle" incorrect ?
I will remember about adding sub contexts when I post it here.
 
@F.Zer Well... the claim does not match the conclusion, and also you made intuitive leaps that aren't backed by proof. Maybe I missed the errors in your earlier version as well.
 
5:07 PM
@user21820 I made another attempt at the lemma, below.
∀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 ) ∨ ∃x,y,z,w,u ∈V ∀t∈V ( t = x ∨ t = y ∨ t = z ∨ t = u ⋁ t = w ), where c : V^2→Bool.
  If ∀x,y∈V ( c(x,y) ⇒ c(y,x) ) ∧ ∀x,y,z∈V ( c(x,y) ∨ c(y,z) ∨ c(z,x) ):
    If ¬∀w∈V ∃x,y,z∈V ( c(x,y) ∧ c(y,z) ∧ c(z,x) ∧ x ≠ y ∧ y ≠ z ∧ z ≠ x ):
      ∀x,y,z∈V ( c(x,y) ∨ c(y,z) ∨ c(z,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 ) )
 
5:19 PM
Upvoted this answer since I think it is excellent: math.stackexchange.com/questions/1667884/…
@user21820 Could you please explain how did you do the last proof ?
 
@F.Zer I'm not sure what you're asking; the last proof in that post is just using ¬intro and ¬¬elim.
 
@user21820 Specifically, how did you go from "If ¬A:" to Contradiction.
 
@F.Zer I wrote:
> [Suppose from "¬A" you can derive "Contradiction".]
 
@user21820 Oh, I get it, now. You are assuming "¬A ⊢ ⊥". I am not used to those kinds of meta-assumptions :-)
 
Yes that post was supposed to justify proof by contradiction, so you start with such an assumption and convince people that it is correct to deduce "A".
 
5:33 PM
Good.
 
And as revealed there, it only works when you can convince them that "A" has a boolean truth-value.
> [I]f you believe that the statements you can make have meaning in the real world, then [LEM] obviously holds because the real world either satisfies a statement or its negation, regardless of whether you can figure out which one.
 
@user21820 That's important, I think. Good to realise that.
 
So if you have a mathematical statement that does not clearly have meaning in the real world, then you would have to work extra hard to convince someone (e.g. me) that it satisfies LEM.
 
@user21820 Could you give an example ?
 
For arithmetical statements, I'm relatively happy with assuming LEM for them as per what I said to Prithu.
 
5:38 PM
Good.
@user21820 Before leaving, could you tell me if my latest attempt is closer to what you'd expect ?
 
But I'm quite unconvinced that there is a real-world interpretation of the "Set Theory" in the system you've been using, though it is equivalent in strength to ZFC, which is the current standard foundation for mathematics. This doesn't mean that I'm unconvinced by real analysis, since the most dubious axioms are replacement (which is completely unnecessary for all ordinary mathematics).
Some people have investigated non-classical versions of ZFC, but I find most of those equally dubious because they still have some form of replacement, which just doesn't make sense to me.
So far you have only used comprehension and some other innocuous axioms, and for the purposes of real analysis you will only need a fixed number of uses of powerset, so it hardly scratches the surface of what ZFC can do.
 
That's very interesting
 
@F.Zer You definitely can't prove what you want in the second-last line. The other error is 'gone' because now you have ∀x,y∈V ( c(x,y) ⇒ c(y,x) ) in the governing assumptions, and I hope you noticed that you were using it everywhere.
 
@user21820 Sure. You're right. I used the fact that I was working with an undirected graph.
 
You would need to use the lemma repeatedly, under the assumption that the final conclusion fails, and you can't prove the second-last line in absence of the failure of the conclusion.
So you shouldn't have that wrong line there.
Well, if you finish the whole proof then you'll see.
 
5:48 PM
@user21820 So, this is wrong.

∀ a,x,y,z ∈ V ( ¬c(a,x) ∧ ¬c(a,y) ∧ ¬c(a,z) ∧ x ≠ y ∧ x ≠ z ∧ y ≠ z ⇒ ⊥ )
...
∀w∈V ∃x,y,z∈V ( c(x,y) ∧ c(y,z) ∧ c(z,x) ∧ x ≠ y ∧ y ≠ z ∧ z ≠ x )
Those "..."
This should be correct:
∀ a,x,y,z ∈ V ( ¬c(a,x) ∧ ¬c(a,y) ∧ ¬c(a,z) ∧ x ≠ y ∧ x ≠ z ∧ y ≠ z ⇒ ⊥ )
...

∀w∈V ∃x,y,z∈V ( c(x,y) ∧ c(y,z) ∧ c(z,x) ∧ x ≠ y ∧ y ≠ z ∧ z ≠ x )
⊥ should be immediately above the last line.
 
??
 
@user21820 I mean, the last line below "¬∀w∈V ∃x,y,z∈V ( c(x,y) ∧ c(y,z) ∧ c(z,x) ∧ x ≠ y ∧ y ≠ z ∧ z ≠ x ):" should be ⊥.
@user21820 I should leave, now. I hope you have a nice day and take care ! See you next time !
If that is not the error you had in mind, I will fix later.
 
Fix later.
 
 
4 hours later…
9:35 PM
∀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 ) ∨ ∃x,y,z,w,u ∈V ∀t∈V ( t = x ∨ t = y ∨ t = z ∨ t = u ⋁ t = w ), where c : V^2→Bool.
  If ∀x,y∈V ( c(x,y) ⇒ c(y,x) ) ∧ ∀x,y,z∈V ( c(x,y) ∨ c(y,z) ∨ c(z,x) ):
    If ¬∀w∈V ∃x,y,z∈V ( c(x,y) ∧ c(y,z) ∧ c(z,x) ∧ x ≠ y ∧ y ≠ z ∧ z ≠ x ):
      ∃w∈V ¬∃x,y,z∈V ( c(x,y) ∧ c(y,z) ∧ c(z,x) ∧ x ≠ y ∧ y ≠ z ∧ z ≠ x )
      Let w' ∈ V such that ¬∃x,y,z∈V ( c(x,y) ∧ c(y,z) ∧ c(z,x) ∧ x ≠ y ∧ y ≠ z ∧ z ≠ x )
@user21820 This is my latest attempt. The current problems are: I am not using the fact that the number of vertices > 5 (≥ 6) and I didn't manage to prove an arbitrary k has at least 3 white edges or it has at least 3 black edges.
 

« first day (1210 days earlier)      last day (964 days later) »