Out of curiosity I wanted to translate modus ponens into a logical statement and condense/solve it in some way, and I ended up getting True:
$p \land (p \rightarrow q) \rightarrow q$
$=p \land (\lnot p \lor q) \rightarrow q$
$=\lnot(p \land (\lnot p \lor q)) \lor q$
$=\lnot((p \land \lnot p) \lor (p \land q)) \lor q$
$=\lnot(\text{False} \lor (p \land q)) \lor q$
$=\lnot(p \land q) \lor q$
$=\lnot p \lor \lnot q \lor q$
$=\lnot p \lor \text{True}$
$=\text{True}$
I'm not really sure what to make of this. Is modus ponens a tautology? How is it useful in practice if it's not really saying anything?
Best Answer
In this sense, yes, modus ponens is a tautology. All logic rules that can be stated as sentences of propositional logic are tautologies in the same way.
The use of modus ponens in practice is as a rule of inference, rather than as a tautology. That is, if we already have sentences $P$ and $P \to Q$, the modus ponens rule of inference says we can conclude $Q$.
The fact that the sentence $(P \land Q) \land P \to Q$ is a tautology means that this rule is sound: if $P$ and $P \to Q$ are true, so is $Q$. That justifies the use of the rule.
It also means that we don't expect rule of inference to really 'say something' by adding information of their own. If they did, then we would look at them as axioms, rather than rules of inference. We don't want rules of inference to add new information - just to rephrase or simplify the information we already have, so that we can identify conclusions that are already implicit in our assumptions, even if they are hard to recognize originally.