Separation conjecture for core and non-core rules in the calculus of structures

Let TT and RR be structures, and let SKS\mathsf{SKS} be the calculus-of-structures system for classical propositional logic. Partition its rules into the core fragment and the non-core fragment, with identity and cut written separately. Let T,T,R,RT',T”,R”,R' be intermediate structures.

Separation conjecture. For every derivation TSKSRT\vdash_{\mathsf{SKS}}R, there is a derivation of the form

TnoncoreT{identity}TcoreR{dual identity}RnoncoreR.T\vdash_{\mathrm{non-core}}T'\vdash_{\{\text{identity}\}}T”\vdash_{\mathrm{core}}R”\vdash_{\{\text{dual identity}\}}R'\vdash_{\mathrm{non-core}}R.

The conjecture asks whether switch and medial, and more generally the core and non-core fragments, can be separated into phases. The source presents this as a problem for future work and notes that related separation results had been proved for two other systems.

Sources & referencesView supporting material

Primary source

Kai Bruennler, “Locality for Classical Logic”, arXiv:math/0301317 (2003).

Progress summary

Never refreshed

Nothing recorded yet. Refresh searches the literature and the public web for attempts on this problem, and writes the first summary here.

Solutions 0

No solutions have been posted yet.