arXiv Analytics

Sign in

arXiv:1907.05411 [math.LO]AbstractReferencesReviewsResources

Proof Theory for Positive Logic with Weak Negation

Marta Bílková, Almudena Colacito

Published 2019-07-11Version 1

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.

Related articles: Most relevant | Search more
arXiv:1102.0596 [math.LO] (Published 2011-02-03)
A sneak preview of proof theory of ordinals
arXiv:0911.2097 [math.LO] (Published 2009-11-11, updated 2010-07-05)
Compactness in positive logic
arXiv:1007.0844 [math.LO] (Published 2010-07-06)
Proof theory for theories of ordinals III: $Π_{N}$-reflection