In MU puzzle: https://en.wikipedia.org/wiki/MU_puzzle#The_puzzle, We have "MU" string and 4 rules. Now when compared this to logic the wiki article says "The MI string is akin to a single axiom, and the four transformation rules are akin to rules of inference.".
What confuses me is why are the four transformation rules compared to rules of inference in logic and not to simply axioms? For me I would think that those 4 rules are axioms of that formal system, isn't it?
This may come down to a terminology issue - some authors use "axiom" fairly broadly. My stance, and I believe Hofstadter's as well, is the following:
You want to think of axioms as "starting strings" and inference rules as the things you're allowed to do in order to "deduce" new strings from existing strings.
It's at this point that a very annoying term crops up: "logical axiom". According to the previous paragraph, a logical axiom is really an inference rule that takes in no inputs and tells us that we can always infer a statement of a given form "for free."
At this point I should give an example of how this plays out. If I want to whip up a Hilbert system proof of some formula $Q$ from some formulas $P_1,...,P_n$, the situation is standardly described as follows:
We have a single inference rule, namely modus ponens: from $\varphi$ and $\varphi\rightarrow\psi$ we can infer $\psi$.
We have nine logical axioms (see here).
While the above two bulletpoints apply throughout the entire logical context we're in, in this specific case we also have the sentences $P_1,..., P_n$ as non-logical axioms.
By contrast, I would prefer to describe it as follows:
We have ten inference rules; one of these is binary (= takes in two inputs and spits out a third) while the other nine are nullary (= just declare a single type of sentence "free").
In this specific case, we have axioms $P_1,...,P_n$.
Sequent calculi basically take this stance. These consist of a series of basic rules for inductively determining a set of "valid sequents" (basically: assertions of the form "From $\Gamma$ we may deduce $\varphi$"). So everything we're given "for free" by the system is clearly declared as a rule, as opposed to a sentence, so there's no possible confusion. (Of course, sequent calculi are often in my experience thought of as less intuitive than Hilbert systems.)
The important feature is that in either case we have two pieces to any deduction: the ambient logical apparatus, and the specific hypotheses of the problem. Whether or not we want to distinguish between inference rules and logical axioms in the first category is purely superficial; the point is that in the Hofstadter example, we do have a "starting string" MI which isn't given an interpretation as a purely logical fact, so it makes sense to put it in that second category.
I believe the useful term my logic professor used was axiom schemata. For instance, What Hofstadter calls Axiom 2 says
$Mx\to Mxx$ for all non-empty strings $x$
This is not a formal axiom of the system because $x$ is not a symbol in the system, nor is there a universal quantifier in the system. (Let's assume for the sake of argument that $\to$ was a symbol in the system. I'll return to this point.) It is a placeholder for the infinite number of statements
$MI\to MII$
$MU\to MUU$
$MII\to MIIII$
$MIU\to MIUIU$
...
So it's an axiom expressed in the metalanguage of the system. This really should be formally distinguished from the pure axioms of the system (like $MI$ is), because an infinite number of axioms are obviously harder to work with.
That said, $\to$ isn't actually a symbol in the $MU$-system. What Axiom 2 really says (again, using traditional logic syntax) is
From $\vdash Mx$ to infer $\vdash Mxx$ for all non-empty strings $x$
This is not expressible in the language of the system for a whole new reason: the language has no "awareness" of what its theorems are. I think it's typical and reasonable to say that rules of this sort would be formally distinguished from axioms (which are well-formed formulas that we give special meta-meaning to).
You have a couple of nigh-equivalent ways of formulating the system that will all be equally useful in "solving" the system. You can say, as Wikipedia seems to, that there is one axiom and four rules of inference of the system. Or you can do something more along your lines, which is to add $\to$ to the language, have one axiom and four axiom schemata, and introduce Modus Ponens as your sole rule of inference. The choice is completely stylistic, as long as you're more formal than Hofstadter was on pages 33-35 of the text. ^_^
