Deducción Natural

1. Lógica Proposicional

El método de deducción natural, desarrollado por Gentzen, utiliza dos reglas de inferencia por cada conectiva: una para insertar la conectiva y otra para eliminarla

Las reglas de inferencia son:

∧I

A B

A∧B

∧E

A∧B

∨I

A∨B

∨E

A∨B A→C B→C

→I

A
...
B

A→B

→E

A→B A

↔I

A→B B→A

A↔B

↔E

A↔B

A→B

A↔B

B→A

∼I

A
...
B∧∼B

∼A

∼E

∼A
...
B∧∼B

∼A∨A

A∧∼A

A continuación se incluyen varios ejemplos de demostraciones en dedución natural.

Ejemplo ([p∧q]⇒p∧(q∨r))

Ejemplo ([p→q,q→r]⇒p→r)

Ejemplo ([p→q∨r,q→r,r→s]⇒p→s)

Ejemplo ([p→∼q,r→q]⇒∼(p∧r))

Ejemplo ([∼p]⇒p→q)

Ejemplo (p↔∼∼p)

Ejemplo (p→q⇒∼p∨q)

2. Lógica de Predicados

Para la lógica de predicados se añaden las siguientes reglas de inferencia para insertar y eliminar cada uno de los cuantificadores.

∀I

(t) libre
...
A(t)

∀xA(x)

∀E

∀xA(x)

A(t)

∃I

A(t)

∃xA(x)

∃E

∃xA(x)

A(t) libre
...
B

Deben cumplirse las siguientes normas:

En las reglas ∀I y ∃E, el término t no debe aparecer en ninguna caja anterior abierta.
En la regla ∃E la fórmula B no puede contener el término t

A continuación se incluyen varias demostraciones de razonamientos en lógica de predicados mediante deducción natural

Ejemplo ([∀x(p(x)→q(x)),∀x(r(x)→q(x)),∀x(p(x)∨r(x))]⇒∀xq(x))

Ejemplo ([∀x(p(x)→q(x),∃xp(x)]⇒∃xq(x))

Ejemplo ([∃xp(x)]⇒∼∀x∼p(x))

Ejemplo ([∼∀x∼p(x)]⇒∃xp(x))

Ejemplo ([∃x(p(x) ∨ q(x)), ∀x(p(x)→r(x,x)), ∼∃xq(x)]⇒∃xr(x,x))

Ejemplo ([∃x∀y p(x,y)]⇒∀y∃x p(x,y))

Ejemplo ([∀x(r(x)→q(x), ∃x(p(x)∧∼q(x))]⇒∃x(p(x)∧∼r(x)))

3. Referencias y Agradecimientos

Los ejemplos han sido implementados mediante el sistema YanDES que permite realizar demostraciones en deducción natural y convertir dichas demostraciones a diversos formatos: XML, HTML, SVG, etc.
Estos apuntes están siendo utilizados en la asignatura Lógica
En la versión HTML, las demostraciones se almacenan en formato SVG. Si no se pueden ver adecuadamente, es posible obtener un visualizador en: SVG Implementations. Además, las páginas utilizan codificación UTF-8 para representar conectivas y cuantificadores de lógica. En caso de problemas, puede consultarse la Página de Unicode
Se agradecerá cualquier comentario o sugerencia sobre estos apuntes.