2
$\begingroup$

Consider Propositional Lax Logic ($PLL$)

The Hilbert system of $PLL$ takes as axiom schemata all theorems of (or a complete set of axioms for) the Intuitionistic propositional calculus plus the modal axiom schemata $\bigcirc R, \bigcirc M, \bigcirc S$ below. The inference rules are Modus Ponens and the rule "from $M \supset N$ infer $\bigcirc M \supset \bigcirc N$":

$$\text{Axiom} \bigcirc R: \hspace{0.5cm}M \supset \bigcirc M$$ $$\text{Axiom} \bigcirc M: \hspace{0.8cm} (\thinspace \bigcirc \bigcirc M\thinspace) \supset \bigcirc M$$ $$\text{Axiom} \bigcirc S: \hspace{0.8cm}(\bigcirc M \land \bigcirc N) \supset \bigcirc(M \land N)$$

A proof of the modal collapse (We can derive both $\bigcirc M \supset M$ and $M \supset \bigcirc M$) of $PLL$ obtained by adding the Excluded Middle (EM) and $\neg \bigcirc false$ was given in this answer: Modal collapse upon addition of the law of the excluded middle to an Intuitionistic modal logic.

However, I was wondering:

(1) Does the proof of the modal collapse go through if we add the law of the excluded middle and $\neg \bigcirc \bot$ to a classical multiplicative linear logic? (i.e, if we abandon the structural rules of contraction and weakening) and adopt the following rules)

$$ \frac{\qquad }{A \vdash A} \,{Id} $$

$$ \frac{\Gamma\vdash B, \Delta \qquad B, \Gamma'\vdash \Delta'}{\Gamma, \Gamma' \vdash \Delta', \Delta} \,{Cut} $$

$$ \frac{\Gamma\vdash A, \Delta \qquad \Gamma', B\vdash \Delta'}{\Gamma, \Gamma', A \rightarrow B \vdash \Delta, \Delta'} \,{\rightarrow L} $$

$$ \frac{\Gamma, A \vdash B, \Delta}{\Gamma \vdash A \rightarrow B, \Delta} \,{\rightarrow R} $$

$$ \frac{\Gamma \vdash A, \Delta'}{\Gamma \vdash \bigcirc A, \Delta'} \,{\bigcirc R} $$

$$ \frac{\Gamma, A \vdash \bigcirc B, \Delta' \qquad }{\Gamma, \bigcirc A \vdash \bigcirc B, \Delta'} \,{\bigcirc L} $$

(2) Does the proof of the modal collapse go through if we add the law of the excluded middle and $\neg \bigcirc \bot$ to the following sequent calculus but treat $\rightarrow$ as primitive, and not as definable via other connectives, as it usually is in linear logic (in linear logic $\rightarrow$ is usually defined as $\neg A \thinspace \Box \thinspace B$, where we use $\Box$ to denote the multiplicative 'or')

$$ \frac{\qquad }{A \vdash A} \,{Id} $$

$$ \frac{\Gamma\vdash B \qquad B, \Delta\vdash C}{\Gamma, \Delta \vdash C} \,{Cut} $$

$$ \frac{\Delta\vdash A \qquad \Gamma, B\vdash C}{\Gamma, \Delta, A \rightarrow B \vdash C} \,{\rightarrow L} $$

$$ \frac{\Gamma, A \vdash B}{\Gamma \vdash A \rightarrow B} \,{\rightarrow R} $$

$$ \frac{\Gamma \vdash A}{\Gamma \vdash \bigcirc A} \,{\bigcirc R} $$

$$ \frac{\Gamma, A \vdash \bigcirc B \qquad }{\Gamma, \bigcirc A \vdash \bigcirc B} \,{\bigcirc L} $$

$\endgroup$

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.