I'm not sure if this has ever been proven/disproven, but, assuming the usual grammar of propositional logic, is there any deductive system which derives exactly the tautologies of classical logic while only using finitely many unary rules and axiom schemes? This would of course be equivalent to proving a similar statement for usual kinds of intutionistic, minimal or even subminimal logic.
By a unary rule, I mean two propositional formulas (premise and conclusion) built from variables and the usual connectives.
A concept of substitution needs to be implicitly assumed, as well as syntactic rules. The restriction to unary rules explicitly forbids the use of binary rules like modus ponens or usual conjunction introduction, as their premises consist both of an implication and its antecedent.
I don't think such a system exists, simply because I cannot think of any real "pattern" in true implications which would apply in such a case. Has any similar statement been proven or is there some reasonably difficult approach to such questions?
There exists a deductive system which derives exactly the tautologies of classical propositional logic while using finitely many at-most-unary rules and axiom schemata.
We will restrict our attention to classical propositional logic given by the two connectives $\neg, \rightarrow$, where other connectives are defined as abbreviations, as customary in Hilbert-style calculi (besides, a nigh-identical strategy would work even if we gave the other connectives explicitly). We abbreviate $\neg (A \rightarrow \neg B)$ as $A \wedge B$. For parenthesis-management we write $\wedge$ and $\rightarrow$ as right-associative, so that $A \wedge B \wedge C$ denotes $A \wedge (B \wedge C)$, while $A \rightarrow B \rightarrow C$ denotes $A \rightarrow (B \rightarrow C)$.
Consider the deductive system (called "our system" from here on) that has the following (nullary and unary) rules of inference.
Axiom rules
We call a formula a logical axiom if it occurs as a substitution instance of one of the following: $P \rightarrow (Q \rightarrow P), (P \rightarrow Q \rightarrow R) \rightarrow (P \rightarrow Q) \rightarrow P \rightarrow R, (\neg Q \rightarrow \neg P) \rightarrow P \rightarrow Q$. Let $\varphi$ denote a logical axiom. We admit the following inference rules:
Modus ponens rules
Shunting rules
Conjunction elimination
Our system clearly satisfies soundness for propositional classical logic. It also satisfies completeness: we prove this by reducing the completeness of our system to that of Hilbert's proof calculus.
Proof. By induction on the length of the Hilbert calculus derivation $\delta$. If the derivation has length 1, then $Q_1$ is a substitution instance of an axiom $\varphi$, so we can use the first axiom rule of our system to prove $Q_1$. From here on assume that the derivation has length $n+1$. By induction hypothesis, our system has a derivation of $Q_n \wedge \dots \wedge Q_1$. We have two cases to consider.
Case 1: The last rule of the derivation $\delta$ is an axiom rule of the Hilbert system. In this case $Q_{n+1}$ is a substitution instance of an axiom, and from $Q_n \wedge \dots \wedge Q_1$ we can infer $Q_{n+1} \wedge Q_n \wedge \dots \wedge Q_1$ using the second axiom rule of our system.
Case 2: The last rule of the derivation $\delta$ is a modus ponens rule of the Hilbert system, inferring $Q_{n+1}$ from $Q_k$ and $Q_\ell$ (w.lo.g. assume $k > \ell > 1$). Take your favorite axiom $\varphi$, then argue in our system as follows:
Qed.
As a corollary, we get completeness for our system.
Proof. Take a classical tautology $P$. By completeness for the Hilbert calculus, we can find a derivation $\delta$ of $P$ in the Hilbert calculus. By our previous lemma, we can find a derivation of $P \wedge Q_n \wedge \dots \wedge Q_1$ for some $n \in \mathbb{N}$ in our system. Using conjunction elimination, we can infer $P$ in our system. Qed.