Is modus ponens a tautology?

Question

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?

Answer 1

Modus ponens isn't that formula or any formula (and thus not a tautology), it's a rule. A rule tells you one way of building a proof. In fact, rules are part of the definition of what a proof is¹ (for a given logical system). For this specific case, it sounds like this: "One way of building a proof of $Q$ is to combine a proof of $P$ and a proof of $P\to Q$ and label that combination "modus ponens". So "modus ponens" is operating at the meta-logical level. It is part of the definition of the logical framework, and specifically part of the definition of proof. (Other logical frameworks may or may not have modus ponens as a rule.)

In more program-y terms, a proof is a data structure and a rule is one of the ways of building a value of that data structure. This is literally how such a thing is represented in many mechanized proof systems when we study logics within them. For example, as demonstrated in Agda for a basic logical framework here where modus ponens literally is a data constructor (H-IM) of a data type.

¹ You can have "derived rules" which can just be thought of as abbreviations of using several "primitive" rules. These derived rules are not part of the definition of a proof. In some presentations of logics, modus ponens might be a derived rule rather than a primitive rule.

Answer 2

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.