Deducción natural/Reglas de introducción

Conectiva	Nombre de la regla	Abreviación	Formalización	Cálculo de secuentes
$\neg \,$	Introducción de la negación Reducción al absurdo	$I\neg \,$	${\begin{array}{l}{\begin{array}{|l|}\hline \quad p\quad \\q\land \neg q\\\hline \end{array}}\\\quad \neg p\end{array}}$ $Supuesto$ $\quad$	$(p\to q\land \neg q)\to \neg p$ $p\land q\land \neg q\to \neg p$ $(p\to q)\land (p\to \neg q)\to \neg p$ $(p\land q)\land p\land \neg q\to \neg p$
$\land \,$	Introducción de la conjunción	$I\land \,$	${\begin{matrix}p\\{\underline {\quad q\quad }}\\{\overline {\;p\land q\;}}\end{matrix}}\qquad {\begin{matrix}p\\{\underline {\quad q\quad }}\\{\overline {\;q\land p\;}}\end{matrix}}$	$p\land q\leftrightarrow p\land q$ $p\land q\leftrightarrow q\land p$
$\lor \,$	Introducción de la disyunción	$I\lor \,$	${\begin{matrix}p\\\hline p\lor q\end{matrix}}\qquad {\begin{matrix}p\\\hline q\lor p\end{matrix}}$	$p\to p\lor q$ $p\to q\lor p$
$\to \,$	Teorema de la deducción	$I\to \,$	${\begin{array}{l}{\begin{array}{|l|}\hline \quad p\quad \\\quad q\quad \\\hline \end{array}}\\\;\ p\to q\end{array}}$ $Supuesto$ $\;\;$	$(p\to q)\to p\to q$ $p\land q\to p\to q$ $p\land q\to q\to p$
$\leftrightarrow \,$	Introducción del bicondicional	$I\leftrightarrow \,$	${\begin{matrix}p\to q\\{\underline {\;q\to p\;}}\\{\overline {\;p\leftrightarrow q\;}}\end{matrix}}\qquad {\begin{matrix}p\to q\\{\underline {\;q\to p\;}}\\{\overline {\;q\leftrightarrow p\;}}\end{matrix}}$	$p\to q\land q\to p\leftrightarrow p\leftrightarrow q$ $p\to q\land q\to p\leftrightarrow q\leftrightarrow p$