{"id":"2e188338-610c-48c2-a184-df5fb239dcc4","arxiv_id":"2608.11496","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Discrete Ensemble Logic over the natural numbers is Sigma-1-1-complete for satisfiability, sits between star-free and monadic Presburger arithmetic, and has an NP-complete existential fragment.","lead":"This paper studies a temporal logic for medical and genomic records that can express exact offsets, bounded windows, and first-order quantification over distances. It shows the full logic is undecidable at the analytical second-order level, while a restricted existential fragment stays decidable and NP-complete.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Example 11's parity separation is asserted, not proved: the transfer from finite-word FO[<,+] lower bounds to infinite words wcd^omega is non-obvious and load-bearing.","rationale":"The reader's weakest_assumption isolates exactly the load-bearing gap: the transfer from finite-word FO[<,+] lower bounds to the infinite structures wcd^omega is asserted rather than proved. This matters because Theorem 12(ii)'s claim that omega-Reg is not contained in EL(N) depends entirely on Example 11; without it, the paper only establishes that EL(N) defines a non-omega-regular language, not incomparability. The gap is a correctness risk, not a disagreement with consensus: the statement is likely true and probably fixable, but as written the key separation is unsupported. A secondary weakness is the appendix's own admission (Section 12.1) that the oracle-relative completeness proof uses only the oracle rule and none of the HEL axioms, which makes the Hilbert-system contribution nearly vacuous. However, that issue does not affect the central classification results, so it does not change the verdict. The paper's core upper bound (Theorem 5), the two-counter-machine hardness (Theorem 8), and the non-omega-regular example (Example 10) all appear coherent. Therefore the appropriate verdict remains CONDITIONAL, unchanged from the reader's assessment.","tokens_in":14766,"tokens_out":22239,"duration_ms":249799,"concrete_test":"Prove or disprove the missing transfer lemma: for every FO(N,<,+,P) formula Phi, if Phi defines Lpar on words wcd^omega, then there is an FO[<,+] formula Psi on finite words such that Psi(w) holds iff Phi(wcd^omega) holds. A concrete check is to attempt an Ehrenfeucht-Fraisse game on the structures (N,<,+,A,B,C,D) with C={n} and D={m>n}, comparing words with even versus odd #a(w); if Duplicator wins for all finite ranks, non-definability holds and Example 11 is sound. Alternatively, exhibit one FO[<,+] formula over N that defines parity of the a-set before the delimiter, which would refute Example 11 and require a revised expressiveness claim.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Theorem 12(ii) claims incomparability with the omega-regular languages, and the non-containment direction rests entirely on Example 11. The argument is: if Lpar = {wcd^omega : #a(w) even} were EL-definable, Theorem 5 would give an FO(N,<,+,P) definition, and 'restricting' to words wcd^omega would yield an FO[<,+] definition of finite-word parity, contradicting the classical AC0 lower bound [9,1,10]. The restriction step is the weak point. The formula supplied by Theorem 5 lives on the infinite structure (N,<,+,P_a,P_b,P_c,P_d) with total addition and an infinite d-tail, whereas the AC0 lower bound concerns finite ordered words with partial addition. It is not shown that non-definability of parity on finite words transfers to this structure, nor that an FO[<,+] formula over N can be converted into one over finite prefixes in the presence of a unique delimiter c and an upward-closed tail. If FO[<,+] over N could define parity of the finite set of a-positions before c, the claimed separation would fail. The cited works [9,1,10] establish parity lower bounds for finite structures, not for the specific omega-word class used here, so the transfer is an unproved assertion in a load-bearing position.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"This paper develops the discrete point-based fragment EL(N) of Ensemble Logic, with syntax φ ::= p | φ^u | ¬φ | φ∧φ | φ∨φ | ♢_t φ | □_t φ | ∃x φ | ∀x φ, interpreted over ω-words over 2^P. The main results are: (1) a linear forward embedding into monadic Presburger arithmetic FO(N,<,+;P) (Theorem 5); (2) Σ1-1-completeness of satisfiability and Π1-1-completeness of validity via a reduction from the recurring problem for nondeterministic two-counter machines (Theorem 8, Corollary 9); (3) an expressiveness classification showing that EL(N) strictly contains the star-free ω-languages and is incomparable with the ω-regular languages (Theorem 12); (4) a sound Hilbert system with completeness relative to monadic Presburger validity (Theorem 14); (5) NP-completeness of the existential fragment, with coNP-complete unsatisfiability (Theorem 17, Corollary 18); and (6) PTIME data and PSPACE-complete combined complexity for finite active-domain model checking (Theorem 21).","tokens_in":15007,"tokens_out":27006,"duration_ms":264192,"significance":"The results, if fully established, would give a precise and nontrivial descriptive and computational profile for a logic with applications in biomedical knowledge representation. The two-counter-machine encoding is carefully designed with positive modal bounds, the embedding theorem is the right tool for the analytical upper bounds, and the NP-completeness proof for the existential fragment is convincing. The oracle-relative completeness theorem is honest about the strength of the oracle. The main weakness is the parity separation in Example 11, which is asserted rather than proved; this is load-bearing for the incomparability claim against the ω-regular languages. The model-checking complexity statement also needs to be made precise.","major_comments":[{"comment":"The separation from the ω-regular languages rests entirely on the assertion that if Lpar were definable in EL(N), then restricting the FO(N,<,+) definition to words of the form wcd^ω would yield an FO[<,+] definition of finite-word parity. This transfer is not proved and is non-obvious: the FO(N,<,+) formula may quantify over the infinite d-tail and use addition on positions beyond the delimiter, whereas the classical lower bounds cited in [9,1,10] are for finite ordered words with addition. A formal reduction from finite-word parity to definability of Lpar in FO(N,<,+) is needed, for example by relativizing quantifiers to the finite prefix and carefully handling addition overflow, or by an independent automata-theoretic argument. As written, Theorem 12(ii) is not supported.","section":"Section 6, Example 11 and Theorem 12(ii)"},{"comment":"The alpha-renaming convention stated in the proof of Theorem 5 does not prevent capture of variables occurring in displacement terms. In the recursion T_z((∀x ψ)_u) = ∀x T_{z+u}(ψ), a free variable of u with the same name as the bound variable x is captured. The convention only mentions avoiding capture of the distinguished variable z and the fresh modal variables. This is fixable by alpha-renaming all bound variables in the input formula to variables not occurring in any additive term of the formula before applying the translation, but the proof must state this explicitly.","section":"Section 4, Theorem 5"},{"comment":"The complexity statement 'combined complexity in |φ|+logN' is not well-defined for the model-checking problem as stated. The input includes the full trace σ of length N; if N is given in binary, the trace cannot be encoded in O(logN) bits. The theorem should either measure combined complexity in |φ|+N (or |φ|+|σ|), or specify an implicit representation of the trace. The upper-bound argument is plausible for fixed φ, but the PSPACE-completeness claim needs a precise input encoding.","section":"Section 9, Theorem 21"}],"minor_comments":[{"comment":"The notation 'T^{x_i}' in the QBF reduction is undefined; it should be the EL formula (T)_{x_i}, meaning that proposition T holds at the position x_i.","section":"Section 9, hardness proof"},{"comment":"The appendix honestly notes that the completeness derivation uses only the oracle rule and none of the structural axioms of HEL. This is acceptable for a relative completeness theorem, but the authors should state in the main text that the Hilbert system plays no essential role in the completeness proof and is primarily a proof-normalization device.","section":"Section 12.1"},{"comment":"The formula defining {a^m b^m c^m d^m | m≥1}·Σ^ω is correct, but the paper should spell out that the chosen n gives m=n+1 and that no constraint is imposed after the d-block, which is exactly the Σ^ω suffix.","section":"Section 6, Example 10"},{"comment":"The notation |n| for the size of a numeral is overloaded with the notation |φ| for formula size; this is harmless but could be clarified.","section":"Section 3, Definition 1"},{"comment":"The comparison with neighboring formalisms is informative, but the statement that 'complexity results based on LTL do not directly apply or need to be revisited' would benefit from a concrete example, since some LTL results are special cases of EL(N) results.","section":"Section 2.2"}],"recommendation":"major_revision","confidential_remarks":"The paper is technically substantial and the main undecidability and NP-completeness arguments are likely correct. The two issues that block acceptance in the current form are the unproved parity transfer in Example 11 and the ill-specified model-checking complexity parameter in Theorem 21. Both are fixable within the manuscript's scope, so I recommend major revision rather than rejection."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"You should know two things about this paper. First, the core complexity results are real and worth taking seriously: the embedding into monadic Presburger arithmetic is simple and correct, the two-counter reduction for Sigma-1-1-completeness is detailed, and the NP-completeness of the existential fragment plus the model-checking bounds fill out a useful picture. Second, the claimed incomparability with the omega-regular languages has a soft spot that is load-bearing. The paper asserts that an FO(N,<,+) definition of the parity language restricted to words wcd^omega would transfer to an FO[<,+] definition of parity on finite words. That transfer is not trivial. The classical lower bounds apply to finite structures with partial addition, not to the full structure (N,<,+) with unary predicates constrained by an infinite d-tail. It could well be true, but it needs a proof or at least a careful argument. As written, the separation from omega-regularity is an assertion supported by a citation, and Theorem 12(ii) leans on it completely.\n\nThe existential-fragment translation is the nicest part of the paper: it reduces satisfiability to existential Presburger arithmetic in a way that is polynomial and cleanly correct. The two-counter encoding also looks sound to me, and the use of positive bounds is handled consistently. I did not find a fatal flaw in the main classification.\n\nThe Hilbert system section is weaker than the abstract implies. The appendix admits that the completeness proof uses only the oracle rule and none of the HEL axioms. That makes the result a soundness theorem plus a direct delegation to a Pi-1-1-complete oracle, which is technically honest but not a substantive axiomatization. The paper should present it that way from the start rather than letting the abstract suggest a real proof system. This does not damage the complexity results, but it does mean the proof-theoretic contribution is much smaller than advertised.\n\nThe model-checking section is somewhat sketched, but the upper bound and QBF reduction are plausible. Minor, not worrying.\n\nOverall: this is a serious paper with new, useful results and one undisciplined expressiveness claim and one oversold proof system. It deserves a serious referee, but the authors should be asked to either prove the parity transfer or state the separation as conditional, and to reframe the Hilbert system section accurately.\n\nMy recommendation: send it to peer review, but only after those two points are addressed. The complexity core is solid enough to justify the effort.","headline":"Solid classification results for EL(N) with a clean embedding and a sharp lower bound, but the key separation from omega-regular languages rests on an unproved transfer argument, and the Hilbert system section overstates a largely oracle-trivial completeness theorem.","tokens_in":15529,"tokens_out":1690,"would_cite":true,"duration_ms":18995,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"Discrete Linear Ensemble Logic, whose metric distances are first-class quantified terms, has $\\Sigma^1_1$-complete satisfiability and $\\Pi^1_1$-complete validity, while its existential fragment is NP-complete.","keywords":["ensemble logic","temporal logic","monadic Presburger arithmetic","descriptive complexity","undecidability","omega-regular languages","model checking","electronic health records"],"falsifier":"Find an $\\mathrm{EL}(\\mathbb{N})$ formula, or after translation a monadic Presburger formula restricted to words of the shape $wcd^\\omega$, that is true exactly when the prefix $w$ contains an even number of $a$'s. Since the paper claims no such formula exists, finding one would collapse the claimed incomparability with the $\\omega$-regular languages.","tokens_in":14557,"feed_emoji":"📏","tokens_out":10537,"duration_ms":87712,"temperature":0.7,"pith_summary":"Discrete Linear Ensemble Logic, $\\mathrm{EL}(\\mathbb{N})$, adds three metric primitives to Boolean logic and first-order quantification over the natural numbers: exact displacement by an additive term, bounded existential windows, and bounded universal windows. The paper's central aim is to locate this logic precisely in the computability and expressiveness hierarchies. It proves that satisfiability of closed formulas is $\\Sigma^1_1$-complete and validity is $\\Pi^1_1$-complete, so the full logic is undecidable in a precise analytical sense. At the same time, the existential fragment $\\exists\\mathrm{EL}(\\mathbb{N})$ has NP-complete satisfiability, and finite active-domain model checking is polynomial-time for a fixed formula. A sympathetic reader should care because these results provide the baseline for any algorithmic use of the logic in biomedical knowledge representation, where displacement and bounded windows are the natural units of clinical and genomic constraints.","feed_headline":"Full logic is Sigma-1-1-complete; existential fragment is NP-complete","feed_subtitle":"A metric logic with reusable distances is analytically undecidable, yet its existential core is decidable.","key_machinery":"The load-bearing mechanism is the pair of window operators together with the arithmetic translation. Displacement $\\varphi^u$ moves evaluation to $i+\\eta(u)$; $\\Diamond_t\\varphi$ and $\\Box_t\\varphi$ quantify over the half-open window $[i,i+\\eta(t))$. The forward embedding $T_z$ compiles these into first-order formulas with addition: $T_z(\\Diamond_t\\varphi)=\\exists j\\,(z\\le j\\wedge j<z+t\\wedge T_j(\\varphi))$, and similarly for $\\Box_t$, with the current evaluation point tracked by the arithmetic term $z$. For hardness, the two-counter reduction encodes counter values as blocks of exact letters whose lengths are additive terms, and the existential-fragment translation eliminates all monadic predicates by replacing each diamond with a fresh witness variable and adding consistency constraints between coinciding literal positions. These mechanisms together carry the four main results: analytical completeness, expressive separation, NP-complete existential satisfiability, and the oracle-relative completeness of the Hilbert system.","core_discovery":"The paper's main discovery is that $\\mathrm{EL}(\\mathbb{N})$ occupies a very specific position between decidability and full second-order arithmetic. Through a linear-time translation $T_z$ into monadic first-order Presburger arithmetic $\\mathrm{FO}(\\mathbb{N},<,+;\\mathcal{P})$, every $\\mathrm{EL}(\\mathbb{N})$ formula becomes an arithmetical formula over unary predicates, yielding $\\Sigma^1_1$ upper bounds for satisfiability. A matching lower bound comes from encoding nondeterministic two-counter machines, with each counter value $x$ represented as a run of length $x+1$ of dedicated letters and a recurrence formula forcing a control state to occur infinitely often. Therefore satisfiability is $\\Sigma^1_1$-complete and validity is $\\Pi^1_1$-complete. Expressively, $\\mathrm{EL}(\\mathbb{N})$ defines the non-$\\omega$-regular counting language $\\{a^m b^m c^m d^m \\mid m\\ge 1\\}\\cdot\\Sigma^\\omega$, yet cannot define the $\\omega$-regular parity language $\\{wcd^\\omega \\mid |w|_a \\equiv 0 \\pmod 2\\}$, so the logic strictly contains the star-free $\\omega$-languages and is incomparable with the $\\omega$-regular languages. For the existential fragment, satisfiability is NP-complete via an explicit polynomial reduction to existential Presburger arithmetic.","pith_inferences":["Because the translation into monadic Presburger arithmetic is purely structural, the same proof strategy should transfer $\\mathrm{EL}$ to other additive monoids, such as dense time or product spaces, whenever the underlying arithmetic has a known first-order theory; the paper mentions these extensions but does not develop them.","The NP-complete existential fragment suggests a practical route for biomedical rule checking: compile bounded-window clauses of a trial protocol into existential Presburger constraints and hand them to a satisfiability solver, an implementation step the paper does not claim.","The conjecture that $\\mathrm{EL}(\\mathbb{N})$ is a proper subclass of $\\mathrm{FO}(\\mathbb{N},<,+;\\mathcal{P})$ remains open; a game-based separation of the two classes would sharpen the hierarchy and likely require new counting-invariant arguments beyond the parity example.","The parity separation relies on a finite-word lower bound; a direct proof that $\\mathrm{EL}(\\mathbb{N})$ cannot express parity on $\\omega$-words would make the argument self-contained and would also yield separation from other regular languages such as modulo-$k$ counting languages."],"forward_implications":["No recursive proof system can be complete for full $\\mathrm{EL}(\\mathbb{N})$: validity is $\\Pi^1_1$-complete, so any sound Hilbert system needs an oracle at least as strong as monadic Presburger validity.","The existential fragment $\\exists\\mathrm{EL}(\\mathbb{N})$ is the decidable core: satisfiability is NP-complete, so constraints written only with diamonds, displacement, and existential quantifiers can be compiled into existential Presburger formulas with polynomial-size witnesses.","A fixed $\\mathrm{EL}(\\mathbb{N})$ formula can be checked on a finite trace in polynomial time, and the combined active-domain model-checking problem is PSPACE-complete, giving a concrete complexity baseline for electronic-health-record monitoring.","Counting patterns such as equal-length blocks $a^m b^m c^m d^m$ are in the logic, so $\\mathrm{EL}(\\mathbb{N})$ can express constraints that no $\\omega$-regular language can, while parity constraints remain out of reach.","The Hilbert system $\\mathrm{HEL}$ is sound and complete relative to monadic Presburger validity, pinning the proof-theoretic strength of the logic exactly to that $\\Pi^1_1$-complete oracle."],"supporting_citations":[{"why":"Supplies the original Ensemble Logic syntax and semantics, including the earlier Post Correspondence Problem reduction for satisfiability.","marker":"[27]"},{"why":"Provides the $\\Sigma^1_1$-completeness of the recurring problem for nondeterministic two-counter machines used as the hardness source.","marker":"[13]"},{"why":"Establishes the correspondence between first-order logic on ordered finite words and star-free languages, anchoring the hierarchy inclusion.","marker":"[16]"},{"why":"Supplies the classical lower bound that parity is not definable in first-order logic with addition on finite ordered words, used for the separation from $\\omega$-regular languages.","marker":"[9, 1, 10]"},{"why":"Shows that monadic Presburger arithmetic with unary predicates is $\\Pi^1_1$-complete, fixing the oracle level for the relative completeness theorem.","marker":"[11]"},{"why":"Gives the NP upper bound for satisfiability of existential Presburger arithmetic with binary numerals, used for the existential-fragment complexity.","marker":"[23]"}],"fun_headline_variants":["Full logic Sigma-1-1-complete; existential fragment NP-complete","Undecidable full logic, but existential core NP-complete","Discrete ensemble logic: Sigma-1-1-hard, yet existential part in NP","Defines non-ω-regular language; existential fragment is NP-complete"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The non-definability of the parity language rests on the assumed, but not proved, transfer of a classical finite-word lower bound to padded infinite words of the form $wcd^\\omega$.","fun_headline_variants_meta":{"raw":{"variants":["Full logic Sigma-1-1-complete; existential fragment NP-complete","Undecidable full logic, but existential core NP-complete","Discrete ensemble logic: Sigma-1-1-hard, yet existential part in NP","Defines non-ω-regular language; existential fragment is NP-complete"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000933,"raw_usage":{"total_tokens":4080,"prompt_tokens":1121,"completion_tokens":2959,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":737,"completion_tokens_details":{"reasoning_tokens":2877}},"tokens_in":737,"tokens_out":2959,"duration_ms":20963,"temperature":1.0,"reasoning_tokens":2877,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-15T14:15:30.568395+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Find an $\\mathrm{EL}(\\mathbb{N})$ formula, or after translation a monadic Presburger formula restricted to words of the shape $wcd^\\omega$, that is true exactly when the prefix $w$ contains an even number of $a$'s. Since the paper claims no such formula exists, finding one would collapse the claimed incomparability with the $\\omega$-regular languages.","supporting_citations":[{"cited_title":"Temporal Ensemble Logic","cited_arxiv_id":"2408.14443","evidence_quote":"Supplies the original Ensemble Logic syntax and semantics, including the earlier Post Correspondence Problem reduction for satisfiability."},{"cited_title":"Kamp.Tense Logic and the Theory of Linear Order","cited_arxiv_id":null,"evidence_quote":"Establishes the correspondence between first-order logic on ordered finite words and star-free languages, anchoring the hierarchy inclusion."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Shows that monadic Presburger arithmetic with unary predicates is $\\Pi^1_1$-complete, fixing the oracle level for the relative completeness theorem."}],"review_version":1}