Deducción natural/Reglas derivadas

Nombre de la regla	Abreviación	Formalización	Cálculo de secuentes
Ex falso sequitur quodlibet Principio de explosión Ex contradictione sequitur quodlibet	$EFQ$	${\begin{matrix}\neg p\\\hline p\to q\end{matrix}}$	$\neg p\to p\to q$
	$ECQ$	${\begin{matrix}p\land \neg p\\\hline q\end{matrix}}\qquad {\begin{matrix}p\leftrightarrow \neg p\\\hline q\end{matrix}}$	$p\land \neg p\to q$ $(p\leftrightarrow \neg p)\to q$
De Morgan	$DM$	${\begin{matrix}{\underline {\neg (p\land q)}}\\{\overline {\neg p\lor \neg q}}\end{matrix}}\qquad {\begin{matrix}{\underline {\neg (p\lor q)}}\\{\overline {\neg p\land \neg q}}\end{matrix}}$	$\neg (p\land q)\leftrightarrow \neg p\lor \neg q$ $\neg (p\lor q)\leftrightarrow \neg p\land \neg q$
		${\begin{matrix}{\underline {\quad \;p\land q\;\quad }}\\{\overline {\neg (\neg p\lor \neg q)}}\end{matrix}}\qquad {\begin{matrix}{\underline {\quad \;p\lor q\;\quad }}\\{\overline {\neg (\neg p\land \neg q)}}\end{matrix}}$	$p\land q\leftrightarrow \neg (\neg p\lor \neg q)$ $p\lor q\leftrightarrow \neg (\neg p\land \neg q)$
Silogismo disyuntivo Inferencia de la alternativa Modus tollendo ponens	$SD$	${\begin{matrix}p\lor q\\\neg p\\\hline q\end{matrix}}\qquad {\begin{matrix}p\lor q\\\neg q\\\hline p\end{matrix}}$	$(p\lor q)\land \neg p\to q$ $(p\lor q)\land \neg q\to p$
		${\begin{matrix}\neg p\lor q\\p\\\hline q\end{matrix}}\qquad {\begin{matrix}p\lor \neg q\\q\\\hline p\end{matrix}}$	$(\neg p\lor q)\land p\to q$ $(p\lor \neg q)\land q\to p$
Carga de premisa	$CP$	${\begin{matrix}p\\\hline q\to p\end{matrix}}\qquad {\begin{matrix}q\\\hline p\to q\end{matrix}}$	$p\to q\to p$ $q\to p\to q$
Identidad Repetición	$Id$	${\begin{matrix}{\underline {\quad p\quad }}\\{\overline {\quad p\quad }}\end{matrix}}\qquad {\begin{matrix}{\underline {\quad q\quad }}\\{\overline {\quad q\quad }}\end{matrix}}$	$p\leftrightarrow p$ $q\leftrightarrow q$
Definición del condicional Implicación material	$Df\to$	${\begin{matrix}{\underline {\;p\to q\;}}\\{\overline {\;\neg p\lor q\;}}\end{matrix}}\qquad {\begin{matrix}{\underline {\quad p\to q\quad }}\\{\overline {\;\neg (p\land \neg q)\;}}\end{matrix}}$	$p\to q\leftrightarrow \neg p\lor q$ $p\to q\leftrightarrow \neg (p\land \neg q)$
Contraposición Transposición	$Tp$	${\begin{matrix}{\underline {\,\quad p\to q\quad \,}}\\{\overline {\,\;\neg q\to \neg p\;\,}}\end{matrix}}\qquad {\begin{matrix}{\underline {\,\quad q\to p\quad \,}}\\{\overline {\,\;\neg p\to \neg q\;\,}}\end{matrix}}$	$p\to q\leftrightarrow \neg q\to \neg p$ $q\to p\leftrightarrow \neg p\to \neg q$
Silogismo hipotético Transición del condicional	$SH$	${\begin{matrix}p\to q\\q\to r\\\hline p\to r\end{matrix}}$	$(p\to q)\land (q\to r)\to p\to r$
Distribución de la conjunción	$DC$	${\begin{matrix}{\underline {\,\;p\land (q\lor r)\;\,}}\\{\overline {p\land q\lor p\land r}}\end{matrix}}$	$p\land (q\lor r)\leftrightarrow p\land q\lor p\land r$
Distribución de la disyunción	$DD$	${\begin{matrix}{\underline {\quad \,p\lor (q\land r)\,\quad }}\\{\overline {(p\lor q)\land (p\lor r)}}\end{matrix}}$	$p\lor (q\land r)\leftrightarrow (p\lor q)\land (p\lor r)$