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}$


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?


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 is1 (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.

1 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.

  • 1
    $\begingroup$ How is it not a tautology if it is equivalent to True? Isn't that what a tautology is? $\endgroup$ – user525966 Aug 26 '18 at 2:42
  • $\begingroup$ @user525966 That's not the definition of a tautology but rather something you can meta-theoretically prove about tautologies (in typical logical systems). I should have been clearer. What I'm saying is that $(p\land(p\to q))\to q$ is not what modus ponens is. Instead what is typically referred to by "modus ponens" is a rule of inference. $\endgroup$ – Derek Elkins left SE Aug 26 '18 at 2:44
  • $\begingroup$ If modus ponens is not a tautology, what is an example of a tautology? $\endgroup$ – saulspatz Aug 26 '18 at 2:45
  • $\begingroup$ @saulspatz $(p\land (p\to q))\to q$ is an example of a tautology (for typical logical systems). Again, what I'm saying is what "modus ponens" refers to is not that formula or any formula. It doesn't refer to something for which asking whether it is or is not a tautology makes sense. What's "useful in practice" is the rule called modus ponens, not this formula which the OP is calling "modus ponens". Except calling it "useful" is a bit misleading. It is simply part of the definition of what a proof is in many common logical systems. $\endgroup$ – Derek Elkins left SE Aug 26 '18 at 2:48
  • 1
    $\begingroup$ @user525966 To be clear, most of the mathematical content of the subject area of logic is meta-theorems. For example, the deduction theorem and the soundness and completeness theorems are meta-theorems. Meta-logic also covers things like "what is the syntax of a formula", "what proofs can we build given these rules", "what can we prove about a given notion of semantics". You can have a formal meta-logic such as Agda or ZFC set theory. However, to talk about those formally requires then a meta-meta-logic and ultimately gets grounded in informal reasoning. $\endgroup$ – Derek Elkins left SE Aug 26 '18 at 3:25

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.

  • $\begingroup$ You may want to separate logical axioms from non-logical axioms. It is the non-logical axioms that we expect to "say something" in the way I believe you mean. A logical axiom, such as $A\to A$, say, we would arguably also expect not to "say something" at least as much as we expect rules not to. Though, if you want to say logical axioms should be viewed as rules, I'd be totally down with that, but it would still warrant being clear. $\endgroup$ – Derek Elkins left SE Aug 26 '18 at 2:51
  • $\begingroup$ For proof systems that have logical axioms, you're right that they are similar to rules of inference in that they don't add new information - and the logical axioms that look like propositional sentences are also tautologies. I was thinking more of deductive systems in which there are no logical axioms. --- Although I don't know that I expect axioms to say something, only that if a rule of inference tried to say something I think we would look at it more like an axiom. There are exceptions to that general principle as well, but they go beyond the level of this kind of answer. $\endgroup$ – Carl Mummert Aug 26 '18 at 3:09

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.