{"id":"19b2ffc5-a034-4b81-a37f-d646296c83df","arxiv_id":"1908.01635","paper_version":2,"verdict":"ACCEPT","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"NNIL formulas are characterized via color-preserving monotonic maps, admit a finite universal model for each number of variables, and the resulting subframe logics are closed under arbitrary substructures.","lead":"This mathematics paper studies NNIL formulas, a restricted family of intuitionistic logic formulas, and builds a small universal model that captures exactly when two such formulas are equivalent. The construction yields new proofs that certain intuitionistic logics are well behaved, including the finite countermodel property and canonicity.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Corollary 4.13 inherits its force from the unproved external Theorem 3.4; the universal-model claims themselves are internally coherent.","rationale":"The reader's weakest-assumption analysis correctly identifies Theorem 3.4 as the non-self-contained step. My independent check of the paper's new constructions found no internal error: the color-monotone refutation criterion in Theorem 3.3 works because the unraveling is finite and the constructed map preserves all required invariants; Proposition 4.4's anti-symmetry argument depends only on the invariant that a root color never reappears deeper in a T(n)-tree, which is true by induction; Lemma 4.8's reduction is sound; and Proposition 4.10(2)'s beta-plus formula handles the empty upset correctly because the conjunction is over all nodes outside U, so no empty-conjunction edge case arises. I therefore would not change the ACCEPT verdict. The external theorem is a normal citation, but because the paper's most sweeping claim about all subframe logics rests on it, the concern is worth a targeted check rather than silent acceptance. My agreement is partial: the reader and I downstream agree on the same dependency, but I do not treat it as a correctness defect of the paper's own contribution.","tokens_in":22191,"tokens_out":51994,"duration_ms":556441,"concrete_test":"Inspect [3, Cor. 3.4.16] and the surrounding construction in [3, §3.3], and verify: (a) every intermediate subframe logic is axiomatized by NNIL formulas of exactly the class B from Definition 3.1, or (b) if the axioms are only NNIL in some broader sense, that Corollary 4.11's B-representation applies to them. If (a) or (b) fails, Corollary 4.13 should be weakened to B-axiomatized logics, while the universal-model and NNIL=MR theorems remain intact.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The universal-model construction in §4 is internally coherent: I checked Proposition 4.4's fixed-point argument, Theorem 4.9's reduction, Proposition 4.10's beta-plus exactness, and the MR/NNIL transfer in Proposition 4.7, and I found no invalid step. The genuinely load-bearing dependency is Theorem 3.4, imported from [3, Cor. 3.4.16] without proof. It is the only bridge from the paper's self-contained B/NNIL/MR results to the headline statement that every intermediate subframe logic has frame classes closed under arbitrary substructures (Corollary 4.12(4) iff (2), and hence Corollary 4.13). Everything up to Corollary 4.12(1) iff (3) is self-contained, and Theorem 5.8 could be repaired using Corollary 3.8 plus Corollary 4.11. The risk, therefore, is not an internal inconsistency but a missing verification: if [3]'s theorem has a hidden hypothesis, or its NNIL axioms are not literally of the class B defined in Definition 3.1, then Corollary 4.13's first sentence is unsupported. This is a dependence on an external source rather than a flaw in the paper's own proofs, but it is the weakest point of the announced 'all subframe logics' generalization.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper studies NNIL-formulas of intuitionistic propositional logic and their model-theoretic behaviour. It first proves a refutation criterion (Theorem 3.3): a formula beta(N) associated with a finite rooted n-model N fails on an n-model M exactly when the unraveling N^t maps monotonically and color-preservingly into M. This is generalized to color-consistent maps into arbitrary Kripke or descriptive frames (Theorem 3.7), yielding preservation of the class B of NNIL-subframe formulas under arbitrary substructures, without the topo-subframe condition (Corollary 3.8). The authors then construct a finite exact n-universal model T(n) for NNIL- and MR-formulas (Proposition 4.10), prove that every finite n-tree is MR-equivalent to a unique node of T(n) (Theorem 4.9), and derive that NNIL-formulas are exactly the formulas reflected by color-preserving monotonic maps and that every MR-formula is equivalent to a finite conjunction of B-formulas (Corollary 4.11). They connect these results to subframe logics (Corollary 4.12) and canonicity (Corollary 4.13), and prove finite model property for logics axiomatized by NNIL- or MR-formulas (Theorem 5.8) using finite color-preserving submodels. The universal-model and B/NNIL/MR portions are self-contained; the statements about all subframe logics rely on Theorem 3.4, imported from Bezhanishvili's thesis.","tokens_in":22372,"tokens_out":20128,"duration_ms":212214,"significance":"If the results hold, the paper is a substantial contribution to the model theory of intuitionistic logic. The construction of T(n) as a finite exact n-universal model for NNIL- and MR-formulas is elegant and gives a new structural proof that NNIL equals both MR and the class of finite conjunctions of B-formulas. The refutation criterion via color-consistent monotonic maps is clean, and the finite-model-property proof via color-preserving submodels is a genuinely different route from earlier canonical-formula arguments. The paper is for the most part carefully written and contains detailed proofs of the universal-model facts, including exact definability of every upset by beta_+(U) and the isomorphism with the n-canonical model. The main caveat is that the extension from B-axiomatized logics to 'all subframe logics' in Corollaries 4.12 and 4.13 is not self-contained: it passes through Theorem 3.4, cited from [3] without proof. This does not appear to be a flaw in the paper's own derivations, but it is a dependency that should be made explicit and verified against the exact form of Definition 3.1.","major_comments":[],"minor_comments":[{"comment":"Please add a sentence stating explicitly that the equivalence with subframe logics and the canonicity corollary are conditional on Bezhanishvili's Theorem 3.4, cited from [3], and verify that the NNIL formulas axiomatizing subframe logics in [3] are indeed of the form given in Definition 3.1. The self-contained part of the paper establishes the B/NNIL/MR equivalences and the substructure preservation for B-formulas; the step to 'all subframe logics' is the one place where the paper relies on an external result.","section":"§3, Theorem 3.4; §4, Corollaries 4.12–4.13"},{"comment":"The proof of Lemma 5.3 does not explicitly treat the root case in the verification that N is color-preserving. If w is the root and a successor u has the same color as the root, the required witness is v = w; if the color is strictly larger, take the first node on the path where the color jumps. Please spell this out, because as written the phrase 'since col(w0) < col(w)' only applies after the root case is separated.","section":"§5, Lemma 5.3"},{"comment":"The proof of Proposition 4.4(1) uses the fact that no element of X contains a node of the color of the fresh root w. This follows from persistence and from the construction because every node in a tree Tw_i has color at least the color of its root, which is strictly larger than col(w); please state this invariant explicitly, since it is otherwise easy to miss.","section":"§4, Proposition 4.4(1)"},{"comment":"In the proof of Proposition 4.10(2), the last displayed sentence says 'Tu does not satisfy beta_+(w)' but the formula is beta_+(U); please correct the variable.","section":"§4, Proposition 4.10(2)"},{"comment":"There are several typos: 'formulas that does not allow' should be 'formulas that do not allow'; 'subsitutions' should be 'substitutions'; and the abstract contains an awkward 'i.e.i' fragment. These should be cleaned up.","section":"Abstract and §1"},{"comment":"Definition 4.1(ii) contains a double period after 'V(phi) = U'; also, since T(n) is finite, it may be worth noting explicitly that the model satisfies the stronger 'exact' condition for all upsets, not only point-generated ones, as is done later in Proposition 4.10.","section":"§4, Definition 4.1"}],"recommendation":"minor_revision","confidential_remarks":"I support publication after minor revision. The only substantive caveat is the reliance on [3, Cor. 3.4.16] for the 'all subframe logics' and canonicity statements; since this is a published theorem and the paper's own universal-model arguments are coherent, I do not regard it as a blocker. If the editors prefer fully self-contained claims, the authors could add a short proof sketch of Theorem 3.4 or restrict the unqualified wording to the B-axiomatized case."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"You should know two things about this paper. First, the construction of T(n), the exact n-universal model for NNIL- and MR-formulas, is real and self-contained. I checked the main inductions—Proposition 4.4's fixed-point argument, Theorem 4.9's back-and-forth map, Proposition 4.10's beta-plus exactness—and they hold together. Second, the advertised closure of all intermediate subframe logics under arbitrary substructures (Corollary 4.13) is not self-contained; it rests on Bezhanishvili's Theorem 3.4, imported without proof from his thesis. That is the load-bearing dependency, and it is the only place I worried about a hidden hypothesis.\n\nWhat is actually new: the T(n) construction itself, its exactness, and the consequence that every MR-formula is a finite conjunction of B-subframe formulas (Corollary 4.11). The paper also uses a neat filtration-like method—color-preserving submodels—to give a new proof of FMP for NNIL-axiomatized logics. It openly says FMP and canonicity were already known; the FMP proof in [18] is disclosed. That is honest scholarship.\n\nThe soft spots are minor. Lemma 5.3's existence argument skips the case where a successor of the root has the same color as the root; the fix is simple (take the root itself) but the proof should say so. Proposition 4.4 relies on an implicit invariant that colors strictly increase away from every tree root; it is true and easy to state, but currently backgrounded. The more substantive caveat is the external Theorem 3.4. If its statement is exactly what the paper needs—every intermediate subframe logic is NNIL-axiomatized with NNIL-subframe formulas in the class B—then Corollary 4.12 and 4.13 go through. I did not find a mismatch, but the paper should make the precise usage explicit. Reassuringly, the FMP result in Theorem 5.8 does not need that external theorem: by Corollary 4.11, an NNIL-axiomatized logic is also B-axiomatized, and then Corollary 3.8 alone gives the needed substructure closure.\n\nWho should read this: people working on intuitionistic logic, universal models, or subframe logics. It is a competent, useful contribution, not a radical one. It deserves a serious referee who knows the [3] theorem.\n\nRecommendation: send it to peer review. The revisions are small: fix the root case in Lemma 5.3, make the Prop 4.4 invariant explicit, and flag the external dependency clearly.","headline":"The n-universal model for NNIL-formulas is a genuinely new tool; the paper is sound, with one manageable external dependency in the headline subframe-logic generalization.","tokens_in":22989,"tokens_out":5967,"would_cite":true,"duration_ms":51872,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03B20","03B55","03F55"],"pacs":[],"model":"deepseek-v4-flash","headline":"NNIL formulas are exactly the intuitionistic formulas preserved by arbitrary substructures, with a finite universal tree model as the witness.","keywords":["NNIL-formulas","intuitionistic logic","universal models","subframe logics","finite model property","monotonic maps","MR-formulas","relational semantics"],"falsifier":"Try to find any intermediate subframe logic whose frame class is not closed under arbitrary substructures; the paper's Corollary 4.13 predicts none exists. More locally, the refutation criterion would be overturned by a finite rooted $n$-model $N$ and a descriptive frame $F$ that refutes $\\beta(N)$ while admitting no color-consistent monotonic map from the unraveled tree $N^t$ into $F$.","tokens_in":21919,"feed_emoji":"🌳","tokens_out":6329,"duration_ms":63234,"temperature":0.7,"pith_summary":"The paper establishes a sharp semantic boundary for NNIL, the intuitionistic propositional formulas that forbid nesting of implication on the left. It proves that being an NNIL formula is the same as being reflected by color-preserving monotonic maps between relational models, and the same as being preserved under arbitrary substructures, not only the topo-subframes usually required. The argument runs through a finite rooted n-universal model built out of finite trees, in which every upset is definable by a NNIL-subframe formula. From this the paper derives that every logic axiomatized by NNIL formulas, equivalently every intermediate subframe logic, has the finite model property and is canonical.","feed_headline":"NNIL formulas are exactly the ones all substructures keep true","feed_subtitle":"A finite universal tree model characterizes the class and yields a fresh finite-model-property proof.","key_machinery":"The engine is the color-preserving monotonic map: an order-preserving function between relational models that leaves the truth values of the $n$ proposition letters unchanged. Against it, the paper sets NNIL-subframe formulas $\\beta(N)$, inductively built from a finite rooted model $N$, with the refutation criterion that a frame $F$ falsifies $\\beta(N)$ exactly when a color-consistent monotonic map from the unraveled tree $N^t$ into $F$ exists. The universal model $T(n)$ is then assembled from finite trees as nodes, ordered by existence of these maps; its key property is that every finite $n$-tree maps back and forth into a unique representative in $T(n)$, which makes the model exact for NNIL and MR.","core_discovery":"On the paper's own terms, the central discovery is that a finite tree-like model $T(n)$ is an exact $n$-universal model simultaneously for NNIL-formulas and for MR-formulas, the formulas reflected by color-preserving monotonic maps. For every finite $n$-tree there is exactly one node $T_w$ of $T(n)$ equivalent to it under two-way color-preserving monotonic maps, and every upset of $T(n)$ is definable by a conjunction $\\beta^+(U)$ of NNIL-subframe formulas. The paper then derives that NNIL and MR coincide: every MR-formula is equivalent to a finite conjunction of NNIL-subframe formulas, and NNIL-formulas are exactly the formulas reflected by color-preserving monotonic maps. It also derives that logics axiomatized by NNIL formulas are precisely the intermediate subframe logics, that their frame classes are closed under arbitrary substructures, and that these logics are canonical and have the finite model property.","pith_inferences":["The finite reduction theorem is constructive in the number of colors; a natural next step, not taken in the paper, is to extract explicit bounds on countermodel size and see whether NNIL fragments have tractable finite-model-finding.","The same 'closed under arbitrary substructures' test could be applied to modal subframe logics: the paper leaves open whether a syntactic characterization exists, and the color-consistent map criterion is a candidate discriminating principle.","Because every upset of $T(n)$ is definable by a $\\beta^+$ formula, the $\\mathrm{NNIL}_n$ Lindenbaum-Tarski algebra has a transparent representation; this may make interpolation or correspondence questions for the fragment easier to settle."],"forward_implications":["Every MR-formula is equivalent to a finite conjunction of NNIL-subframe formulas, so the two classes coincide up to equivalence; in particular, formulas reflected by color-preserving monotonic maps are exactly NNIL formulas.","The frame class of any intermediate subframe logic is closed under arbitrary substructures, not only topo-subframes, and every such logic is canonical.","Every logic axiomatized by NNIL or MR formulas has the finite model property, obtained here by a direct finite color-preserving submodel reduction.","The $n$-universal model $T(n)$ is finite and rooted, isomorphic to the $n$-canonical model, and exact: every upset is NNIL-definable."],"supporting_citations":[{"why":"Supplies the theorem, imported without proof, that every intermediate subframe logic is axiomatized by NNIL-formulas; this carries the extension from beta-axioms to all subframe logics.","marker":"[3]"},{"why":"Supplies Lemma 2.2, the reflection of NNIL-formulas by color-preserving monotonic maps, which underlies the refutation criterion.","marker":"[6]"},{"why":"Earlier result that NNIL-formulas are exactly the submodel-preserved formulas; the paper gives a new proof of this equivalence via $T(n)$.","marker":"[28]"},{"why":"Constructed the 2-universal model for NNIL and initiated the study that the present $T(n)$ completes.","marker":"[29]"}],"fun_headline_variants":["NNIL and MR formulas coincide via finite universal trees","Universal trees yield NNIL = MR and new finite model proof","One finite tree model unifies NNIL and MR formulas","Exact universal tree model for NNIL and MR formulas","NNIL = MR: finite universal tree models"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The paper's broadest conclusion, that every intermediate subframe logic has a frame class closed under arbitrary substructures, rests on an imported theorem that every intermediate subframe logic is axiomatized by NNIL-subframe formulas; the paper does not prove that theorem.","fun_headline_variants_meta":{"raw":{"variants":["NNIL and MR formulas coincide via finite universal trees","Universal trees yield NNIL = MR and new finite model proof","One finite tree model unifies NNIL and MR formulas","Exact universal tree model for NNIL and MR formulas","NNIL = MR: finite universal tree models"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001042,"raw_usage":{"total_tokens":4387,"prompt_tokens":956,"completion_tokens":3431,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":572,"completion_tokens_details":{"reasoning_tokens":3362}},"tokens_in":572,"tokens_out":3431,"duration_ms":21943,"temperature":1.0,"reasoning_tokens":3362,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T15:09:04.886186+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Try to find any intermediate subframe logic whose frame class is not closed under arbitrary substructures; the paper's Corollary 4.13 predicts none exists. More locally, the refutation criterion would be overturned by a finite rooted $n$-model $N$ and a descriptive frame $F$ that refutes $\\beta(N)$ while admitting no color-consistent monotonic map from the unraveled tree $N^t$ into $F$.","supporting_citations":[{"cited_title":"Bezhanishvili","cited_arxiv_id":null,"evidence_quote":"Supplies the theorem, imported without proof, that every intermediate subframe logic is axiomatized by NNIL-formulas; this carries the extension from beta-axioms to all subframe logics."},{"cited_title":"Bezhanishvili and D","cited_arxiv_id":null,"evidence_quote":"Supplies Lemma 2.2, the reflection of NNIL-formulas by color-preserving monotonic maps, which underlies the refutation criterion."},{"cited_title":"Visser, D","cited_arxiv_id":null,"evidence_quote":"Earlier result that NNIL-formulas are exactly the submodel-preserved formulas; the paper gives a new proof of this equivalence via $T(n)$."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Constructed the 2-universal model for NNIL and initiated the study that the present $T(n)$ completes."}],"review_version":1}