{"id":"5e924d9d-e785-4a64-bb0d-3d8a5c97d84e","arxiv_id":"2601.04080","paper_version":4,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A Maehara-style sequent construction builds Craig interpolants for the logic of here and there by passing through an intermediate logic with the nh operator and then translating to ordinary HT.","lead":"This paper builds Craig interpolants—small bridge formulas—for the three-valued logic of here and there by carrying a symbolic label through a sequent proof, using an auxiliary operator 'nh' that is later removed. It is a proof-theoretic contribution to interpolation for a logic used in answer set programming, not a new theorem about the logic itself.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Axiom Ax-nh-1-LR violates interpolation condition (I1), making the interpolating sequent system unsound as stated.","rationale":"I focused on the correctness of the interpolating sequent system itself. The reader identified completeness of the base system and the omitted rules in Lemma 3 as the weakest assumptions. Those are legitimate gaps, but I found a more direct and decisive flaw: axiom Ax-nh-1-LR, which is presented as part of the system, violates the very conditions (I1)–(I3) that Lemma 3 must establish. With A = p and empty context, (I1) requires |= nh(p) ∨ p, which fails at p = NF. This is not a missing proof sketch; it is a false statement about a displayed rule. Consequently, a proof using Ax-nh-1-LR can produce a preliminary interpolant C′ that does not satisfy A |= C′, invalidating the construction in Theorem 1 and hence Theorem 5. The flaw is concrete and easily checked, so the paper cannot be accepted as a proof of the central claim without at least removing or repairing this axiom and showing the construction still goes through. I also noticed a likely typo in Theorem 4's proof (replacing nh(E_i) with ¬¬E_i rather than ¬E_i), but the invalid axiom alone is sufficient to reject the paper as written.","tokens_in":9734,"tokens_out":24622,"duration_ms":207911,"concrete_test":"Instantiate Ax-nh-1-LR with A = p, Γ = ∅, ∆ = ∅. The split-sequent is ∅ ⇒ p_L, nh(p)_R with H = nh(p). Condition (I1) requires |= nh(p) ∨ p; evaluate at p = NF: nh(p) = NF and p = NF, so nh(p) ∨ p = NF, not T. Hence the axiom fails (I1). Alternatively, run the Maehara construction on a proof that uses this axiom on the branch p_L ⇒ r_L, ¬p_L, nh(r)_R, p_R; the interpolant H = nh(r) fails I1 at p = T, r = NF.","verdict_should_be":"REJECT","load_bearing_attack":"The central construction depends on Lemma 3, which asserts that every split-sequent in any proof satisfies conditions (I1)–(I3). But the presented axiom Ax-nh-1-LR does not satisfy (I1). The axiom is: Γ H ⇒ ∆, A_L, nh(A)_R, with H = nh(A). For this axiom, W∆L contains A, so (I1) requires VΓL |= nh(A) ∨ A ∨ W∆L′. Taking ΓL = ∅ and ∆L′ = ∅, this reduces to |= nh(A) ∨ A, which is not valid in HT: at A = NF, nh(A) = NF and A = NF, so nh(A) ∨ A = NF ≠ T. Thus an instance of the axiom with empty context violates (I1). The paper's claim that verification is 'easy to verify' is incorrect. Since the axiom is explicitly included in the system of Section 5.3, a proof using it can yield an interpolant C′ that fails the defining condition A |= C′. This is a concrete soundness failure in the interpolating system, not merely an omitted detail, and it undermines Theorem 1 and therefore Theorem 5 as proven.","agreement_with_reader":"disagree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes a Maehara-style, sequent-based construction of Craig interpolants for propositional HT (Gödel's G_3). It introduces an auxiliary three-valued operator nh, defines an interpolating version of a variation of Mints' sequent system for HT, and claims (Theorem 5) that from a proof of A |= B in this system one can effectively construct an HT-formula C with A |= C, C |= B, and voc(C) confined to the common atoms of A and B. The proof is in two stages: Theorem 1 constructs a preliminary nh-NNF interpolant C' by means of split-sequents; Theorem 4 converts C' to an HT interpolant. The paper is explicitly a research note and relies on known facts about HT, including Maksimova's interpolation theorem and Mints' sequent system.","tokens_in":9970,"tokens_out":16312,"duration_ms":148217,"significance":"If the construction were correct, it would provide a direct, sequent-based constructive interpolation proof for propositional HT, complementing Maksimova's existence results and the classical-encoding method of [6]. The nh-operator idea and the two-stage postprocessing are interesting, and the paper is clearly written. However, the proof as written contains a concrete unsoundness in an axiom, several load-bearing omissions in the rule set, and an internally inconsistent step in the conversion of Theorem 4. Credit is due for stating the two-stage plan explicitly and for not assuming the target interpolation property; but the central theorem is not established by the presented arguments.","major_comments":[{"comment":"The split-sequent axiom Ax-nh-1-LR, displayed as Γ H=⇒∆, A_L, nh(A)_R with H=nh(A), does not satisfy condition (I1) of §4. Taking Γ_L=∅ and Δ_L={A}, condition (I1) requires |= nh(A)∨A. In the 3-valued truth table, at A=NF both nh(A) and A are NF, so nh(A)∨A is NF, not T. Thus the instance with empty Γ_L and Δ_L={A} violates (I1). The verification paragraph in §5.3 ('easy to verify') is therefore incorrect: it writes the required condition as VΓ_L |= nh(A)∨WΔ_L∨A, but WΔ_L already contains A. The same problem affects the unsplit Ax-nh-1 in §3: the claimed soundness implication B→(C∨A∨nh(A)) is not valid in the 3-valued semantics; take B=⊤, C=⊥, A=NF. Since Ax-nh-1-LR is the only rule that introduces nh(A) into the interpolant, Lemma 3(ii) and Theorem 1 are not established as stated.","section":"§5.3, Ax-nh-1-LR (and §3, Ax-nh-1)"},{"comment":"Lemma 3 is stated for all split-sequents in any proof in the interpolating system of §5.3, but that system is not fully specified. The text explicitly omits axioms/rules for the truth-value constants, the eight ∧/∨ rules, the four ¬¬ rules, the twelve negation-inward rules, and the three nh-inward rules. Since Lemma 3 claims properties (i)–(vi) for every proof, each omitted rule must be specified and checked against (I1)–(I3). As written, the system is not well defined, and Theorem 1 cannot be verified even if the faulty axiom were corrected.","section":"§5.3, 'Further Axioms and Rules that are not Presented'"},{"comment":"The conversion step contains an internal mismatch. The proof defines D' as D with every nh(E_i) replaced by ¬E_i, but then modifies the proof P by replacing nh(E_i) with ¬¬E_i. This yields a proof of ¬¬A |= ¬¬(¬¬E_1∨...∨¬¬E_m∨F), not a proof of ¬¬A |= ¬¬D' as claimed. Unless '¬¬E_i' is a typo for '¬E_i', the step is invalid. Since Theorem 4 is the bridge from the preliminary nh-interpolant to the final HT interpolant, this is a load-bearing gap in the proof of Theorem 5.","section":"§6, Theorem 4 proof"},{"comment":"The completeness of the extended system for HTnh-formulas is only sketched: 'Completeness of systems for HTnh-formulas can be shown in the same way as outlined by Mints.' The countermodel construction for leaf sequents is given, but the rule set is incomplete (see above) and the argument does not cover the new implication rule ⇒→* or the nh-inward rules. Since Theorem 1 presupposes that a proof of A |= B exists in the system, this completeness gap is load-bearing. A rigorous completeness proof for the full rule set is needed.","section":"§3, Completeness"}],"minor_comments":[{"comment":"The title and abstract claim 'Craig-Lyndon interpolation', but the paper proves only vocabulary-restricted Craig interpolation; §7 explicitly says that strengthening to Craig-Lyndon interpolation is future work. The title/abstract should be adjusted to avoid overclaiming.","section":"Title and Abstract; §7"},{"comment":"The assertion that for A_R=⇒A_L 'there actually is no formula H' that satisfies (I1)–(I3) is stated informally. Since this is used to justify a restriction of the axiom system, a proof of the non-existence would strengthen the paper.","section":"§5.3, Ax-1-RL"},{"comment":"In the displayed interpolating versions of ⇒∧, the rules are named ⇒∧L and ⇒∧R, but in both the principal formula is placed in the succedent. The naming convention should be clarified for readers.","section":"§4, Example rules"},{"comment":"The condition that nh(A) must occur with positive polarity is not formalized as an inductive definition, which makes the exact class of nh-formulas slightly ambiguous.","section":"§2, grammar"}],"recommendation":"major_revision","confidential_remarks":"The stress-test concern about Ax-nh-1-LR is correct and is the primary technical obstacle. The paper is a research note; the two-stage interpolant idea is intriguing, and the existence of HT interpolation is already known, so the claimed contribution is the constructive method rather than the theorem itself. I recommend inviting a major revision rather than outright rejection, provided the author can repair the axiom, supply the missing rules, and fix the Theorem 4 substitution step. The known interpolation property means this is not a case of proving a false theorem, but the presented proof is not yet sound."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The paper's core idea is worth knowing: replacing the classical encoding with a direct Mints-style sequent system plus an auxiliary nh operator, then converting the nh-interpolant back to a proper HT formula. That two-stage structure is a real variation on the existing classical-encoding method, and the second-stage conversion (Theorem 4) is a neat trick that could be reusable even if the rest collapses. The author is also honest about the many omitted rules and the sketchiness of the completeness proof.\n\nBut the main construction has a load-bearing flaw. The stress-test note is correct: axiom Ax-nh-1-LR, with relative interpolant H = nh(A), does not satisfy condition (I1). For an instance with empty L-context and only A_L in the L-succedent, (I1) reduces to |= nh(A) ∨ A, which fails at A = NF. The paper's claim that this is 'easy to verify' is simply false. Since this axiom is explicitly part of the interpolating system, Lemma 3 does not hold for all proof instances, and Theorem 1 — and therefore Theorem 5 — are not established by the given proof. This is not an omitted detail; it is a concrete counterexample to the soundness of the interpolating system.\n\nOther soft spots reinforce the conditional verdict: the completeness argument for the sequent systems is only sketched, several rule families are omitted, and the title/abstract promise Craig-Lyndon interpolation while the paper itself only claims Craig. None of those are fatal by themselves, but they are consistent with a paper that is not yet referee-ready.\n\nThe approach may be repairable — perhaps the axiom needs a different interpolant or a different formulation — and the two-stage idea is a solid starting point. As written, though, the proof does not go through.\n\nThis deserves a serious referee: the idea is significant and the flaws are specific and addressable. I would send it out, but with an expectation of major revision, and I would point the referee directly at Ax-nh-1-LR and the conditions (I1)–(I3).","headline":"The two-stage nh-operator interpolation idea is genuinely new, but the presented sequent system has a concrete unsound axiom (Ax-nh-1-LR) that breaks the central theorem as stated.","tokens_in":10466,"tokens_out":6281,"would_cite":false,"duration_ms":59666,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03B50","03B55","03F05"],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper proves Craig interpolation for the three-valued logic of here and there by a constructive two-stage method based on Mints' sequent system.","keywords":["here-and-there logic","Gödel logic G3","Craig interpolation","Maehara's method","Mints' sequent system","split-sequents","strong equivalence in logic programming","answer set programming"],"falsifier":"Using the truth table printed in the paper, consider the axiom Ax-nh-1 (Γ⇒∆, A, nh(A)) and its stated soundness condition: the implication B→(C∨A∨nh(A)) must be valid. Under the assignment A=NF, B=T, C=F, the table gives nh(NF)=F, hence A∨nh(A)=NF∨F=NF, so the consequent C∨A∨nh(A) is not T and the implication is invalid, contradicting soundness of Ax-nh-1 unless the table's entry for nh(NF) is corrected to T. This single truth-table check settles whether the system as printed is sound and, with it, whether the claimed interpolation construction can be trusted.","tokens_in":9587,"feed_emoji":"🔗","tokens_out":17046,"duration_ms":143404,"temperature":0.7,"pith_summary":"The paper aims to prove that the propositional logic of here and there (HT), also known as Gödel's G3, has a constructive Craig interpolation property: whenever an HT formula A entails an HT formula B, an HT formula C can be effectively computed such that A entails C, C entails B, and C contains only atoms that occur in both A and B. To get this, the paper adapts Maehara's method to a variation of Mints' sequent system for HT, working directly on HT formulas rather than through a classical encoding. The construction proceeds in two stages: first, a preliminary interpolant is built in an intermediate logic that adds the operator nh(A), read as 'A is false in the here world', and this interpolant is then converted to a genuine HT formula by a CNF-based transformation that turns each clause nh(E1)∨...∨nh(Em)∨F into the implication E1∧...∧Em→F. The significance is that it transfers a recently introduced interpolation technique from the realm of classical logic programming encodings into the sequent-system setting, which the author expects can be extended to Craig-Lyndon interpolation.","feed_headline":"Build Craig interpolants from sequent proofs of here-and-there logic","feed_subtitle":"Two-stage sequent method produces interpolants that use only common atoms of the two formulas.","key_machinery":"The key mechanism is Maehara's interpolation method with split-sequents: a sequent is decorated with a relative interpolant H satisfying the two entailment conditions VΓL |= H∨V∆L and VΓR∧H |= V∆R together with the vocabulary condition voc(H) ⊆ voc(VΓL∧¬V∆L) ∩ voc(¬VΓR∨V∆R), and each axiom and rule propagates H inductively. To handle HT, the paper modifies Mints' sequent system, adding a third succedent rule for implication (⇒→*) that, read bottom-up, introduces the operator nh(A), whose argument is an atom; the operator is governed by axioms Ax-nh-1 and Ax-nh-2. In the interpolating system, nh only ever appears with right provenance in the succedent, which is what makes the preliminary inte","core_discovery":"The central result is Theorem 5: for any HT-formulas A and B with A|=B, there exists an HT-formula C with A|=C and C|=B, whose atoms are restricted to the common vocabulary, and C can be effectively constructed from a proof of A⇒B in a slight variation of Mints' sequent system for HT. The proof proceeds by first establishing Theorem 1, which produces a preliminary interpolant C' in the form of an nh-NNF formula (a formula using atoms, negated atoms, double-negated atoms, applications of nh to atoms, conjunction, and disjunction) from the same sequent proof, and then applying Theorem 4, which converts any nh-NNF formula C' entailed by a HT-formula A into an HT-formula C with A|=C, C|=C', and","pith_inferences":["One testable upshot: because the two non-polynomial steps (body normalization of B and CNF conversion of C') are the only apparent sources of complexity, replacing them with Tseitin-style encodings might yield a polynomial-time interpolation construction for propositional HT without expanding the interpolant vocabulary — a conjecture the paper's open-issues section plants but does not settle.","The nh operator, as an explicitly non-definable strengthening of HT, offers a template for proving interpolation in intermediate logics by extension-and-reduction: prove interpolation in an enriched language, then show the extra connectives can be eliminated from interpolants by a local formula transformation.","The author expects the method to strengthen to Craig-Lyndon interpolation (where polarities of atoms are also tracked); the split-sequent provenance structure already carries enough information to support polarity tagging, so the extension is a concrete research avenue rather than a mere wish."],"forward_implications":["Given any sequent proof of A⇒B in the modified Mints' system, an HT interpolant C is effectively computable, so interpolation is realized as a byproduct of proof search rather than a separate model-theoretic argument.","The interpolant vocabulary is contained in the common atoms of A and B (Theorem 5, condition 2), matching the classical Craig property.","The conversion of the preliminary interpolant to the final HT interpolant is independent of the formula A, only depending on the nh-NNF formula C'.","The method provides a sequent-based alternative to the classical-encoding approach to HT interpolation, fulfilling the note's stated objective."],"fun_headline_variants":["Sequent proofs yield two-stage interpolants for HT logic","Here-and-there interpolation via two-stage sequent system","Two-stage sequents construct interpolants for HT logic","Effective Craig-Lyndon interpolants from Mints' proofs"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"The whole construction depends on the claim that the modified sequent system is complete for HT and for the intermediate logic that adds the nh operator — a claim the paper sketches by analogy with Mints rather than proving — since the interpolant is read off a proof in that system; if completeness fails, a valid entailment A|=B may have no proof at all, so the construction cannot even start.","fun_headline_variants_meta":{"raw":{"variants":["Sequent proofs yield two-stage interpolants for HT logic","Here-and-there interpolation via two-stage sequent system","Two-stage sequents construct interpolants for HT logic","Effective Craig-Lyndon interpolants from Mints' proofs"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001368,"raw_usage":{"total_tokens":5384,"prompt_tokens":746,"completion_tokens":4638,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":490,"completion_tokens_details":{"reasoning_tokens":4571}},"tokens_in":490,"tokens_out":4638,"duration_ms":27526,"temperature":1.0,"reasoning_tokens":4571,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-03T12:08:01.614409+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Using the truth table printed in the paper, consider the axiom Ax-nh-1 (Γ⇒∆, A, nh(A)) and its stated soundness condition: the implication B→(C∨A∨nh(A)) must be valid. Under the assignment A=NF, B=T, C=F, the table gives nh(NF)=F, hence A∨nh(A)=NF∨F=NF, so the consequent C∨A∨nh(A) is not T and the implication is invalid, contradicting soundness of Ax-nh-1 unless the table's entry for nh(NF) is corrected to T. This single truth-table check settles whether the system as printed is sound and, with it, whether the claimed interpolation construction can be trusted.","supporting_citations":[],"review_version":2}