Should Modus Ponens and Modus Tollens be viewed as implications? I ask because of the following. It seems that Modus Ponens can be written as $\left(P\rightarrow Q\right)\land P\rightarrow Q$ And Modus Tollens can be written as $\left(P\rightarrow Q\right)\land\lnot Q\rightarrow\lnot P$
-
3Both Modus Ponens and Modus Tollens are technically not implications, bur rather sequents, and are written with a metalogic symbol $\vdash$. E.g; Modus tollens, in its most formal form is written ${P, P\to Q}\vdash {Q}$ (but the curly brackets are usually dropped for brevity). However, you can think of $\vdash$ as a kind of implication which reads as "If everything on the left (of the symbol) is true, then at least something on the right is true". – Graviton Apr 27 '23 at 05:26
-
1@Graviton, you forgot to consider this part of the linked article: The assertion symbol in sequents originally meant exactly the same as the implication operator...n 1934, Gentzen did not define the assertion symbol ' ⊢ ' in a sequent to signify provability. He defined it to mean exactly the same as the implication operator ' ⇒ '...In 1939, Hilbert and Bernays stated likewise that a sequent has the same meaning as the corresponding implication formula. – Apr 27 '23 at 05:38
-
1that's a good point, and it should be mentioned. In my expanded answer that can be realized by the deduction theorem. However, from a purely technical point, if you've ever played around with proof verification software, for example, you'll know that implications and assertions necessarily represent different data structures. – Graviton Apr 27 '23 at 05:44
1 Answers
I should really put my comment as an answer:
Inference rules, like Modus Ponens and Modul Tollens, etc, are not implications in the traditional sense, but sequents, also called assertions.
A sequent is of the form $$\{A_1,\dots, A_m\}\vdash \{B_1,\dots,B_n\}$$ where $\{A_1,\dots, A_m\}$ is the sequence of antecedents and $\{B_1,\dots,B_n\}$ is the sequence of consequents. Whether these are considered sets vs. sequences are a matter of debate amongst logicians (that is to say, it depends on if the order of antecedents and consequents matters to you). Usually the curly brackets are dropped for brevity.
But in any case, a sequent is understood as a transformation rule which reads as
If all the antecedents are true, then at least one of the consequents are true.
In the case of Modus Ponens and Modus Tollens, there is only one consequent, thus they are specifically simple conditional assertions.
Thus, Modus Ponens can be denoted as $$P,P\to Q\vdash Q,$$ and Modus Tollens can be denoted as $$P\to Q,\neg Q \vdash \neg P.$$
However, by the deduction theorem, we can realize $$(P,P\to Q\vdash Q)\iff \vdash (P\wedge (P\to Q))\to Q.$$
I.e; $\vdash (P\wedge (P\to Q))\to Q$ is an equivalent formulation, in which the initial $\vdash$ is often dropped for brevity; hence you can intepret the sequent only in terms of logical operators.
- 4,462