Logical Axioms and Rules of Inference

Question

In A Tour Through Mathematical Logic, Wolf mentions that

These [logical axioms] usually include some or all tautologies, the usual equality axioms, and some simple laws involving quantifiers.

Question: Why are tautologies included as axioms? Axioms are something which we adopt to be true. But aren’t tautologies defined to be things that are true?

He then mentions that a first-order theory also includes rules of inference.

Question: Rules of inferences are based on logical consequences, which are nothing but tautologies. So why include then separately?

Answer 1

This is the author's way of saying something like:

You probably already know one or more proof system that will allow you to write down proofs of all the propositional tautologies. For our purposes here we don't really need to care how the part of our systems that deals with propositional reasoning works -- as long as its effects is the usual classical propositional logic. Please feel free to imagine that we're talking about a system that includes your favorite way of writing down propositional reasoning.

Since the quote just says that the rules include some or all tautologies, it's not an attempt to define anything, but merely to remind you what the basic shape of the favorite logical system you're going to choose is.

And it's certainly true that many proof system do include some tautologies. For example, Hilbert systems generally include (among others) these as logical axioms: $$ A\to(B\to A) \qquad\qquad (A\to B)\to(A\to(B\to C))\to(A\to C) $$ These are definitely tautologies, and they combine with each other and rules of inference to allow you to prove additional tautologies.

---

For the difference between axioms and rules of inference I'll recommend this answer by Peter Smith.

Answer 2

Except in some degenerate cases, all proof systems contain rules of inference. They are what allow you to derive new theorems from old theorems. That is, even a proof system for classical propositional logic will include rules of inference. The most commonly available one is Modus Ponens.

Tautologies are definitely not things that are true by definition. The typical definition of "tautology" is: a formula of propositional logic is a tautology if and only if, when interpreted as a Boolean function, it is the constantly $1$ function. The set of tautologies is just a set of formulas. This subset of formulas is computable using the normal truth table approach.

A theorem is a formula that can be derived in our proof system. An axiom is a formula that is taken to be a theorem by fiat.

At no point in the above do I talk about "adopting" things as "true".

As Henning Makholm states, the point is to include all (substitution instances of) formulas provable in classical propositional logic as provable within classical first-order logic. However, first-order logic has additional formulas beyond propositional ones which would not be tautologies even if they were provable within classical first-order logic.

A proof system is like an unending jigsaw puzzle. Axioms are like the pieces of the puzzle. Rules of inference tell you when you're allowed to add a puzzle piece to an existing picture. Theorems are any of the pictures you can make. You can choose the axioms and rules of inference however you like (though usually we want to at least restrict things so that we can mechanically check if the rules are followed). There is absolutely no a priori reason this should have anything to do with reasoning.

While our definitions of proof systems and semantics for logics are usually motivated by informal reasoning, they are not defined by it.¹ If it turns out informal reasoning works in a way incompatible with what classical first-order logic suggests, say, then that just means classical first-order logic is not a good model for informal reasoning and perhaps another logic would be a better model, not that the definition of classical first-order logic changes to come in line with our informal reasoning.

You are going to be a lot more confused and have a lot of unnecessary difficulty if you don't separate informal reasoning from formal logic. Conflating the two leads to simple questions like whether $A\to B$ is equivalent to $\neg A\lor B$ in classical propositional logic becoming potential philosophical crises. I'm not saying you can't think about the philosophical consequences of such an equivalence holding for informal reasoning, but you can have your philosophical crisis and do your homework too since the question doesn't depend on the resolution to that philosophical question but on the definition of classical propositional logic.

¹ At least not directly, and no more than anything else is. We obviously need to use our informal reasoning somewhere to think about anything. The relationship for logic is no different than for, say, group theory or topology.