Unique set of inference rules for a deductive system?

Question

I have the impression that for a deduction system there are many sets of inference rules to describe it. Simple example, the inference rules for (classical or intuitionistic, this is not the matter) propositional $\wedge,\to$ logic are widely known. But aren't there other sets of inference rules with which we could prove exactly the same formulas as with the established inference rules?

This impression comes from the fact that for a theory $T$ there are countably many sets of axioms. But each axiom can be translated into an inference rule. So, if there are many sets of axioms, aren't there also many sets of rules?

Answer 1

There are different systems with different sets of inference rules that prove exactly the same formulas.

Just to give an example: For first-order logic, there are Hilbert-style deduction systems which have only three rules (modus ponens and one for each quantifier) and an infinite axiom set (axiom schemes for each formula). On the other hand, there are "natural" deduction systems without any axioms but with a bigger number of rules. Furthermore, in systems of number theory, you have the choice between using an axiom scheme for induction and defining a rule for it. So there is always a trade-off between the size of the axiom set and the number of rules.

Most important, both systems, i.e. Hilbert-style and natural deduction, have been proven to be equivalent and complete.

A simple example of how to replace the rule of conjunction introduction, now in a sequent calculus, could be to replace

$${ \Delta \vdash A,\Gamma \qquad \Delta \vdash B,\Gamma \over \Delta \vdash A \land B,\Gamma}\ \mathrm{andRight} $$

with the rule

$${\Delta \vdash \neg(\neg A \lor \neg B), \Gamma \over \Delta \vdash A\land B,\Gamma}\ \mathrm{elimAndRight}$$

which is of course classically valid (need to check whether this is still complete, but basically this is just a way of eliminating conjunctions which should work in my opinion). Possibly one could also delete the rule and add a new set of axiom schemes to the system to keep completeness.

Answer 2

Hardly. For eyample if you wanted to replace Conjunction introduction $$ A,B\vdash A\land B$$ with other rules, you'd need some rule $A,B\vdash ???$ and some rule $A,B,???\vdash A\land B$. What should these rules be (without introducing falsehood)?