>>5055963
The modus tollens rule may be written in sequent notation:
P
→
Q
,
¬
Q
⊢
¬
P
P\to Q,\neg Q\vdash \neg P
where
⊢
\vdash is a metalogical symbol meaning that
¬
P
\neg P is a syntactic consequence of
P
→
Q
P\to Q and
¬
Q
\neg Q in some logical system;
or as the statement of a functional tautology or theorem of propositional logic:
(
(
P
→
Q
)
∧
¬
Q
)
→
¬
P
{\displaystyle ((P\to Q)\land \neg Q)\to \neg P}
where
P
P and
Q
Q are propositions expressed in some formal system;
or including assumptions:
Γ
⊢
P
→
Q
Γ
⊢
¬
Q
Γ
⊢
¬
P
{\frac {\Gamma \vdash P\to Q~~~\Gamma \vdash \neg Q}{\Gamma \vdash \neg P}}
though since the rule does not change the set of assumptions, this is not strictly necessary.
More complex rewritings involving modus tollens are often seen, for instance in set theory:
P
⊆
Q
P\subseteq Q
x
∉
Q
x\notin Q
∴
x
∉
P
\therefore x\notin P
("P is a subset of Q. x is not in Q. Therefore, x is not in P.")
Also in first-order predicate logic:
∀
x
:
P
(
x
)
→
Q
(
x
)
\forall x:~P(x)\to Q(x)
∃
x
:
¬
Q
(
x
)
\exists x:~\neg Q(x)
∴
∃
x
:
¬
P
(
x
)
\therefore \exists x:~\neg P(x)
("For all x if x is P then x is Q. There exists some x that is not Q. Therefore, there exists some x that is not P.")
Strictly speaking these are not instances of modus tollens, but they may be derived from modus tollens using a few extra steps.