pith. sign in

arxiv: 2212.01053 · v3 · submitted 2022-12-02 · 🧮 math.LO

Deducibility in Sudoku

Dragan Ma\v{s}ulovi\'c This is my paper

Pith reviewed 2026-05-24 09:53 UTC · model grok-4.3

classification 🧮 math.LO
keywords Sudoku logicdeducibilityuniquenesssoundnesscompletenesssymmetryaxioms
0
0 comments X

The pith

A Sudoku puzzle has a unique solution if and only if that solution is deducible cell by cell in Sudoku logic, and the uniqueness statement itself is an axiom of the system.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces Sudoku logic as a formal system in which a solution counts as deducible once every cell can be shown to exclude all but one option. It proves the deductive rules are sound and complete relative to standard Sudoku constraints. This equivalence yields that uniqueness of solution coincides exactly with deducibility. The work further encodes symmetries via grid transformations and derives that the uniqueness formula is derivable as an axiom, allowing it to be used without separate justification.

Core claim

Sudoku logic is sound and complete, therefore a Sudoku puzzle has a unique solution if and only if it has a deducible solution. The formula that expresses the uniqueness of a solution is itself an axiom of Sudoku logic.

What carries the argument

Sudoku logic, whose rules allow the exclusion of all but one option per cell.

If this is right

  • Any uniquely solvable Sudoku admits a complete deductive solution without trial and error.
  • The uniqueness principle may be invoked directly as an axiom in any deduction.
  • Symmetry properties of Sudoku grids admit formal proofs within the logic.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same axiomatic treatment of uniqueness could be applied to other grid-based constraint problems.
  • Sudoku solvers could treat uniqueness statements as built-in rather than optional shortcuts.
  • The completeness result suggests that the logic might serve as a decision procedure for unique solvability.

Load-bearing premise

The exclusion rules of Sudoku logic correctly capture what counts as valid deduction.

What would settle it

A grid with a unique solution that cannot be reached by successive cell-by-cell exclusions, or a derivation showing the uniqueness formula is not an axiom.

read the original abstract

In this paper we provide a formalism, Sudoku logic, in which a solution is logically deducible if for every cell of the grid we can provably exclude all but a single option. We prove that the deductive system of Sudoku logic is sound and complete, and as a consequence of that we prove that a Sudoku puzzle has a unique solution if and only if it has a deducible solution. Using the classification of fundamental Sudoku transformations by Adler and Adler we then formalize the notion of symmetry in Sudoku and provide a formal proof of Gurth's Symmetrical Placement Theorem. In the concluding section we present a Sudoku formula that captures the idea of a Sudoku grid having a unique solution. It turns out that this formula is an axiom of Sudoku logic, making it possible for us to offer to the Sudoku community a resolution of the Uniqueness Controversy: if we accept Sudoku logic as presented in this paper, there is no controversy! Uniqueness is an axiom and, as any other axiom, may freely be used in any Sudoku deduction.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper introduces Sudoku logic, a formal deductive system in which a solution is deducible precisely when every cell can be shown to exclude all but one option. It proves soundness and completeness of this system relative to its semantics, derives the equivalence that a Sudoku puzzle has a unique solution if and only if it has a deducible solution, formalizes symmetries via the Adler-Adler classification of fundamental transformations, and supplies a formal proof of Gurth's Symmetrical Placement Theorem. In the concluding section it exhibits a formula expressing that a grid has a unique solution and asserts that this formula is an axiom of Sudoku logic, thereby claiming to resolve the uniqueness controversy by permitting its unrestricted use in deductions.

Significance. If the soundness, completeness, and symmetry results are correct, the work supplies a machine-checkable logical foundation for standard Sudoku deduction techniques and for symmetry arguments, together with an explicit axiomatization that makes uniqueness available as a primitive inference rule. These elements would be of interest to researchers in applied logic, automated reasoning, and combinatorial puzzle theory.

major comments (2)
  1. [Concluding section] Concluding section: the assertion that the uniqueness formula is an axiom requires an explicit statement of the underlying semantics. If the models include grids with zero or multiple solutions, then any derivation that invokes the axiom is unsound on those instances; the soundness theorem must therefore either restrict the class of models or treat the axiom as a hypothesis rather than an unconditional axiom. This point is load-bearing for the claim that the uniqueness controversy is resolved.
  2. [Soundness and completeness theorems] Soundness and completeness theorems (and the derived equivalence): the central claim that unique solution iff deducible solution follows immediately once soundness and completeness are established, but the paper must clarify whether the semantics are defined only over unique-solution grids. If the deductive rules are themselves formulated in terms of single-option exclusion, completeness risks being tautological with respect to the chosen models; an independent model-theoretic definition is needed to confirm the equivalence is non-circular.
minor comments (2)
  1. The reference to Adler and Adler for the symmetry classification should be given a full bibliographic entry and the relevant theorems or definitions from that work should be restated or cited with page numbers for self-contained reading.
  2. Notation for the deductive rules and for the uniqueness formula should be introduced with explicit definitions before first use; the current abstract-level presentation leaves the precise syntax of the uniqueness formula unclear.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful and constructive report. We respond point-by-point to the major comments and will revise the manuscript accordingly to improve the clarity of the semantics and the statements of the theorems.

read point-by-point responses

  1. Referee: [Concluding section] Concluding section: the assertion that the uniqueness formula is an axiom requires an explicit statement of the underlying semantics. If the models include grids with zero or multiple solutions, then any derivation that invokes the axiom is unsound on those instances; the soundness theorem must therefore either restrict the class of models or treat the axiom as a hypothesis rather than an unconditional axiom. This point is load-bearing for the claim that the uniqueness controversy is resolved.

    Authors: We agree that an explicit statement of the semantics is required. The models are all grids satisfying the standard Sudoku constraints. The uniqueness formula is an axiom of the deductive system, but soundness of derivations that use it holds relative to the subclass of models that possess a unique solution. In the revised manuscript we will add an explicit clause restricting the soundness theorem (when the uniqueness axiom is active) to unique-solution models, or equivalently present the formula as a hypothesis in that context. This preserves both soundness and the intended resolution of the uniqueness controversy within the standard Sudoku-solving setting. revision: yes

  2. Referee: [Soundness and completeness theorems] Soundness and completeness theorems (and the derived equivalence): the central claim that unique solution iff deducible solution follows immediately once soundness and completeness are established, but the paper must clarify whether the semantics are defined only over unique-solution grids. If the deductive rules are themselves formulated in terms of single-option exclusion, completeness risks being tautological with respect to the chosen models; an independent model-theoretic definition is needed to confirm the equivalence is non-circular.

    Authors: The semantics are defined independently of the deductive system: a model is any complete filling of the grid that satisfies the row, column and block constraints (each contains 1–9 exactly once). The deductive rules consist of the standard exclusion inferences together with the uniqueness axiom; they do not presuppose uniqueness of the overall solution. Soundness asserts that every deducible exclusion holds in all models; completeness asserts the converse. The equivalence “unique solution iff deducible solution” is then obtained by applying soundness and completeness to the full set of cells. Because the model class is defined model-theoretically without reference to the deduction rules, the argument is not circular. The revised manuscript will include an expanded, self-contained definition of the models and a brief outline of the completeness argument to make the independence explicit. revision: yes

Circularity Check

0 steps flagged

No significant circularity; core claims rest on independent soundness/completeness proofs

full rationale

The paper defines a deductive system via explicit rules for excluding all but one option per cell, then proves soundness and completeness relative to that system before deriving the unique-solution iff deducible-solution theorem as a direct consequence. The uniqueness formula is identified as an axiom only in the concluding section after these proofs; this does not reduce the iff statement to a definitional tautology or fitted input. The sole self-citation (Adler and Adler) supports symmetry classification and is not load-bearing for the logical results. The derivation is self-contained against external benchmarks and exhibits none of the enumerated circularity patterns.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The paper introduces Sudoku logic whose axioms include a uniqueness formula; full list of axioms and any free parameters cannot be extracted from the abstract alone.

axioms (1)
  • ad hoc to paper The uniqueness formula is an axiom of Sudoku logic
    Stated in the concluding section of the abstract

pith-pipeline@v0.9.0 · 5700 in / 1158 out tokens · 18068 ms · 2026-05-24T09:53:42.828819+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.