I'm sadly an outsider to nonclassical propositional logics. All terminology below comes from Humberstone's book The Connectives, specifically section 4.2.

A new connective - a bit more precisely, a set of rules in some appropriate form for said connective - is conservative over a deductive system $\mathcal{L}$ if adjoining it does not result in any new valid sequents in the original language of $\mathcal{L}$ itself. The standard non-example of this with $\mathcal{L}$ = classical propositional logic is Prior's $\mathsf{tonk}$, with rule set $$A\vee B\vdash A\mathsf{\,tonk\,}B\quad\mbox{and}\quad A\mathsf{\,tonk\,}B\vdash A\wedge B.$$

Interestingly, two individually-conservative connectives may not be jointly conservative. Elaborating on C.G. McKay 1985, Humberstone observes that the connectives $O$ and $\perp$ described by the schemes$$(A\rightarrow OA)\rightarrow A\quad\mbox{and}\quad \perp\rightarrow A$$ are separately-but-not-jointly conservative over positive logic (= the fragment of propositional intuitionistic logic using only $\wedge,\vee,\rightarrow$).

This suggests the following. Say that a connective $\star$ (or more accurately again, a set of intro/elim rules for same) is hereditarily conservative over $\mathcal{L}$ iff $\star$ and $@$ are jointly conservative over $\mathcal{L}$ whenever $@$ is conservative over $\mathcal{L}$. Obviously any "already-definable" connective is hereditarily conservative, but beyond this not much is clear to me. I'm interested in any information about hereditary conservativity, but to get things off the ground here's a concrete question:

Are there any hereditarily conservative connectives over positive logic which are not already definable over positive logic?

(I could not find an answer to this question in Humberstone, but that book is large enough that I'm not confident in my searching abilities. Meanwhile, the "universal-algebra" tag is admittedly tenuous but there is apparently no "nonclassical-logic" or "propositional-logic" tag, so it seems the best available.)

I'm sadly an outsider to nonclassical propositional logics. All terminology below comes from Humberstone's book The Connectives, specifically section 4.2.

A new connective - a bit more precisely, a set of rules in some appropriate form for said connective - is conservative over a deductive system $\mathcal{L}$ if adjoining it does not result in any new valid sequents in the original language of $\mathcal{L}$ itself. The standard non-example of this with $\mathcal{L}$ = classical propositional logic is Prior's $\mathsf{tonk}$, with rule set $$A\vee B\vdash A\mathsf{\,tonk\,}B\quad\mbox{and}\quad A\mathsf{\,tonk\,}B\vdash A\wedge B.$$

Interestingly, two individually-conservative connectives may not be jointly conservative. Elaborating on C.G. McKay 1985, Humberstone observes that the connectives $O$ and $\perp$ described by the schemes$$(A\rightarrow OA)\rightarrow A\quad\mbox{and}\quad \perp\rightarrow A$$ are separately-but-not-jointly conservative over positive logic (= the fragment of propositional intuitionistic logic using only $\wedge,\vee,\rightarrow$).

This suggests the following. Say that a connective $\star$ (or more accurately again, a set of appropriate rules for same) is hereditarily conservative over $\mathcal{L}$ iff $\star$ and $@$ are jointly conservative over $\mathcal{L}$ whenever $@$ is conservative over $\mathcal{L}$. Obviously any "already-definable" connective is hereditarily conservative, but beyond this not much is clear to me. I'm interested in any information about hereditary conservativity, but to get things off the ground here's a concrete question:

Are there any hereditarily conservative connectives over positive logic which are not already definable over positive logic?

(I could not find an answer to this question in Humberstone, but that book is large enough that I'm not confident in my searching abilities. Meanwhile, the "universal-algebra" tag is admittedly tenuous but there is apparently no "nonclassical-logic" or "propositional-logic" tag, so it seems the best available.)