Since long ago I've been feeling uneasy about the modus ponens. It's sometimes presented as if it were a sort of discovery or a law of how things are.
I think it simply describes what the sentence structure "If ... then ..." means. It's basically the definition of implication.
How is this treated formally in mathematics? Is "implication" a primitive black box at first and then we assert the modus ponens as an axiom?
Once you know the semantics of implication (if-then sentences), you don't need the modus ponens any more. And learning the modus ponens teaches you all there is to know about the meaning of if-then sentences.
I mean, "modus ponens" and "semantics of implication" cover the exact same thing.
You can specify the semantics of implication with a truth-table. Why do you ever need to deal with modus ponens then?
EDIT: Additional clarification. I think the modus ponens is a superfluous step in most discussions. I think the moment that you prove to yourself, the moment you realize, the moment that it clicks in your head that "If p then q"; and then later on you notice that p is true, you automatically realize that q is true.
Otherwise what does it mean that you truly realized "If p then q"? If this belief cannot work with the p belief to yield q automatically, in what sense do these beliefs really encode their meanings?
By automatical I mean that you don't have to go through another step like
Okay, so whenever I have an if-then sentence and I also have its antecedent among my beliefs, I can apply modus ponens and append the consequent to my list of beliefs. Since I'm in such a situation now, I can do this.
But this would just introduce another meta modus ponens. Because you have the modus ponens rule, which itself has an if then structure on a meta level: If you have such two sentences, you can also have a third. In order to apply it, you need to see that you indeed have two such sentences and realize by meta modus ponens that this situation in conjunction with modus ponens mean that you can indeed apply the rule. This leads to an infinite regress.
I think it's best to stop on the first level already and accept q automatically. Just as you don't appeal to meta modus ponens to actually make modus ponens work (you assume modus ponens automatically kicks in), you could already assume that the "If p then q" sentence works automatically too.