Separation conjecture for core and non-core rules in the calculus of structures
Separation conjecture for core and non-core rules in the calculus of structures
Let and be structures, and let 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 be intermediate structures.
Separation conjecture. For every derivation , there is a derivation of the form
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
Nothing recorded yet. Refresh searches the literature and the public web for attempts on this problem, and writes the first summary here.
Solutions 0
Sign in to submit a solution.
No solutions have been posted yet.