Difference between Logical Axioms and Rules of Inference

Question

What's the difference between Logical Axioms and Rules of Inference? In my understanding, both are ordered pairs of formulas which are used to reach a conclusion through syllogisms.

My questions

1. Can both be formalized in a language?

2. Are both present in Hilbert and in Gentzen Calculi?

3. Are both elements of a theory?

I saw in this post a similar question, but I believe mine to be much more elementary.

Answer 1

It is essentially a matter of point of view.

The idea of logical axioms can be tracked back to Frege's Begriffsschrift (1879). For Frege, logic is a science, in particular, the branch of knowledge that deals with truth. Therefore, it is essential to have a body of laws governing the subject matter, namely, the notion of truth. Those are the things we know as logical axioms.

It seems natural to derive the more complex of these judgments [of pure thought] from simpler ones, not in order to make them more certain, which would be unnecessary in most cases, but in order to make manifest the relations of the judgments to one another. Merely to know the laws is obviously not the same as to know them together with the connections that some have to others. In this way we arrive at a small number of laws in which, if we add those contained in the rules, the content of all the laws is included, albeit in an undeveloped state. (Frege 1879, §13)

It is also important to mention that, for Frege (and Russell), there was no clear difference between logic and mathematics, so the modern practice, exemplified in set theories such as ZFC, of incorporating logical principles as rules of inference and subject-specific mathematical facts as axioms was unthinkable.

Gentzen's Untersuchungen über das logische Schließen (1934/1935) marked the turning point from this early axiomatic to the modern inferential conception of logic. Basically, Gentzen's idea was to develop a notion of formal proof that more closely represents actual mathematical reasoning:

My starting point was this: The formalization of logical deduction especially as it has been developed by Frege, Russell, and Hilbert, is rather far removed from the forms of deduction used in practice in mathematical proofs. Considerable formal advantages are achieved in return. In contrast, I intended first to set up a formal system which comes as close as possible to actual reasoning. The result was a 'calculus of natural deduction'. (Gentzen, 1934/1935)

Indeed, Hilbert-style calculi are not very nice to work with, as formal proofs of simple tautologies in those systems are often based on extremely artificial arguments. It may be worth mentioning that Frege himself did not notice that his six axioms for the propositional calculus are not independent:

1. $A \rightarrow (B \rightarrow A)$
2. $(A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C))$
3. $(A \rightarrow (B \rightarrow C)) \rightarrow (B \rightarrow (A \rightarrow C))$
4. $(A \rightarrow B) \rightarrow (\neg B \rightarrow \neg A)$
5. $\neg \neg A \rightarrow A$
6. $A \rightarrow \neg \neg A$

That is, Axiom 3 can be obtained from modus ponens and Axioms 1 and 2. This result was first established by Łukasicwicz in 1929. Moreover, Axioms 3, 4 and 5 can all be reduced to a single axiom:

$$(\neg B \rightarrow \neg A) \rightarrow (A \rightarrow B)$$

This was also unnoticed by Frege.

Gentzen-syle calculi gives more prominence to rules of inference, which represents the process of reasoning with logical connectives by explaining how they can be obtained (introduction rules) and what we can do with them (elimination rules). Typically, they only rely on few axioms, such as the axiom of reflection:

$$p \in \Gamma \vdash p$$

but even this may be regarded as a rule of inference with no assumptions!

Answer 2

A logical axiom can be considered a rule of inference that happens to have no antecedents.

Any interesting proof system must have at least one axiom and one rule of inference with premises. If it has no axioms then there is no way to begin a proof in the empty theory, and without rules of inference all that could be proven would be the axioms themselves.

Hilbert-style proof systems generally have many axioms and few proper inference rules. By contrast, Gentzen-style calculi (sequent calculus and natural deduction) have a minimal number of axioms and many inference rules.

In both cases, one may express each instance of an axiom and/or inference rule as a string in a particular formal language.

A theory consists of axioms that one adds to the logical axioms that come from the logic. Theories don't contain any proper rules of inference of their own.