I have seen some systems where propositional logic can be written by a single axiom plus an inference rule such as Nicod's axiom.
This to me seems like two rewrite rules. If Nicod's axiom is $N(a,b,c,d)$ then any statements $a\land b\land c\land d \land e$ can be replaced by $N(a,b,c,d) \land e$ which could be written in terms of NANDs. And modus ponens which says $(a ⊼ (b ⊼ c))\land a$ can be replaced by $b$. Actually there are probably a few hidden implied rewrite rules here too for example $a \land a $ replacing $a$ and $a \land (b \land c)$ replacing $(a \land b) \land c$.
Can propositional calculus be defined using a single rewrite rule?
Further if we have a single binary operator $(|)$ and an atomic unit could we encode propositional calculus in terms of propositions encoded like:
$$( ( (|)| (|))|(|))$$
And then use a single rewrite rule which encode both the single axiom the inference rule in one? i.e. essentially it would be to encode every propositional statement in terms of binary trees and the axiom/inference rule as a rewrite/substitution rule on the trees.
Is this possible?
Edit: Thinking about it. I think this would be impossible seeing as one rewrite rule needs to increase the length of the string while the second needs to decrease it. Hence to get anything interesting we would need at least two rewrite rules. Is this argument correct? So are two rewrite rules possible?
Edit2: Actually this argument is false as a single rule could both increase and decrease the length (see comments)