If we consider the sequent calculus formalization of the positive fragment of the logic of ticket entailment (let's label the logic $LT_{+\leftarrow\rightarrow}^{\circ t})$, that is a Lindenbaum algebra, we have various axioms (classic sequent calculus axioms for substructural logics) and the following structural rules:


$\cfrac{\alpha[\beta;(\gamma;\delta)]\vdash A}{\alpha[(\beta;\gamma);\delta]\vdash A}$ $\;$ $\cfrac{\alpha[\gamma;(\beta;\delta)]\vdash A}{\alpha[(\beta;\gamma);\delta]\vdash A} \;\cfrac{\alpha[(\beta;\gamma);\gamma]\vdash A}{\alpha[\beta;\gamma]\vdash A} \;\cfrac{\alpha[\beta]\vdash A}{\alpha[t;\beta]\vdash A} \; \cfrac{\alpha[t;t]\vdash A}{\alpha[t]\vdash A}$


If we add to the logic two connectives $(\leftarrow)$ and $(\circ)$, we have two more structural rules:


$\cfrac{\alpha[t;\beta;\gamma]\vdash A}{\alpha[\beta;(t;\gamma)]\vdash A}$, comes with $(\vdash\leftarrow)$ and $(\leftarrow\vdash)$ rules;


$\cfrac{\alpha[(t;\beta);\gamma]\vdash A}{\alpha[t;(\beta;\gamma)]\vdash A}$, comes with $(\vdash\circ)$ and $(\circ\vdash)$ rules.


The only other connective that we admit in our sequent calculus is $\rightarrow$, and some properties like the admissibility of the Cut theorem or Soundness and Completeness are preserved in the extension to a logic with $\leftarrow$ and $\circ$


Why are the two added rules necessary (or not)? The hint of the book (is the chapter of Relevance Logic in Philosophy of Logic, vol. 5 of Handbook of the Philosophy of Science, Gabbay, D., P. Thagard and J. Woods) is that they are necessary for replacement and equivalent classes.

So, I guess the question, in general, is: how does replacement work for equivalent classes in a Lindenbaum algebra? And how is this related to the structural rules?


  • $\begingroup$ Maybe we need some references to correctly read the formalism: book, lectures... $\endgroup$ – Mauro ALLEGRANZA Nov 27 '17 at 12:56
  • $\begingroup$ The first two rules are Permutation; the third one is Contraction; fourth is Weakening. And the fifth is ? $\endgroup$ – Mauro ALLEGRANZA Nov 28 '17 at 10:00
  • $\begingroup$ I think the fifth is some sort of monotonicity for the truth constant $\endgroup$ – Rameau Nov 29 '17 at 11:00

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.