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.


Essentially, both correspond to two different historical approaches of logic:

In Frege's Begriffsschrift (1879), for example, logic is thought as a science, that is, a body of laws governing the notion of truth. Therefore, what is important for him is to highlight the fundamental principles of thought and put them together, as the fundamental bricks on which this science can be erected. In §13 he writes:

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.

Therefore, it is natural for him to conceive logic in the axiomatic approach: the axioms are the logical laws that rule the ideal thought. This is more or less the approach of Russell as well.

In fact, the turning point from this scientific approach to the conception of logic as we know it is due to Gentzen's paper Untersuchungen über das logische Schließen (1934/1935). Basically, his idea was to develop a notion of formal proof that comes closer to 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)

The point is that the axiomatic approach is not very nice to work with, rather, the proofs in it can get very artificial. To give an illustration, 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$

In the sense that the Axiom 3 can be obtained as a theorem from his rules of inference and the Axioms 1 and 2. This result was only 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. Should we argue then that he was bad at axiomatic proofs? I do not think so. However, this suggests that human reasoning is not based on laws but rules. In this sense, rules of inference correspond to the formalization of the process of reasoning and the logical connectives get their meaning from the way they are used, e.g. the conjunction introduction rule "from $\vdash A$ and $\vdash B$, obtain $\vdash A \land B$".


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.

  • $\begingroup$ Are there any inference rules which cannot be conceived as axioms? $\endgroup$ – Bruno Schiavo Jun 10 '15 at 3:52
  • 1
    $\begingroup$ "Hilbert-style proof systems generally have many axioms and few proper inference rules" I don't know how you're getting this. It is not all that hard to prove that so long as we allowable countably infinite variables, that there exist a countable infinity of single-axiom systems for plenty of propositional calculi. A countably infinite sequence of single axioms for the implicational propositional calculus is (CCCpqrCCrpCsp, Cp$_1$CCCpqrCCrpCsp, Cp$_2$Cp$_1$CCCpqrCCrpCsp, ...) $\endgroup$ – Doug Spoonwood Jun 10 '15 at 5:21
  • 1
    $\begingroup$ Perhaps the intended wording is "many axiom schemata", instead of "many axioms"? $\endgroup$ – Ioannis Filippidis Nov 14 '16 at 7:12

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.