Why can't we generally replace inference rules with axioms?

712 Views Asked by At

Is there a big difference in having insufficient axioms and insufficient inference rules/proof procedure to have a complete theory?

It seems like in many cases adding a new inference rule or a new axiom has the same effect. For example, consider a language with 2-place connectives $\rightarrow, \land$. The language also has an inference rule $a\rightarrow b,a \Longrightarrow b$.

Now we can add a new axiom schemes: $a\land b \rightarrow a$ and $a \land b\rightarrow b$ for any formula $a,b$. An alternative is to add a new inference rules: $a\land b \Longrightarrow a$ and $a\land b \Longrightarrow b$. In this case I claim the theories are equivalent no matter the axiomatization.

In particular, I would think that in second order logic something prevents us from replacing inference rules with axioms, no matter how many inference rules are defined, since it is stated that second order proof calculus is always insufficient (for certain theories). Otherwise we could always use the same proof calculus and merely add axioms, and thus have a universal proof checking procedure. Why does adding axioms in place of inference rules fail?

1

There are 1 best solutions below

6
On

Axioms, Axiom Schemas, and Rules of Inferences are 3 different things.

An axiom is a piece of data. It is a proposition that is introduced to a logic without proof.

A Rule of Inference (RoI) is a program. It can be thought of as a program to generate a new proposition from existing propositions (enumeration); it can be thought of as a decision procedure to check if a new proposition follows from existing propositions (verification).

An Axiom Schema is an RoI that introduces a countably infinite number of propositions. So the description of an axiom schema as $(A \land B) \to A$ introduces $(X \land X) \to X$, $(x > y \land y > z) \to (x > z)$, etc, all to the theory.

Some logics explicitly have an RoI named "Propositional Substition". This is the rule that if you have a propositional expression proven, any propositional variable can be completely replaced by an arbitrary propositional expression. So for example, if you have proven $(X \to X)$, then you can infer $((A \lor B) \to (A \lor B))$. Jaśkowski made this rule explicit in his logic.

In a logic with Propositional Substition, Axioms and Axiom Schema of the same description induce the same theory. In fact, such logics tend to not even bother with Axiom Schema. In a logic without Propositional Substitution, then Axioms and Axiom Schema of the same description can induce different theories. For example, from the axiom $X \to X$ you could not infer $Y \to Y $ without Propositional Substitution.

Eliminating all RoI (even just those that are not Axiom Schema) would make it impossible to introduce new theorems to the theory, so you would never be able to prove anything except what is explicitly assumed.

In modern logic, a hot question tends to actually be the exact opposite: how can we make it so that user of a logic can introduce new valid RoI? There are a lot of decision procedures that can evaluate propositions and decide their correctness much faster than being restricted to compositions of a few hardcoded RoI, and as formal libraries get larger, this becomes a major bottleneck.