# Is there any finite deductive system for propositional logic which only uses unary rules?

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?

• I don't think this question makes sense if you don't define what constitutes a rule precisely and explicitly. For example, do steps like "from $A \wedge B$ infer $B \wedge A$" constitute acceptable rules? If so, you can just emulate the usual Hilbert system using unary rules. Commented Nov 4, 2020 at 23:40
• Sorry, I missed out the second, more important question from my previous comment: is "from $A$ infer $\phi \wedge A$" where $\phi$ is required to be an instance of either the $K$ or $S$ axioms a valid rule/axiom schema? (presumably you allow "infer $\phi$" as a finite axiom schema) Commented Nov 4, 2020 at 23:52
• Do you consider a set {(x$\rightarrow$y), x} one object? If so, isn't modus ponens a unary rule? Alright, I guess you might formulate this question as asking if there exists a finite deductive system where all rules of inference only have singletons as their premises, assuming that {X} = X, where X is an arbitrary set. Commented Nov 5, 2020 at 15:51
• @Z.A.K. Certainly, but I don't see how that allows for modus ponens to work in general? Commented Nov 5, 2020 at 17:10
• @DougSpoonwood how is a set a premise? The question might have been a bit informal but I don't see your point to be honest. Commented Nov 5, 2020 at 17:11

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:

1. Infer $$\varphi$$.
2. From $$C$$ infer $$\varphi \wedge C$$.
3. From $$C$$ infer $$C \wedge \varphi \wedge \varphi$$.

Modus ponens rules

1. From $$C \wedge D \wedge (A \wedge (A \rightarrow B) \wedge E)$$ infer $$C \wedge D \wedge (A \wedge (A \rightarrow B) \wedge B \wedge E)$$.
2. From $$C \wedge D \wedge ((A \rightarrow B) \wedge A \wedge E)$$ infer $$C \wedge D \wedge ((A \rightarrow B) \wedge A \wedge B \wedge E)$$.

Shunting rules

1. From $$(A \wedge C) \wedge D \wedge E$$ infer $$C \wedge (A \wedge D) \wedge E$$.
2. From $$(A \wedge C) \wedge D \wedge E$$ infer $$C \wedge D \wedge (A \wedge E)$$.
3. From $$C \wedge (A \wedge D) \wedge E$$ infer $$(A \wedge C) \wedge D \wedge E$$.
4. From $$C \wedge D \wedge (A \wedge E)$$ infer $$(A \wedge C) \wedge D \wedge E$$.

Conjunction elimination

1. From $$A \wedge B$$ infer $$A$$.

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.

Lemma. Given a derivation of length $$n$$,

• {1) $$Q_1$$
• (2) $$Q_2$$
• (3) $$\dots$$
• (n) $$Q_n$$

in the Hilbert calculus, we can find a derivation of $$Q_n \wedge \dots \wedge Q_2 \wedge Q_1$$ in our system.

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:

1. Have $$Q_n \wedge \dots \wedge Q_1$$ by induction hypothesis.
2. Infer $$(Q_n \wedge \dots \wedge Q_1) \wedge \varphi \wedge \varphi$$ using the third axiom rule.
3. Infer $$(Q_k \wedge \dots \wedge Q_1) \wedge (Q_{k+1} \wedge \dots \wedge Q_n \wedge \varphi) \wedge \varphi$$ by using the first shunting rule repeatedly.
4. Infer $$(Q_{k-1} \wedge \dots \wedge Q_1) \wedge (Q_{k+1} \wedge \dots \wedge Q_n \wedge \varphi) \wedge (Q_k \wedge \varphi)$$ by using the second shunting rule.
5. Infer $$(Q_\ell \wedge \dots \wedge Q_1) \wedge (Q_{\ell + 1} \wedge \dots \wedge Q_{k-1} \wedge Q_{k+1} \wedge \dots \wedge Q_n \wedge \varphi) \wedge (Q_k \wedge \varphi)$$ by using the first shunting rule repeatedly.
6. Infer $$(Q_{\ell-1} \wedge \dots \wedge Q_1) \wedge (Q_{\ell + 1} \wedge \dots \wedge Q_{k-1} \wedge Q_{k+1} \wedge \dots \wedge Q_n \wedge \varphi) \wedge (Q_\ell \wedge Q_k \wedge \varphi)$$ using the second shunting rule.
7. Infer $$(Q_{\ell-1} \wedge \dots \wedge Q_1) \wedge (Q_{\ell + 1} \wedge \dots \wedge Q_{k-1} \wedge Q_{k+1} \wedge \dots \wedge Q_n \wedge \varphi) \wedge (Q_\ell \wedge Q_k \wedge Q_{n+1} \wedge \varphi)$$ using the relevant modus ponens rule.
8. Infer $$(Q_{\ell} \wedge \dots \wedge Q_1) \wedge (Q_{\ell + 1} \wedge \dots \wedge Q_{k-1} \wedge Q_{k+1} \wedge \dots \wedge Q_n \wedge \varphi) \wedge (Q_k \wedge Q_{n+1} \wedge \varphi)$$ using the fourth shunting rule.
9. Infer $$(Q_{k-1} \wedge \dots \wedge Q_1) \wedge (Q_{k+1} \wedge \dots \wedge Q_n \wedge \varphi) \wedge (Q_k \wedge Q_{n+1} \wedge \varphi)$$ using the third shunting rule repeatedly.
10. Infer $$(Q_{k} \wedge \dots \wedge Q_1) \wedge (Q_{k+1} \wedge \dots \wedge Q_n \wedge \varphi) \wedge (Q_{n+1} \wedge \varphi)$$ using the fourth shunting rule.
11. Infer $$(Q_{n} \wedge \dots \wedge Q_1) \wedge \varphi \wedge (Q_{n+1} \wedge \varphi)$$ using the third shunting rule repeatedly.
12. Infer $$(Q_{n+1} \wedge \dots \wedge Q_1) \wedge \varphi \wedge \varphi$$ using the fourth shunting rule.
13. Infer $$Q_{n+1} \wedge \dots \wedge Q_1$$ using conjunction elimination.

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.

If equivalence rules are allowed, then yes.

You could have one inference rule that infers a tautology from nothing (e.g. Law of Exclude middle: $$\vdash \phi \lor \neg \phi$$), and other than that use equivalence rules as inference rules. Since we know that a relatively small set of equivalence rules can transform any statement into any equivalent statement, that starting tautology can be transformed into any other tautology.

• A relatively small (finite) set of identities can transform any statement into any equivalent statement. Can a finite set of equivalence inference rules do the same thing? That's not obvious to me. E.g. the inference rule "from $A \vee B$ get $B \vee A$" can't really help you infer $(B \vee A) \wedge C$ from $(A \vee B) \wedge C$: the rule does not apply, since $(A \vee B) \wedge C$ is not a substitution instance of $A \vee B$. You need either a "deep inference" system (where rules can apply to _sub_formulas), or auxiliary inferences (which normally require binary rules). Commented Nov 6, 2020 at 3:49
• @Z.A.K. Exactly! So, as you say in the comments, it depends on how you define what is seen as a rule. Commented Nov 6, 2020 at 21:04