And now 'Godel' too? (some assert that Kurt Godel effectively argued or 'proved' for a real possibility of 'reverse time travel' ?)
'Godel' help us !!
Chess will never be solved, here's why
Sort:
Apr 14, 2022
0
#3002
Apr 14, 2022
0
#3003
Actually Truth is a higher level of provability. 
This is only slightly ironic: in mathematics, this is meaningful because of the existence of alternative axiomatisations. Goedel's incompleteness theorem showed that no finite scheme of axioms can fully represent any mathematical system sufficiently rich to include the natural numbers.
What happens in practice is that any given axiom scheme in incomplete in that there are statements about the natural numbers that true but not provable in that scheme. An axiom can be added to fix such a hole, but there will always be another example.
To avoid any confusion note that this does no harm to the present discussion. We are talking about very simple statements that would be provable in any formal system representing the finite structure of chess. This is _much_ simpler in a fundamental sense than the natural numbers, which are intrinsically infinite. But what we are discussing is a formal proof of a fact about this finite structure called "chess" (with some chosen rule set). That is the strict and appropriate meaning of "solve".
Apr 14, 2022
0
#3004
Hi @Elroch !
Regarding 'proof' and its realities:
There's something that could be called 'objective proof' and there's lots of that around.
But then there's a flip side of proof.
Which isn't quite like the silliness of "if a tree falls in the forest but there's nobody around to hear it then it makes no sound" ...
not quite as 'silly' as that.
It goes like this: its a kind of analysis of 'proof' behaviour.
And some optional connotations of the word 'proof'.
I'll put it as a question:
Does 'proof' require cooperation from the person to whom something might or might not be proved to?
I would say ... Yes. Its not proof unless whoever finds it such.
Even the proof there is no greatest prime number -
a very very Neat proof ...
well whoever can simply refuse to follow the logic of it.
"No - that's Not Proof !" And then even assign his own 'defaults'.
We've seen that here.
Apr 14, 2022
0
#3005
It's probably worth bearing in mind the notion of a mechanised proof. This is one where the axioms are encoded and every logical step verified by computer in full detail.
Normal mathematical proofs have the character that they could feasibly be mechanised.
For example, this has been done for both of Goedel's main theorems.
Apr 14, 2022
0
#3006
Elroch wrote:
It's probably worth bearing in mind the notion of a mechanised proof. This is one where the axioms are encoded and every logical step verified by computer in full detail.
Normal mathematical proofs have the character that they could feasibly be mechanised.
For example, this has been done for both of Goedel's main theorems.
I looked at that linked site for a bit.
'Mechanized proof'.
Could a computer prove the 'no greatest prime' argument ?
I would guess yes. Using computerization of mathematical logic.
But only a guess. I would think the computer would need much 'help' from a human programmer - to so prove.
Makes me wonder - do computers solve differential equations ... and very tough integrals - where just substituting values for variables in formulas isn't going to work ... ?
Maybe differential equations have changed a lot nowadays ...
Apr 14, 2022
0
#3007
Not only "could", pretty sure that has been done. I think all of Euclid has been mechanised. Here is a paper about mechanical verification of book I.
Apr 14, 2022
0
#3008
Elroch wrote:
Not only "could", all of Euclid has been mechanised.
Even there - 'proof' to whoever might still 'require cooperation' by the provee.
Yes - I realize that the 'proof' still exists if whoever refuses to accept it.
But there's something about the word that connects with 'it takes two to tango'.
Pi would still be a constant without anybody around to know that it is.
Einstein apparently didn't need anybody to agree with him initially or at all - for his fundamentals to exist and be valid.
(ein ... a ... 'one')
But for 'proof' something about that word implies 'at least two persons participating and with some degree of cooperation'.
Apr 14, 2022
0
#3009
tygxc wrote:
#3034
"I think I can honestly say I doubt if I'd win it as Black even against Stockfish. I'd put money on losing it against a 32 man tablebase if there were such a thing. "
++ Yes, I guess that is true. However, we are not talking about practical play against Stockfish here with the inherent human errors, but rather about weakly solving chess. I.e. both entities commanding the white and the black pieces are presumed to play optimal moves.
You are talking about practical play with inherent human errors and inherent engine errors. Your assessment of the position is entirely based on that.
It's also based on the results of such play under a range of different rule sets which quite possibly (indeed probably) don't have any common weak solution and certainly don't have any common strong solution. Optimal moves under any set are not necessarily optimal under any other set.
It's possible that the position in question is a theoretical win under FIDE basic rules and ICCF rules, but a theoretical draw under FIDE competition rules rules.
What you're not talking about when you discuss that position is weakly solving chess.
Stockfish should win this against itself or against any present or future engine, or against the postulated 32-men table base.
I guess that SF (any of the versions I have) would win the position as Black against itself.
You have no grounds at all to say it would win against any future engine and certainly not against a postulated 32-men table base.
This is a similar but simpler position which we know is won for Black under either basic or competition rules. SF14 draws against the Syzygy tablebase.
So you're not only guessing from zero practical data; you're guessing contrary to what happens in similar but simpler situations where there are data.
An ICCF grandmaster should win this against the postulated 32-men table base.
You have no grounds for saying that. I'd guess they'd draw or lose.
In practice ICCF grandmasters resign when they lose a pawn without compensation.
The tablebases don't resign. Resigning is almost never an optimal move.
There is also no doubt at all that the postulated 32-men table base would list the entry 1 e4 e5 2 Ba6 as black checkmates in X moves, presumably with X < 50.
That you have no doubt at all that the position would be a win for Black doesn't mean "there is also no doubt at all" that it would.
Again you don't specify the game in question or the type of tablebase. Syzygy tablebases don't give a specific number of moves to checkmate and Nalimov tablebases don't necessarily work under competition rules.
Personally, I would doubt there is a forced mate in under 50 moves, but I would guess there is a mate, and within the 50 move rule.
If I could somehow know the answer, I wouldn't be too surprised if I've guessed wrong.
Apr 14, 2022
0
#3010
Regarding a chess engine defeating itself after being given material odds ...
Perhaps it would be better to have it play such against different engines.
Otherwise - it supports its own flaws.
In the research projects though - maybe that would slow down the 'solved' stuff too much.
playerafar wrote:
Martiggan, Mpaetz, Playerafar, Elroch, and now myself), you now want to extricate yourself and be left alone. Conveniently, this wish for getting along always follows only after you have already dropped your payload and have run out of bombs yourself. There's an adjective for describing those who sue for peace in this manner having already unloaded their salvos...
'adjective' yes.
But the constant and consistent projection from the individual is remarkable.
Every time he does something - its 'the other person doing it'.
Close to 100% of the time. He'll even project his projecting too.
But that's part of chronic projection though.
If he admits it - how can he continue?
It might even extend to his trying to deter use of the word.
One is not to say it ?
And 'is not to disagree with him nor criticize any post he makes'?
A kind of 'emperor has no clothes but you mustn't say it' situation.
Normally, it comes at a time when I'm starting to get annoyed with someone, due to their method of doing business. People with a lot in common tend to stick together and find refuge with one-another. So I generally suggest that enough is enough because, when you're dealing with people who lack moral strength, it's best not to become angry. Of course I like to get on with people but it's hardly going to happen here. Inadequate people conglomerate around each other, when each is somewhat insignificant on his own. There's no-one here whom I respect but there are one or two whom I like a little, because they're capable of exercising some restraint. But there's no-one who can put together a well-thought-out argument by themselves. That has been well and truly demonstrated. Facebook used to be better for that kind of thing but it's gone the same way. Nothing but triviality and, when something actually may be important, people who are completely over-bearing and one-sided in their viewpoints. Like on the Covid thread. The quality of discussion on these forums has dropped over the past year and it was never all that good, so it's time to call it a day and leave you all to it. I'll continue to pass the time of day socially and contribute to chess-related themes. This kind of thing, where everyone is a self-appointed expert and is determined to defend that dubious status by any means possible, is symptomatic of those who have reached a certain age and have nothing at all left, except bitterness and jealousy. I don't want to be part of what you, between you, are doing. So goodbye xxx.
Apr 14, 2022
0
#3013
Elroch wrote:
Not only "could", pretty sure that has been done. I think all of Euclid has been mechanised. Here is a paper about mechanical verification of book I.
Interesting paper. (Only twelve to go.)
Apr 14, 2022
0
#3014
I am not sure about my claim. I thought I recalled that being done, but I may be mistaken.
Here is some earlier work that addresses books I to IV:
https://www.andrew.cmu.edu/user/avigad/Papers/formal_system_for_euclids_elements.pdf
Apr 14, 2022
0
#3015
tygxc wrote:
Has chess been solved? No
Can chess be solved? Yes, it takes 5 years on cloud engines.
Will chess be solved? Maybe, it depends on somebody paying 5 million $ for the cloud engines and the human assistants during 5 years.
Have humans walked on Mars? No
Can humans walk on Mars? Yes
Will humans walk on Mars? Maybe, it depends on somebody paying billions of $ to build and launch a spacecraft.
That is post 2 of this forum - three months ago and over 3000 posts ago.
There's an attempt at an analogy between solving chess and a manned mission to Mars.
That doesn't prove anything of course.
And in that post @tygxc doesn't qualify with 'weakly' solving.
Its a kind of 'provocative dogbone'.
Has @tygxc conceded anything at all yet?
Has he conceded that 'strong' solving isn't feasible?
Not exactly. In his post 2 he didn't specify 'strong'.
So no. Nothing conceded. Not one point.
Regarding 10 to the 9th power computer - implying a billion positions solved per second - that doesn't hold up at all.
I didn't say he said that though.
A node isn't a 'position solved'.
If the computer could do a billion 'somethings' per second ...
and you put that up against 10 to the 44th positions.
Even if - the 'something' was solving a position -
it would still take 10 to the 35th seconds.
Which is more than 3000 trillion trillion years.
If it was 10 to the 37th positions ... then it would still take over
30 million trillion years.
But a node is not 'solving a position' ...
so it would take a lot longer than 30 million trillion years.
@tygxc is essentially still maintaining that 'it'
"takes 5 years on cloud engines.".
He has the same position 3 months later.
But what is 'it' ?
'It' may be nothing.
If solution is to be 'weak' that could mean chess already is solved as in
"chess is a draw unless somebody makes a mistake that can be exploited enough to force a win - except when that's not the case and its a win anyway"
In which case 5 years and cloud computers are both irrelevant.
So with a range of 'weak' possibilities that extends from 'already solved' all the way up to much more than 30 million trillion years -
then 5 years and cloud computers is random and arbitrary.
Another way to say this:
Could all of @tygxc's posts be 'skipped' except for his first posting here five years ago ? Because they're all essentially repetitions.
And post 2 at best is saying that chess can be solved but it could take over 30 million trillion years to do so.
And since the number of possible positions is finite -
then indeed it could be. And can be.
No bogus time needs to be added to support a possibility of 'solved'.
Its a finite number of positions - so it can be solved.
But that doesn't mean it will be.
Point: @tygxc 's post can be divided into two sections.
Concerning a possibility of solving - but that's already known because the number of positions is finite.
What's he's trying to do is argue that it can be solved by assigning a bogus time to it. Its like he's venturing a proof by assigning an unfounded time period.
Can the Andromeda galaxy be reached?
Yes. 'It takes two months using faster than light travel.'
If that had been his initial post in a forum about reaching Andromeda - how much response would that have deserved and gotten?
None. So what's actually different about his post 2?
Cloud computers exist whereas faster than light travel doesn't?
Doesn't hold up.
Space travel exists - but no computers exist that can solve a billion positions per second.
So it looks like his post 2 fails. It makes an assertion with no basis.
Still - it gets a lot of attention anyway 
Maybe that will continue.
tygxc wrote:
I am sure the phrase was 'provability is a higher degree of truth'. It figured in a feature article in Scientific American about unsolved mathematical problems including at that time Fermat's Last Theorem. It also discussed ramifications of Gödel's incompleteness theorems.
I cannot unfortunately provide volume, no., or page: I have no eidetic memory allowing total recall.
Then concede to take that statement as unreferenced. Anyway, if the statement was true, a proof could not be true at a higher degree than a knowledge already 100% true, and an axiom cannot be used to prove the axiom itself, like you do.
Apr 14, 2022
0
#3017
"and an axiom cannot be used to prove the axiom itself, like you do."
'trying' to do. For three months.
Failing - but controlling the forum anyway.
and he's got Nerve - pushing same.
Is another 1000 posts of that coming up ?
Apr 14, 2022
0
#3018
Elroch wrote:
Not only "could", pretty sure that has been done. I think all of Euclid has been mechanised. Here is a paper about mechanical verification of book I.
I put the link in my home page notes. So I could get around to reviewing that site sometime.
Regarding putting mathematical history on a timeline - creating a timeline in other words - its much easier to do that nowadays than in pre-internet times.
Regarding math and proofs being 'mechanized' it might be useful to know what isn't mechanized - or not yet. Or what can't be.
In a way - the discussion of solving chess is a bit like discussion of the future history of mathematics.
Chess apparently wasn't designed to have a relation to math though.
It was a game of royalties and generals and merchants and nobles is what I've read. And scribes and clergy.
Apr 14, 2022
0
#3019
Don’t rely on links for everything. It’s best to keep up the mathematics and not use links as examples.
🙁
#3046
"Provability is a higher degree of truth.
I asked if you can provide papers supporting this statement, because we use in general only two values of truth: true and false. Are you sure you did not mistake "provability" for "probability", reading something about fuzzy logic? "
++ Yes, I am sure the phrase was 'provability is a higher degree of truth'. It figured in a feature article in Scientific American about unsolved mathematical problems including at that time Fermat's Last Theorem. It also discussed ramifications of Gödel's incompleteness theorems.
I cannot unfortunately provide volume, no., or page: I have no eidetic memory allowing total recall.