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.)

  • $\begingroup$ If I’m understanding the question right, there’s a trivial example: a connective with no rules at all. Did you have other constraints in mind to rule out this example? $\endgroup$ Mar 19 at 6:49
  • $\begingroup$ @PeterLeFanuLumsdaine doesn't this fall under "already definable over positive logic"? $\endgroup$
    – Holo
    Mar 19 at 12:33
  • $\begingroup$ @Holo: Not unless I’m either mistaken or badly misunderstanding some terminology here? To me, “$\star$ is already definable” means there’s some formula in two propositional variables $M[A,B]$, such that the rules for $\star$ imply that $\varphi \star \psi \dashv \vdash M[\varphi,\psi]$. If there are no rules at all for $\star$, then surely it’s not definable in this sense? $\endgroup$ Mar 19 at 16:00
  • $\begingroup$ @PeterLeFanuLumsdaine You are correct, I had a small brainfart $\endgroup$
    – Holo
    Mar 19 at 17:39


Your Answer

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