I noticed a little symmetry recently and I’m not sure how to explain it yet. The symmetry is between intuitionistic and classical logic. In the Gentzen presentation for classical logic, you have \Gamma => \Delta, where \Delta and \Gamma are multisets. The inference rules for classical and intuitionstic logic are the same with one exception. The rules of intuitionistic logic restrict \Delta to singleton sets. So, proof theoretically (in Gentzen) we have (potentially) several formulas in conclusions for classical logic and only one in intuitionistic logic. Switch gears to semantics. Suppose we have a Kripke tree (W, ≤) for intuitionistic logic. This gives the semantics for intuitionistic logic. Restrict the set of worlds W to a singleton and it becomes classical semantics. So, semantically (in Kripke) we have several worlds for intuitionistic logic and only one world for classical. (You get the same thing if ≤ is an equivalence relation, but this just makes W behave as if it had only one world.)

Why would this be? In proof theory, allowing multiple conclusions lets you move formulas back and forth at will from antecedent to consequent, e.g. p=>p,\bot goes to =>p, ~p which goes to =>pv~p. Restricting to one conclusion means you can’t derive the law of excluded middle for arbitrary formulas like that, since the first step is blocked. In the semantics, you get ~p only if all the worlds ≤ the world of evaluation do not verify p. This means that you can have a world w that doesn’t verify p but also doesn’t verify ~p since some w’≥w does verify p. Restricting to one world eliminates this wiggle room, since there will not be any such w’≥w if w is the only world. If w verifies p, then p. If w doesn’t verify p, then ~p. Classical. Why there should be any sort of symmetry I don’t know.