{"id":"363c603b-d589-4174-8dbf-6cfffbd3142c","arxiv_id":"1908.00924","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Determining whether the logic of a finite reduced matrix is algebraizable, weakly algebraizable, equivalential, protoalgebraic, or order algebraizable is EXPTIME-complete; for truth-equational logic it is EXPTIME-hard.","lead":"This paper shows that deciding which level of the Leibniz hierarchy a finite logical matrix occupies is EXPTIME-complete for the main classes, and EXPTIME-hard for truth-equational logic. It answers an open question in abstract algebraic logic by reducing a known EXPTIME-complete clone problem to these classification problems.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Lemma 5.4's only-if direction asserts every closed term of A♭ evaluates to 1; this is false (for instance □_a(1)=0), and the proof's next step depends on it.","rationale":"The reader's weakest assumption targeted the appendix behind Lemma 5.2(iv)⇒(v). I examined those tree-property lemmas: although they are intricate and some steps are compressed, I did not find a definite false statement there, and the missing invariance used in Lemma 6.7 can be supplied by a short induction. The concrete mathematical error I found is in Lemma 5.4, where the proof asserts that every closed term of A♭ evaluates to 1; the term □_a(1) is a counterexample. This is a genuine gap in the written proof of the truth-equational hardness result, but it appears repairable by a short argument, so it does not by itself overturn the theorem. The verdict remains CONDITIONAL: the paper should be accepted only after the proof of Lemma 5.4 is corrected and the reader's requested clarifications to Corollary 5.7 are addressed.","tokens_in":20553,"tokens_out":42729,"duration_ms":450685,"concrete_test":"Formalize the only-if direction of Lemma 5.4 and check whether the repair succeeds: prove that any closed term of A♭ evaluates to 0 if it contains some □_a and to 1 otherwise, and then prove that a separating equation ε≈δ∈τ with ε(0)≠δ(0) cannot have a closed ε evaluating to 0, because δ would also have to be closed and equal to ε on G, forcing ε(0)=δ(0). If this argument goes through, Lemma 5.4 is sound after inserting it before the sentence 'In particular... t(1,...,1)≈1'. As a sanity check, compute the closed term □_a(1) in A♭ and confirm it evaluates to 0, which directly refutes the paper's unqualified claim.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Lemma 5.4, which supplies the EXPTIME-hardness reduction for truth-equational logic in Theorem 5.5, contains a false assertion in its only-if direction. After choosing an equation ε≈δ in τ with ε(0)≠δ(0), the proof says ε is a closed term 'of the form t(1,...,1)' and 'in particular A♭⊨ t(1,...,1)≈1'. This is not true: A♭ has unary operations □_a with □_a(1)=0, so the closed term □_a(1) evaluates to 0, not 1. The immediately following step, 'Together with the definition of τ, this implies that the equation δ(x)≈1 belongs to τ', uses ε=1; if ε evaluated to 0, this step would only yield δ≈0, and the subsequent descent to a formula x+ψ(x)≈1 could not get started. The statement can probably be repaired: a closed ε containing □_a evaluates to 0, and then ε≈δ∈τ with ε(0)≠δ(0) would force δ to be closed and equal to ε on G, contradicting ε(0)≠δ(0). Hence any separating ε must evaluate to 1. But that argument is not present in the paper. Since Lemma 5.4 is the only reduction proving truth-equational hardness, this unproved step is load-bearing.","agreement_with_reader":"partial"},"referee_report":null,"author_rebuttal":null,"desk_editor":null,"rs_alignment":null,"lean_confirmation":null,"pith_extraction":null,"created_at":"2026-08-14T15:49:41.756714+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":null,"supporting_citations":[],"review_version":1}