Craig-Lyndon Interpolation for the Logic of Here and There with a Variation of Mints' Sequent System

Christoph Wernhard

REVIEW 4 major objections 4 minor 16 references

Craig-Lyndon Interpolation for the Logic of Here and There with a Variation of Mints' Sequent System

T0 review · 4 major / 4 minor · reviewed 2026-08-03 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read 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.

desk verdict 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. read the letter →

arxiv 2601.04080 v4 pith:75J4HPOJ submitted 2026-01-07 cs.LO

Christoph Wernhard This is my paper · ORCID

classification cs.LO MSC 03B5003B5503F05

keywords here-and-therelogicGödelG3CraiginterpolationMaehara'smethodMints'sequentsystemsplit-sequentsstrongequivalenceinprogramminganswerset

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

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.

What carries the argument

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

What would settle it

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.

Watch

Extended reading notes

Core claim

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

Load-bearing premise

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.

Editorial extensions

If this is right

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.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

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.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the 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.

But 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.

Other 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.

The 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.

This 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).

Referee Report

4 major / 4 minor

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.

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 (4)

[§5.3, Ax-nh-1-LR (and §3, Ax-nh-1)] 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.
[§5.3, 'Further Axioms and Rules that are not Presented'] 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.
[§6, Theorem 4 proof] 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.
[§3, Completeness] 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.

minor comments (4)

[Title and Abstract; §7] 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.
[§5.3, Ax-1-RL] 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.
[§4, Example rules] 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.
[§2, grammar] 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.

Circularity Check

0 steps flagged · score 2.0 of 10

No significant circularity: self-citations are contextual, not load-bearing.

full rationale

The derivation chain of Theorem 5 is a two-stage Maehara-style construction and does not reduce to its inputs. Theorem 1 is proved by an induction on split-sequents: axioms are checked against (I1)-(I3), and the rule presentations give the transfer properties; the root interpolant satisfies (I1)-(I3) by construction, not by preassuming an interpolant exists. Theorem 4 is proved locally: from A|=C' and the nh truth table, a CNF conversion yields the HT formula C as a conjunction of implications, and the proof does not invoke the desired interpolant. The only self-citations are [6] (the same author's earlier classical-encoding method, used as motivation and as the source of the two-stage idea) and [2] (an edited volume for general context); neither is load-bearing. In particular, Theorem 4 is not taken on faith from [6, Theorem 11]: a proof is given in the text. Maksimova's external interpolation theorem and Mints' sequent system are not self-citations. The explicitly omitted rules in Sec. 5.3 and the sketched completeness proof in Sec. 3 are presentation or completeness gaps, not circular steps. The suspected failure of (I1) for Ax-nh-1-LR is not supported by Fig. 1: at A=NF the table gives nh(A)=T, so nh(A)∨A evaluates to T; in any case, a soundness issue would be a correctness matter, not circularity. Overall, no predicted quantity is a fitted input and no definition or citation chain imports the target theorem.

Assumptions & free parameters 0 free parameters · 5 assumptions · 1 invented entities

No numerical free parameters; assumptions are proof-theoretic. The most consequential are the completeness of the modified sequent system (sketched) and the semantic equivalences governing nh, particularly the conversion in Theorem 4. The nh operator is an auxiliary connective invented for the interpolation construction and removed in the final interpolant.

assumptions (5)

domain assumption The variation of Mints' sequent system is complete for propositional HT and for HTnh-formulas.
Stated in §3 ('Completeness') with only a sketch; the interpolation construction in Theorem 1 requires a proof to exist whenever A|=B.
standard math The Maehara split-sequent conditions (I1)-(I3) correctly characterize relative interpolants and transfer under all rules.
Standard method (§4); the paper verifies only example rules and relies on the standard transfer argument.
domain assumption The new rule ⇒→*R is sound, justified by the equivalence C→(D∨(A→B)) ≡ (C→(D∨nh(A)∨B))∧((¬B∧C)→(D∨¬A)).
Given in §3; the equivalence is asserted, not proved.
domain assumption For every nh-NNF clause D=nh(E1)∨...∨nh(Em)∨F, the formula D∧¬¬D′ is equivalent to E1∧...∧Em→F (Theorem 4).
This semantic equivalence is the load-bearing step of the second stage; presented with references to proof transformations but not formalized.
standard math Any HT formula can be body-normalized and any nh-NNF formula can be converted to CNF without altering semantics.
Body-normalization is attributed to Mints (§5.1); CNF conversion is a classical construction used in Theorem 4; both are asserted rather than proved.

invented entities (1)

nh(A) operator
purpose: Auxiliary truth-functional connective that is true when A is false in the 'here' world; used to carry preliminary interpolants in stage 1 and then eliminated in stage 2.
The operator is defined by a truth table inside the paper and only appears in intermediate interpolants; no external observable counterpart is claimed. Its behavior is fully specified, so it is honest, but it is not an independent empirical entity.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Craig-Lyndon Interpolation for the Logic of Here and There with a Variation of Mints' Sequent System." pith.science (2026). https://pith.science/paper/75J4HPOJ

@misc{pith2026260104080,
  author       = {Pith},
  title        = {Pith review of: Craig-Lyndon Interpolation for the Logic of Here and There with a Variation of Mints' Sequent System},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/75J4HPOJ}},
  note         = {Machine review of arXiv:2601.04080}
}

abstract

We present a variation of Maehara's method to construct Craig-Lyndon interpolants for the three-valued propositional logic of here and there (HT), also known as G\"odel's $G_3$, a superintuitionistic logic of importance in logic programming. Our method adapts a recent interpolation technique that operates on classically encoded logic programs to a variation of Mints' sequent system for HT. The approach is characterized by two stages: First, a preliminary interpolant is constructed, a formula that is an interpolant in some sense but not yet the desired HT formula. In the second stage, an actual HT interpolant is obtained from this preliminary interpolant. With the classical encoding, the preliminary interpolant is a classical Craig-Lyndon interpolant for classical encodings of the two input HT formulas. In the presented adaptation, the sequent system operates directly on HT formulas, and the preliminary interpolant is in a nonclassical logic that generalizes HT by an additional logic operator.

Figures

Figures reproduced from arXiv: 2601.04080 by the authors.

Review history (2 revisions) →

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

16 extracted references

[6]

In: Benzmüller, C., Heule, M., Schmidt, R

Heuer, J., Wernhard, C.: Synthesizing strongly equivalent logic programs: Beth definability for answer set programs via Craig interpolation in first-order logic. In: Benzmüller, C., Heule, M., Schmidt, R. (eds.) IJCAR 2024. LNCS (LNAI), vol. 14739, pp. 172–193. Springer (2024).https://doi.org/10.1007/ 978-3-031-63498-7_11

2024
[1]

A Study in the Philosophy of Sci- ence

Beth, E.W.: The Foundations of Mathematics. A Study in the Philosophy of Sci- ence. North-Holland (1959)

1959
[2]

(eds.): The- ory and Applications of Craig Interpolation

ten Cate, B., Jung, J.C., Koopmann, P., Wernhard, C., Wolter, F. (eds.): The- ory and Applications of Craig Interpolation. Ubiquity Press (2026), to appear; preprints accessible fromhttps://cibd.bitbucket.io/taci/ 14 Christoph Wernhard

2026
[3]

Springer, 2nd edn

Fitting, M.: First-Order Logic and Automated Theorem Proving. Springer, 2nd edn. (1995).https://doi.org/10.1007/978-1-4612-2360-3

doi:10.1007/978-1-4612-2360-3 1995
[4]

Oxford Univ

Gabbay, D.M., Maksimova, L.L.: Interpolation and Definability: Modal and Intu- itionistic Logics. Oxford Univ. Press (2005).https://doi.org/10.1093/acprof: oso/9780198511748.001.0001

arXiv 2005
[5]

JAIR42, 917–943 (2011)

Gabbay, D.M., Pearce, D., Valverde, A.: Interpolable formulas in equilibrium logic and answer set programming. JAIR42, 917–943 (2011)

2011
[7]

ACM Trans

Lifschitz, V., Pearce, D., Valverde, A.: Strongly equivalent logic programs. ACM Trans. Comp. Log.2(4), 526–541 (2001).https://doi.org/10.1145/383779. 383783

doi:10.1145/383779 2001
[8]

Sugaku12, 235– 237 (1960)

Maehara, S.: On the interpolation theorem of Craig (Japanese). Sugaku12, 235– 237 (1960)

1960

Show all 16 references

[9]

Algebra and Logic16(6), 427–455 (1977)

Maksimova, L.L.: Craig’s theorem in superintuitionistic logics and amalgamable varieties of pseudo-Boolean algebras. Algebra and Logic16(6), 427–455 (1977). https://doi.org/10.1007/BF01670006

1977 doi
[10]

Studia Log- ica38(4), 419–428 (1979).https://doi.org/10.1007/BF00370479

Maksimova, L.L.: Interpolation properties of superintuitionistic logics. Studia Log- ica38(4), 419–428 (1979).https://doi.org/10.1007/BF00370479

1979 doi
[11]

Mints, G.: Cut-free formulations for a quantified logic of here and there. Ann. Pure Appl. Log.162(3), 237–242 (2010).https://doi.org/10.1016/J.APAL.2010.09. 009

2010 doi
[12]

In: Gebser, M., Inclezan, D., Ricca, F., Carro, M., Truszczynski, M

Otten, J., Schaub, T.: Implementing the first-order logic of here and there. In: Gebser, M., Inclezan, D., Ricca, F., Carro, M., Truszczynski, M. (eds.) ICLP 2025. EPTCS, vol. 439, pp. 453–468 (2026).https://doi.org/10.4204/EPTCS.439.31

2025 doi
[13]

Pearce, D., Valverde, A.: Synonymous theories and knowledge representations in answer set programming. J. Comput. Syst. Sci.78(1), 86–104 (2012).https:// doi.org/10.1016/J.JCSS.2011.02.013

2012 doi
[14]

Springer (1968), also republished with correc- tions by Dover publications, 1995

Smullyan, R.M.: First-Order Logic. Springer (1968), also republished with correc- tions by Dover publications, 1995

1968
[15]

North-Holland, second edn

Takeuti, G.: Proof Theory. North-Holland, second edn. (1987)

1987
[16]

Cambridge University Press, second edn

Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory. Cambridge University Press, second edn. (2000)

2000

Pith tools

Reviewed August 3, 2026 · model on record in the stance chip above.

[1] [6]

In: Benzmüller, C., Heule, M., Schmidt, R

Heuer, J., Wernhard, C.: Synthesizing strongly equivalent logic programs: Beth definability for answer set programs via Craig interpolation in first-order logic. In: Benzmüller, C., Heule, M., Schmidt, R. (eds.) IJCAR 2024. LNCS (LNAI), vol. 14739, pp. 172–193. Springer (2024).https://doi.org/10.1007/ 978-3-031-63498-7_11

2024

[2] [1]

A Study in the Philosophy of Sci- ence

Beth, E.W.: The Foundations of Mathematics. A Study in the Philosophy of Sci- ence. North-Holland (1959)

1959

[3] [2]

(eds.): The- ory and Applications of Craig Interpolation

ten Cate, B., Jung, J.C., Koopmann, P., Wernhard, C., Wolter, F. (eds.): The- ory and Applications of Craig Interpolation. Ubiquity Press (2026), to appear; preprints accessible fromhttps://cibd.bitbucket.io/taci/ 14 Christoph Wernhard

2026

[4] [3]

Springer, 2nd edn

Fitting, M.: First-Order Logic and Automated Theorem Proving. Springer, 2nd edn. (1995).https://doi.org/10.1007/978-1-4612-2360-3

doi:10.1007/978-1-4612-2360-3 1995

[5] [4]

Oxford Univ

Gabbay, D.M., Maksimova, L.L.: Interpolation and Definability: Modal and Intu- itionistic Logics. Oxford Univ. Press (2005).https://doi.org/10.1093/acprof: oso/9780198511748.001.0001

arXiv 2005

[6] [5]

JAIR42, 917–943 (2011)

Gabbay, D.M., Pearce, D., Valverde, A.: Interpolable formulas in equilibrium logic and answer set programming. JAIR42, 917–943 (2011)

2011

[7] [7]

ACM Trans

Lifschitz, V., Pearce, D., Valverde, A.: Strongly equivalent logic programs. ACM Trans. Comp. Log.2(4), 526–541 (2001).https://doi.org/10.1145/383779. 383783

doi:10.1145/383779 2001

[8] [8]

Sugaku12, 235– 237 (1960)

Maehara, S.: On the interpolation theorem of Craig (Japanese). Sugaku12, 235– 237 (1960)

1960