Are axioms and rules of inference interchangeable?

Question

There is an equivalence between cellular automata and formal systems, you can code one into the other and vice versa. But in the the cellular automata (CA) the rules of inference are fixed and are pretty simple (for instance, the universal two neighbor, two state rule 110). So all the rules of the formal system that is coded into a rule 110 CA (also a formal system) must be coded mostly in the input. And vice versa, if you have a formal system resembling rule 110, you can code your axioms into inference rules in a different formal system.

Is this correct? Do this exchangeability between axioms and rules have any meaning for the foundations of logic and/or mathematics?

Answer 1

Cellular automata are considered a subset of the formal systems, so, what you say about axioms and rules being relative is correct. I actually remember reading something about that a long time ago in a book about automatic theorem proving, but I cant remember the details. Regarding the philosophical meaning of this, my view is that it only shows how many options you have when choosing a formal system to code your model of interest.

Answer 2

In axiomatic and natural deduction proof systems, axiom schemata and inference rules are interchangeable, for the most part. In a system with modus ponens and a conditional $\to$, for instance, any inference rule of the form $$\Lambda\,/\,\Gamma$$ could be replaced by the axiom schema $$\Lambda \to \Gamma$$ In the first case, if you have $\Lambda$, then by the inference rule, you may infer $\Gamma$. In the second case, if you have $\Lambda$, then instantiate the axiom schema to yield $\Lambda \to \Gamma$ and use modus ponens to infer $\Gamma$. I think that shows how inference rules can be replaced by axiom schemata (as long as you have modus ponens or an equivalent).

Replacing axiom schemata by inference rules is a little bit easier, though it may feel like a bit of hack. If you have the axiom schema $$\Lambda$$ just replace it by an inference rule with no preconditions $$/\,\Lambda$$

This approach should work regardless of the particulars of your axiom schemata and inference rules, since checking whether a step in a derivation is a valid application of an inference rule based on some set of premises should not be any more or less difficult than checking whether a formula is an instance of an axiom schema.