pith. sign in

arxiv: 1907.05411 · v1 · pith:QKUSRY4Gnew · submitted 2019-07-11 · 🧮 math.LO

Proof Theory for Positive Logic with Weak Negation

Marta B\'ilkov\'a , Almudena Colacito This is my paper

Pith reviewed 2026-05-24 22:48 UTC · model grok-4.3

classification 🧮 math.LO
keywords sequent calculusCraig interpolationPSPACE-completenessweak negationJohansson logicproof theoryintuitionistic logicsubstructural logic
0
0 comments X

The pith

Subsystems of Johansson's logic with weak negation admit cut-free sequent calculi that establish Craig interpolation and PSPACE-completeness.

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

The paper develops sequent calculi for extensions of the positive fragment of intuitionistic logic by weak negations, viewed as subsystems of Johansson's logic. Cut-free complete versions of these calculi are constructed and directly applied to prove the Craig interpolation property. Loop-checking history mechanisms are added to obtain alternative calculi whose termination is established. The termination result yields that the logical systems are decidable in PSPACE.

Core claim

By introducing cut-free complete sequent calculi for the positive logic with weak negation, the systems are shown to satisfy Craig interpolation. Alternative calculi incorporating a loop-checking history mechanism terminate, allowing the conclusion that the systems are PSPACE-complete.

What carries the argument

Cut-free sequent calculi with an added loop-checking history mechanism, used to obtain completeness, interpolation proofs, and termination.

Load-bearing premise

The specific definition of weak negation permits the construction of cut-free sequent rules that remain complete and support the interpolation and termination arguments.

What would settle it

A concrete formula or sequent in one of the systems for which interpolation fails to hold, or a derivation sequence in the loop-checking calculus that fails to terminate.

Figures

Figures reproduced from arXiv: 1907.05411 by Almudena Colacito, Marta B\'ilkov\'a.

Figure 1
Figure 1. Figure 1: The systems G3 In Figures 1 and 2, four different sequent systems are presented. Keeping the rules for the positive connectives and the structural rules fixed, the rule (n) defines a proof system for N-algebras; by adding the rule (nef) and by substituting the rule (n) with (copc), we obtain systems for the two proper subvarieties 4 [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Structural rules of N-algebras defined, respectively, by 2.2 and 2.3. Finally, by adding the rule (an) to the system obtained with (copc), we obtain a sequent proof system for contrapositionally complemented lattices. Sequent proof systems for MPC were already introduced, e.g., in [31], using a different presentation of MPC. In fact, MPC is often formulated with the negation ¬ϕ as a defined connective ϕ → … view at source ↗
Figure 3
Figure 3. Figure 3: Rules for positive connectives in the systems [PITH_FULL_IMAGE:figures/full_fig_p015_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Rules for negation in the systems G3Hist Lemma 5.3. The following contraction rule is admissible in G3Hist H | Γ, α, α ⇒ ϕ H | Γ, α ⇒ ϕ Proof. By induction on the height of a derivation of the premise. We focus on the induction step, and on the non-intuitionistic rules. Suppose that the last step in the derivation is an instance of (n1) of the form ∅ | Γ, ¬α, ¬α, β ⇒ α ∅ | Γ, ¬α, ¬α, α ⇒ β H | Γ, ¬α, ¬α ⇒ … view at source ↗
read the original abstract

Proof-theoretic methods are developed for subsystems of Johansson's logic obtained by extending the positive fragment of intuitionistic logic with weak negations. These methods are exploited to establish properties of the logical systems. In particular, cut-free complete sequent calculi are introduced and used to provide a proof of the fact that the systems satisfy the Craig interpolation property. Alternative versions of the calculi are later obtained by means of an appropriate loop-checking history mechanism. Termination of the new calculi is proved, and used to conclude that the considered logical systems are PSPACE-complete.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 4 minor

Summary. The paper develops proof-theoretic methods for subsystems of Johansson's minimal logic, obtained by extending the positive fragment of intuitionistic logic with various forms of weak negation. It constructs cut-free sequent calculi for these systems, uses them to prove the Craig interpolation property, introduces loop-checking history mechanisms to obtain terminating variants, proves termination of the resulting calculi, and concludes that the systems are PSPACE-complete.

Significance. If the results hold, the work supplies a uniform sequent-calculus treatment of these weak-negation extensions, yielding both interpolation theorems and tight complexity bounds via explicit, terminating proof search. The constructive character of the arguments (cut-free completeness plus loop-checking termination) is a clear strength for the field of proof theory for non-classical logics.

minor comments (4)
  1. §3.2: the side-condition on the (R¬) rule is stated in terms of 'not occurring free,' but the precise notion of free occurrence for the weak-negation connective is not defined until §2.4; a forward reference or inline clarification would help.
  2. §4.3, Theorem 4.12: the induction on the height of the derivation in the interpolation proof assumes that the interpolant is constructed uniformly for all premises, but the case for the (L¬) rule is only sketched; an explicit inductive clause would make the argument easier to verify.
  3. §5.2: the loop-checking mechanism is described via a history set H, yet the precise update rule for H when a new sequent is added is given only informally; a formal recursive definition or pseudocode would improve clarity.
  4. The paper cites Johansson (1936) and several sequent-calculus papers on minimal logic, but does not reference recent work on interpolation for weak-negation logics (e.g., papers on Nelson's logic or subminimal logics); adding one or two such references would situate the contribution more precisely.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive summary, recognition of the significance of the uniform sequent-calculus treatment, and recommendation of minor revision. No major comments appear in the report.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The derivation proceeds by explicitly constructing cut-free sequent calculi for the subsystems, proving their completeness directly from the rules, then using those calculi to derive Craig interpolation via standard proof-theoretic arguments, and finally obtaining terminating loop-checking variants whose termination is proved to establish PSPACE-completeness. None of these steps reduce to self-definition, fitted parameters renamed as predictions, or load-bearing self-citations; each property is established from the constructed rules and termination arguments rather than presupposed by them. The paper is self-contained against external benchmarks in the form of explicit rule sets and inductive proofs.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The work rests on standard background in intuitionistic logic and the specific choice of weak negation operators; no free parameters or invented entities are mentioned.

axioms (2)
  • standard math The positive fragment of intuitionistic logic obeys its standard axioms and rules.
    Base system being extended.
  • domain assumption Weak negation is defined so that sequent rules can be formulated without cut.
    Enables the cut-free calculi construction.

pith-pipeline@v0.9.0 · 5613 in / 1110 out tokens · 19202 ms · 2026-05-24T22:48:58.208329+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

32 extracted references · 32 canonical work pages

  1. [1]

    Bezhanishvili, G. , T. Moraschini , and J. G. Raftery , ‘Epimorphisms in varieties of residuated structures’, Journal of Algebra, 492 (2017), 185–211

    work page 2017

  2. [2]

    Bezhanishvili, N. , A. Colacito , and D. de Jongh , ‘A study of subminimal logics of negation and their modal co mpan- ions’, 12th International Tbilisi Symposium on Logic, Lang uage, and Computation. To appear

    work page

  3. [3]

    , Lattice theory, vol

    Birkhoff, G. , Lattice theory, vol. 25, Colloquium Publications edn., American Mathemat ical Society, 1967

    work page 1967

  4. [4]

    Caicedo, X. , and R. Cignoli , ‘An algebraic approach to intuitionistic connectives’, The Journal of Symbolic Logic , 66 (2001), 04, 1620–1636

    work page 2001

  5. [5]

    Ciardelli, I. , J. Groenendijk , and F. Roelofsen , ‘Inquisitive semantics’, NASSLLI Lecture Notes , 187 (2012)

    work page 2012

  6. [6]

    Ciardelli, I. , J. Groenendijk , and F. Roelofsen , ‘Inquisitive semantics: a new notion of meaning’, Language and Linguistics Compass , 7 (2013), 9, 459–476. 25

    work page 2013

  7. [7]

    , Minimal and Subminimal Logic of Negation , Master’s thesis, ILLC Master of Logic Series MoL-2016-14, Universiteit van Amsterdam

    Colacito, A. , Minimal and Subminimal Logic of Negation , Master’s thesis, ILLC Master of Logic Series MoL-2016-14, Universiteit van Amsterdam

    work page 2016

  8. [8]

    Colacito, A. , D. de Jongh , and A. L. V argas, ‘Subminimal negation’, Soft Computing , 21 (2017), 1, 165 – 174

    work page 2017

  9. [9]

    de Jongh, D. , and Z. Zhao , ‘Positive formulas in intuitionistic and minimal logic’, in International Tbilisi Symposium on Logic, Language, and Computation , Springer, 2013, pp. 175–189

    work page 2013

  10. [10]

    Ertola, R. C. , A. Galli , and M. Sagastume , ‘Compatible functions in algebras associated to extensio ns of positive logic’, Logic Journal of IGPL , 15 (2007), 1, 109–119

    work page 2007

  11. [11]

    Ertola, R. C. , and M. Sagastume , ‘Subminimal logic and weak algebras.’, Reports on Mathematical Logic , 44 (2009), 153–166

    work page 2009

  12. [12]

    Groenendijk, J. , and F. Roelofsen, ‘Inquisitive semantics and pragmatics’, in Workshop on Language, Communication, and Rational Agency at Stanford , 2009

    work page 2009

  13. [13]

    Gurevich, Y. , and I. Neeman , ‘Logic of infons: The propositional case’, ACM Transactions on Computational Logic (TOCL), 12 (2011), 2, 9

    work page 2011

  14. [14]

    Hazen, A. P. , ‘Is even minimal negation constructive?’, Analysis, 55 (1995), 105–107

    work page 1995

  15. [15]

    , Sequent Calculi for Proof Search in Some Modal Logics , Ph.D

    Heuerding, A. , Sequent Calculi for Proof Search in Some Modal Logics , Ph.D. thesis, Universit¨ at Bern, 1998

    work page 1998

  16. [16]

    Heuerding, A. , M. Seyfried , and H. Zimmermann , ‘Efficient loop-check for backward proof search in some non- classical propositional logics’, in International Workshop on Theorem Proving with Analytic Ta bleaux and Related Methods , Springer, 1996, pp. 210–225

    work page 1996

  17. [17]

    Howe, J. M. , ‘Theorem proving and partial proof search for intuitionis tic propositional logic using a permutation-free calculus with loop-checking’, Technical Report CS/96/12, University of St Andews, 1996

    work page 1996

  18. [18]

    Howe, J. M. , ‘Two loop detection mechanisms: a comparison’, in International Conference on Automated Reasoning with Analytic Tableaux and Related Methods , Springer, 1997, pp. 188–200

    work page 1997

  19. [19]

    Howe, J. M. , Proof Search Issues in Some Non-classical Logics , Ph.D. thesis, University of St Andrews, 1998

    work page 1998

  20. [20]

    , The Connectives , MIT Press, Cambridge, Ma, US, 2011

    Humberstone, L. , The Connectives , MIT Press, Cambridge, Ma, US, 2011

    work page 2011

  21. [21]

    , ‘Der Minimalkalk¨ ul, ein reduzierter intuitionistische r Formalismus’, Compositio mathematica , 4 (1937), 119–136

    Johansson, I. , ‘Der Minimalkalk¨ ul, ein reduzierter intuitionistische r Formalismus’, Compositio mathematica , 4 (1937), 119–136

    work page 1937

  22. [22]

    Kolmogorov, A. N. , ‘On the principle of excluded middle’, Matematicheskii Sbornik , 32 (1925), 24, 646–667

    work page 1925

  23. [23]

    , ‘On the interpolation theorem of Craig’, Sˆ ugaku, 12 (1960), 4, 235–237

    Maehara, S. , ‘On the interpolation theorem of Craig’, Sˆ ugaku, 12 (1960), 4, 235–237

    work page 1960

  24. [24]

    , Constructive Negations and Paraconsistency , vol

    Odintsov, S. , Constructive Negations and Paraconsistency , vol. 26 of Trends in Logic , Springer Science & Business Media, 2008

    work page 2008

  25. [25]

    Pitts, A. M. , ‘On an interpretation of second order quantification in firs t order intuitionistic propositional logic’, The Journal of Symbolic Logic , 57 (1992), 1, 33–52

    work page 1992

  26. [26]

    , ‘W eak negation in inquisitive semantics’, Journal of Logic, Language and Information , 24 (2015), 3, 323–355

    Punˇcoch´aˇr, V. , ‘W eak negation in inquisitive semantics’, Journal of Logic, Language and Information , 24 (2015), 3, 323–355

    work page 2015

  27. [27]

    Rasiow a, H., An Algebraic Approach to Non-classical Logics , Studies in Logic and the Foundations of Mathematics, North-Holland Publishing Company, 1974

    work page 1974

  28. [28]

    Rybakov, M., ‘Complexity of intuitionistic propositional logic and it s fragments’, Journal of Applied Non-Classical Logics , 18 (2008), 2-3, 267–292

    work page 2008

  29. [29]

    , ‘Der interpolationssatz der intuitionistischen pr¨ adikatenlogik’, Mathematische Annalen , 148 (1962), 3, 192– 200

    Sch¨utte, K. , ‘Der interpolationssatz der intuitionistischen pr¨ adikatenlogik’, Mathematische Annalen , 148 (1962), 3, 192– 200

    work page 1962

  30. [30]

    Statman, R., ‘Intuitionistic propositional logic is polynomial-spac e complete’, Theoretical Computer Science , 9 (1979), 1, 67–72

    work page 1979

  31. [31]

    Troelstra, A. S. , and H. Schwichtenberg , Basic Proof Theory , no. 43 in Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 2000

    work page 2000

  32. [32]

    , ‘The Johansson/Heyting letters and the birth of minimal lo gic’, ILLC Technical Notes X-2016-03, Universiteit van Amsterdam

    van der Molen, T. , ‘The Johansson/Heyting letters and the birth of minimal lo gic’, ILLC Technical Notes X-2016-03, Universiteit van Amsterdam. 26

    work page 2016