Why are inference rules necessary?

Question

It has been stated, both on this site and elsewhere, that without inference rules, a theory can only prove its own axioms.

I don't understand how, though, and will try to show derivation without inference rules:

Axioms:

1. $P = P$

2. $\neg(P \land \neg P)$

3. Cows are fat

I will denote the axiom Cows are fat as $Q$.

Now, through the interplay of 1., 2. and 3., I derive this theorem:

$$[(P = P ) \land (\neg(P \land \neg P) ) \land (\text{ Cows are fat} = Q) ]\implies ( \neg\neg Q = \text{It is not the case that cows are not fat})$$

One could say this is using the following inference rule:

$$\text{Sps.} \\ P = P \\ \neg(P \land \neg P) \\ P \\ \therefore \neg \neg P $$

But if one must call this logical interplay of axioms an inference rule, then one is robbing the axioms of their meaning. If inference rules are required, then $\neg(P \land \neg P)$ does not mean something cannot be true and false at the same time. If it did mean that, it would be sufficient. Since the axiom is not sufficient to prove anything beyond itself, then that means you can assert it, yet the possibility that something is true and false at the same time remains. That robs it of its meaning, because asserting it does not remove the possibility of its negation being true.

If you want to describe and name the ways of interplay between axioms as inference rules, that is fine, but to say they are necessary to prove theorems is like saying that describing/naming the sky is necessary for it to exist.

Answer 1

Yes and no.

Yes, you don't need inference rules to show that some statement is a logical consequence of others, because we can use semantics to do so. And this is some of what you are doing when you talk about the 'interplay' of the statements involved.

But in the context of logic, when we talk about 'proofs' or 'derivations', we typically mean formal proofs and derivations, i.e. through the syntactical manipulation of formulas. And yes, the inference rules we use to do so can be seen as 'mere' descriptions of logical consequences that are already the case on basis of the semantics, but in the context of a 'proof system' we are almost invariably referring to a syntactical proof, i.e. something that uses inference rules. Indeed, the 'axioms' of a 'theory' are already syntactical objects, so in that sense what you were really doing in your post was a bit of weird mix between syntax and semantics.

In sum, I think you will find it informative to read about the difference between formal semantics and formal proofs.