The sequent calculus for classical logic can be interpreted as a non-substructural (structural?) logic with sets of formulas on both sides of $\vdash$. In this setting the premises are implicitly conjuncted and the conclusion is implicitly disjuncted. The fact that the premises and conclusions are packaged into a set bakes in the rules of contraction and exchange (as Alex Kruckman points out in this comment).
Substructural logics can be thought as either "simpler" or "more complex" than structural logics depending on whether we think of ourselves as taking away structural rules or picking more structured objects as our collections.
- if we use multisets, we might get linear logic as pointed out by Noah Schweber.
- if we use sequences, we might get some kind of linear logic without exchange.
- if we use some kind of tree, we might get bunched logic.
The problem I'm having is: I'm not sure how to talk about all substructural logics in a meaningful way.
Each new structure seems kind of ad hoc. Thinking about less structural logics by removing structural rules, which is more natural, presupposes some kind of stopping point. Beyond that point, further loosening of structural rules would require stepping outside the system, so it's important that we choose wisely. Indeed, Alex Kruckman's comment proposes some additional new ways of organizing well-formed formulas into a collection, indexed sets, ordinal-indexed sets, etc.
Is there a natural stopping point? Is there a natural "least structured"-logic that can be used for making statments about all substructural logics?
Here's the immediate context that led to this question.
In this answer to one of my questions, Alex Kruckman describes substructural logics as a natural choice for a consequence relation that doesn't satisfy the following property:
$$ \Gamma \models \Delta \; \text{holds} \;\;\textit{if and only if} \;\; \mathcal{Q}\; \delta \in \Delta , \text{it holds that}\; \Gamma \models \delta $$
Where $\mathcal{Q}$ is $\textit{there exists}$ or $\textit{for all}$. I made a pretty serious mistake in my original question. I thought that the term generalized consequence relation was used in Humberstone's The Connectives to refer a relation like $\models$ with implicit conjunctions on both sides, but I checked the book just now and that is not the case. (I actually can't find any unambiguous reference for a double-conjunct consequence relation in that book.)
There is some precedent for using a relation like this in model theory, but that relation is defined in terms of the truth-in-a-model relation (also written $\models$) and AFAICT it isn't usually an object of study on its own.
