denis_berthier wrote:re'born wrote:denis_berthier wrote:re'born wrote:your notion of constructiveness is the extra assumption.

Constructive logic is weaker than classical logic. How could it be an extra assumption?

Classical logic is the default assumption, but not necessarily always the best one. See my last answer to RedEd.

Your extra assumption is that one needs to find a solution path using resolution rules (as you define them). That is a matter of taste on

your part. The rules of sudoku do not mandate that a solution be found using 'pure logic' (and you really need to stop using that phrase as it is needlessly inflammatory and offensive to people who solve puzzles using ideas that fail to meet your standards). To require such is fine, but it changes the game.

I've always been clear and I've always said that my framework is an interpretation and a formalisation of the undefined expression "pure logic solution".

Yes, but you've never accepted that using that phrase, at best, seems like a PR move, and, at worst, is insulting to a large number of players. If I used an expression similar to a racial slur for a resolution rule, it wouldn't matter how many times I explained the exact meaning or protested that it was merely 'a formalization of an undefined expression', I would still get my <expletive deleted> kicked.

Denis wrote:Requiring a "pure logic solution" changes the game, whatever is meant by this.

I completely agree.

Denis wrote:I think few players would accept backtracking. So doing, they change the game.

If you are talking about players on the forum, yes. If you are talking about the millions around the world who play, I suspect (with good reason) a whole lot of backtracking goes on.

Denis wrote:What I'm doing is developing a consistent conceptual framework. You may accept it or not, but you can't deny it allows to define powerful resolution rules.

The problem isn't me (or anyone else) accepting your 'consistent conceptual framework' and I won't deny your 'powerful resolution rules'. As a player, I find the framework almost useless, but as a mathematician, I very much appreciate the point of view. The problem is

Denis wrote:RedEd's proof has an implicit assumption: we must accept any kind of solution, including non constructive ones, e.g. those obtained by recursive backtracking with guessing.

You are confusing the issues by suggesting that RedEd's proof is hiding an assumption, when the reality is that it is your conceptual framework that requires a different standard of proof for a deduction. The default is always anything goes.

Denis wrote:re'born wrote:denis_berthier wrote:Now your turn, tell me: don't you find it intuitively shocking that the entries of a puzzle allow you to prove that 3 cells in the UR1.1 pattern have well defined values and you're then asked to suppose that there might be another solution with other values for these 3 cells?

I'm sorry Denis, I don't understand your question. Who is asking me to suppose there might be another solution?

RedEd's proof

In that case, no I'm not intuitively (or otherwise) shocked; I've seen a proof by contradiction before.