When I asked whether the empty logic (the one on which no argument is valid) is axiomatizable, the consensus was that it is, and that it is axiomatized by a proof system having no rules whatsoever.
Is this in fact a proof system? If a proof system is determined by its rules, then what is a rule, exactly?
The answer here characterizes a derivation in some system as a legally-labelled (well-founded) tree, where the rules of the proof system determine the legality of labellings.
It seems to me that the rules of a Hilbert system correspond to logics: the rules that allow leaves to be labelled with axioms correspond to logics for each axiom schemata $\alpha$ which validate just substitution instances of $\vdash \alpha$ while the rule for non-leaves (i.e., modus ponens) corresponds to the logic which validates just substitution instances of $\varphi \to \psi, \varphi \vdash \psi$. Perhaps the "rule" (not standardly described as such) that one may also label a leaf node with any premise corresponds to the logic validating just the arguments $\vdash \gamma$ where $\gamma$ is a premise (but not necessarily any substitution instance thereof).
This line of thinking applies just as well to, e.g., Gentzen calculi by moving from formulas and arguments to sequents and sequent arguments.
If this is right, can we then see the logic axiomatized by a proof system as being generated somehow by the logics corresponding to its rules? Can we avoid circularity here? Maybe the system with no rules is a sort of base case, the bottom element of a lattice of proof systems?