Deducción natural/Reglas de eliminación

Conectiva	Nombre de la regla	Abreviación	Formalización	Cálculo de secuentes
$\neg$	Doble negación	$E \neg$	$\begin{matrix} \underline{p} \\ \overline{\neg \neg p} \end{matrix}$	$\neg \neg p \leftrightarrow p$
$\land$	Eliminación de la conjunción	$E \land$	$\begin{matrix} p \land q \\ p \end{matrix} \begin{matrix} p \land q \\ q \end{matrix}$	$p \land q \to p$ $p \land q \to q$
$\lor$	Eliminación de la disyunción	$E \lor$	$\begin{matrix} p \lor q \\ p \to r \\ q \to r \\ r \end{matrix} \begin{matrix} \neg p \lor \neg q \\ r \to p \\ r \to q \\ \neg r \end{matrix}$	$(p \lor q) \land (p \to r) \land (q \to r) \to r$ $(\neg p \lor \neg q) \land (r \to p) \land (r \to q) \to \neg r$
$\to$	Modus ponendo ponens	$M P$	$\begin{matrix} p \to q \\ p \\ q \end{matrix}$	$(p \to q) \land p \to q$
$\to$	Modus tollendo tollens	$M T$	$\begin{matrix} p \to q \\ \neg q \\ \neg p \end{matrix}$	$(p \to q) \land \neg q \to \neg p$
$\leftrightarrow$	Eliminación del bicondicional	$E \leftrightarrow$	$\begin{matrix} p \leftrightarrow q \\ p \to q \end{matrix} \begin{matrix} p \leftrightarrow q \\ q \to p \end{matrix}$	$p \leftrightarrow q \to p \to q$ $p \leftrightarrow q \to q \to p$

Menú de navegación