Deducció natural

La deducció natural és una aproximació a la teoria de la demostració en la que es busca capturar la manera en que les persones raonen naturalment en construir demostracions matemàtiques. En lloc de contar en uns pocs axiomes als que s'apliquen unes poques regles d'inferència, la deducció natural propon buidar la llista de axioma i ampliar la de regles d'inferència, introduint dos regles per a cada constant llògica: una per a introduir-la i una atra per a eliminar-la. Una demostració es construïx partint de supòsits i aplicant les regles per a aplegar a la conclusió desijada. Servix per a demostrar la validea d'un argument.

La deducció natural va ser introduïda per Gerhard Gentzen en el seu treball Investigacions sobre l'inferència llògica (Untersuchungen über dones logische Schliessen), publicat en 1934-1935.

Regles d'inferència

Conectivas

Conectiva	Nom de la regla	Abreujament	Formalisació	Càlcul de secuentes
$\mathrm{\neg }$	Introducció de la negació (vore reducció l'absurt)	$I\mathrm{\neg }$	$\begin{array}{c}\varphi \\ ⋮\\ \perp \\ \mathrm{\neg }\varphi \end{array}$
	Eliminació de la negació	$E\mathrm{\neg }$	$\frac{\mathrm{\neg }\mathrm{\neg }\varphi }{\varphi }$	$\mathrm{\neg }\mathrm{\neg }\varphi ⊢\varphi$
$\wedge$	Introducció de la conjunció	$I\wedge$	$\begin{array}{c}\varphi \\ \psi \\ \varphi \wedge \psi \end{array}\begin{array}{c}\varphi \\ \psi \\ \psi \wedge \varphi \end{array}$	$\varphi ,\psi ⊢\varphi \wedge \psi \varphi ,\psi ⊢\psi \wedge \varphi$
	Eliminació de la conjunció	$E\wedge$	$\frac{\varphi \wedge \psi }{\varphi }\frac{\varphi \wedge \psi }{\psi }$	$\varphi \wedge \psi ⊢\varphi \varphi \wedge \psi ⊢\psi$
$\vee$	Introducció de la disjunció	$I\vee$	$\frac{\varphi }{\varphi \vee \psi }\frac{\varphi }{\psi \vee \varphi }$	$\varphi ⊢\varphi \vee \psi \varphi ⊢\psi \vee \varphi$
	Eliminació de la disjunció (vore silogisme disyuntivo)	$E\vee$	$\begin{array}{c}\varphi \vee \psi \\ \mathrm{\neg }\varphi \\ \psi \end{array}\begin{array}{c}\varphi \vee \psi \\ \mathrm{\neg }\psi \\ \varphi \end{array}$	$\varphi \vee \psi ,\mathrm{\neg }\varphi ⊢\psi \varphi \vee \psi ,\mathrm{\neg }\psi ⊢\varphi$
$\to$	Introducció del condicional material (vore teorema de la deducció)	$I\to$	$\begin{array}{c}\varphi \\ ⋮\\ \psi \\ \varphi \to \psi \end{array}$
	Eliminació del condicional material (vore modus ponens)	$E\to$	$\begin{array}{c}\varphi \to \psi \\ \varphi \\ \psi \end{array}$	$\varphi \to \psi ,\varphi ⊢\psi$
$\leftrightarrow$	Introducció del bicondicional	$I\leftrightarrow$	$\begin{array}{c}\varphi \to \psi \\ \psi \to \varphi \\ \varphi \leftrightarrow \psi \end{array}\begin{array}{c}\varphi \to \psi \\ \psi \to \varphi \\ \psi \leftrightarrow \varphi \end{array}$	$\varphi \to \psi ,\psi \to \varphi ⊢\psi \leftrightarrow \varphi$
	Eliminació del bicondicional	$E\leftrightarrow$	$\frac{\varphi \leftrightarrow \psi }{\varphi \to \psi }\frac{\varphi \leftrightarrow \psi }{\psi \to \varphi }$	$\varphi \leftrightarrow \psi ⊢\varphi \to \psi \varphi \leftrightarrow \psi ⊢\psi \to \varphi$

Quantificadors

Siga a una constant d'individu i t un terme. Siga A(b/c) el resultat de reemplaçar totes les aparicions de b en A per c. Després:

Quantificador	Nom de la regla	Abreujament	Formalisació	Càlcul de secuentes
$\mathrm{\forall }$	Introducció del quantificador universal	$I\mathrm{\forall }$	$\frac{\varphi (a)}{\mathrm{\forall }x\varphi (a/x)}$	$\varphi (a)⊢\mathrm{\forall }x\varphi (a/x)$
	Eliminació del quantificador universal	$E\mathrm{\forall }$	$\frac{\mathrm{\forall }x(\varphi )}{\varphi [x/a]}$	$\mathrm{\forall }x(\varphi )⊢\varphi [x/a]$
$\mathrm{\exists }$	Introducció del quantificador existencial	$I\mathrm{\exists }$	$\frac{\varphi (a)}{\mathrm{\exists }x\varphi (a/x)}$	$\varphi (a)⊢\mathrm{\exists }x\varphi (a/x)$
	Eliminació del quantificador existencial	$E\mathrm{\exists }$	$\frac{\mathrm{\exists }x(\varphi )}{\varphi (x/t)}$	$\mathrm{\exists }x(\varphi )⊢\varphi (x/t)$

Demostracions

Eixemple senzill

A demostrar: $\varphi \to \varphi$
Pas	Fòrmula	Raó
1	$\varphi$	Supòsit.
2	$\varphi \vee \psi$	Des de (1) per introducció de la disjunció.
3	$(\varphi \vee \psi )\wedge \varphi$	Des de (1) i (2) per introducció de la conjunció.
4	$\varphi$	Des de (3) per eliminació de la conjunció.
5	$\varphi ⊢\varphi$	Resum de (1) fins a (4).
6	$⊢\varphi \to \varphi$	Des de (5) per introducció del condicional. Q.E.D.

Eixemple més complex

En esta secció es presenta una demostració d'una de les lleis de De Morgan. La mateixa diu:

$\mathrm{\neg }(\varphi \vee \psi )\leftrightarrow (\mathrm{\neg }\varphi \wedge \mathrm{\neg }\psi )$

Ya que la conectiva principal és un bicondicional, l'estratègia serà demostrar que $\mathrm{\neg }(\varphi \vee \psi )\to (\mathrm{\neg }\varphi \wedge \mathrm{\neg }\psi )$ i que $(\mathrm{\neg }\varphi \wedge \mathrm{\neg }\psi )\to \mathrm{\neg }(\varphi \vee \psi )$, per a després poder introduir el bicondicional (per mig de la regla d'introducció del bicondicional). Per a obtindre cada una d'estes subfórmulas, que les seues conectivas principals són condicionals materials, es deu supondre l'antecedent i intentar derivar el conseqüent.

A demostrar: $\mathrm{\neg }(\varphi \vee \psi )\leftrightarrow (\mathrm{\neg }\varphi \wedge \mathrm{\neg }\psi )$
Pas	Fòrmula	Raó
1	$\mathrm{\neg }(\varphi \vee \psi )$	Supòsit.
2	$\varphi$	Supòsit.
3	$\varphi \vee \psi$	$I\vee 2$
4	$\perp$	$I\wedge 1,3$
5	$\mathrm{\neg }\varphi$	$I\mathrm{\neg }2-4$
6	$\psi$	Supòsit.
7	$\varphi \vee \psi$	$I\vee 6$
8	$\perp$	$I\wedge 1,7$
9	$\mathrm{\neg }\psi$	$I\mathrm{\neg }6-8$
10	$\mathrm{\neg }\varphi \wedge \mathrm{\neg }\psi$	$I\wedge 5,9$
11	$\mathrm{\neg }(\varphi \vee \psi )\to (\mathrm{\neg }\varphi \wedge \mathrm{\neg }\psi )$	$I\to 1-10$
12	$\mathrm{\neg }\varphi \wedge \mathrm{\neg }\psi$	Supòsit.
13	$\mathrm{\neg }\varphi$	$E\wedge 12$
14	$\mathrm{\neg }\psi$	$E\wedge 12$
15	$\varphi \vee \psi$	Supòsit.
16	$\psi$	$E\vee 13,15$
17	$\perp$	$I\wedge 14,16$
18	$\mathrm{\neg }(\varphi \vee \psi )$	$I\mathrm{\neg }15-17$
19	$(\mathrm{\neg }\varphi \wedge \mathrm{\neg }\psi )\to \mathrm{\neg }(\varphi \vee \psi )$	$I\to 12-18$
20	$\mathrm{\neg }(\varphi \vee \psi )\leftrightarrow (\mathrm{\neg }\varphi \wedge \mathrm{\neg }\psi )$	$I\leftrightarrow 11,19$

Jaśkowski

$⊢$	$\begin{array}{c}\varphi \to (\psi \to \varphi )\\ \begin{array}{c}\varphi \\ \begin{array}{c}\psi \\ \begin{array}{c}\mathrm{\neg }\varphi \\ \mathrm{\perp }\end{array}\\ \varphi \end{array}\\ \psi \to \varphi \end{array}\\ \varphi \to (\psi \to \varphi )\end{array}$
$1.$		$Supuesto$
$2.$		$Supuesto$
$3.$		$Supuesto$
$4.$		$I\wedge 1,3$
$5.$		$I\mathrm{\neg }3-4$
$6.$		$I\to 2-5$
$7.$		$I\to 1-6$

Fitch

$⊢(\varphi \to (\psi \to \chi ))\to ((\varphi \to \psi )\to (\varphi \to \chi ))$

1.     $\varphi \to (\psi \to \chi )$   Supost     2.       $\varphi \to \psi$         Supost       3.         $\varphi$   Supost 4.         $\psi \to \chi$   I→ 1,3 5.         $\psi$   I→ 2,3 6.         $\chi$   I→ 4,5         7.       $\varphi \to \chi$   I→ 3-6       8.     $(\varphi \to \psi )\to (\varphi \to \chi )$   I→ 2-7   9.   $(\varphi \to (\psi \to \chi ))\to ((\varphi \to \psi )\to (\varphi \to \chi ))$   I→ 1-8

Vore també

• Llògica proposicional
• Llògica de primer orde