PDF de programación - Tema 8: Deducción natural en lógica de primer orden - Lógica informática (2015–16)

PD Tema 8: Deducción natural en lógica de primer orden

Lógica informática (2015–16)

Tema 8: Deducción natural en lógica de primer orden

José A. Alonso Jiménez
Andrés Cordón Franco
María J. Hidalgo Doblado

Grupo de Lógica Computacional

Departamento de Ciencias de la Computación e I.A.

Universidad de Sevilla

1 / 29

PD Tema 8: Deducción natural en lógica de primer orden

Tema 8: Deducción natural en lógica de primer orden

1. Sustituciones

2. Reglas de deducción natural de cuantificadores

3. Reglas de la igualdad

2 / 29

PD Tema 8: Deducción natural en lógica de primer orden

Sustituciones

Tema 8: Deducción natural en lógica de primer orden

1. Sustituciones

Definición de sustitución
Aplicación de sustituciones a términos
Aplicación de sustituciones a fórmulas
Sustituciones libres

2. Reglas de deducción natural de cuantificadores

3. Reglas de la igualdad

3 / 29

PD Tema 8: Deducción natural en lógica de primer orden

Sustituciones

Definición de sustitución

Sustituciones
(ti ,

σ(x ) =

si x es xi;
si x /∈ {x1, . . . , xn}

x ,

Def.: Una sustitución σ (de L) es una aplicación σ : Var → Térm(L).
Notación: [x1/t1, x2/t2, . . . , xn/tn] representa la sustitución σ definida por

Ejemplo: [x /s(0), y /x + y ] es la sustitución σ de Var en los términos de

la aritmética definida por

σ(x ) = s(0), σ(y ) = x + y y σ(z) = z para z ∈ Var \ {x , y}

Notación: σ, σ1, σ2, . . . representarán sustituciones.

4 / 29

PD Tema 8: Deducción natural en lógica de primer orden

Sustituciones

Aplicación de sustituciones a términos

Aplicación de sustituciones a términos

Def.: t[x1/t1, . . . , xn/tn] es el término obtenido sustituyendo en t

las apariciones de xi por ti.

Def.: La extensión de σ a términos es la aplicación

σ : Térm(L) → Térm(L) definida por



tσ =

c,
σ(x ),
f (t1σ, . . . , tnσ),

si t es una constante c;
si t es una variable x;
si t es f (t1, . . . , tn)

Ejemplo: Si σ = [x /f (y , a), y /z], entonces

aσ = a, donde a es una constante.
w σ = w, donde w es una variable distinta de x e y.
h(a, x , w )σ = h(aσ, x σ, w σ) = h(a, f (y , a), w )
f (x , y )σ = f (x σ, y σ) = f (f (y , a), z)
h(a, f (x , y ), w )σ = h(aσ, f (x , y )σ, w σ) = h(a, f (f (y , a), z), w )

5 / 29

PD Tema 8: Deducción natural en lógica de primer orden

Sustituciones

Aplicación de sustituciones a fórmulas

Aplicación de sustituciones a fórmulas

Def.: F [x1/t1, . . . , xn/tn] es la fórmula obtenida sustituyendo en

Def.: La extensión de σ a fórmulas es la aplicación

F las apariciones libres de xi por ti.
σ : Fórm(L) → Fórm(L) definida por



F σ =
P(t1σ, . . . , tnσ),
t1σ = t2σ,
¬(Gσ),
Gσ ∗ Hσ,
(Qx )(Gσx ),

(x ,

si F es la fórmula atómica P(t1, . . . , tn);
si F es la fórmula t1 = t2;
si F es ¬G;
si F es G ∗ H;
si F es (Qx )G y Q ∈ {∀,∃}

donde σx es la sustitución definida por

σx (y ) =

si y es x;
si y es distinta de x

σ(y ),

.

6 / 29

PD Tema 8: Deducción natural en lógica de primer orden

Sustituciones

Aplicación de sustituciones a fórmulas

Ejemplos de aplicación de sustituciones a fórmulas

Ejemplos: Si σ = [x /f (y ), y /b], entonces

(∀x (Q(x ) → R(x , y )))σ = ∀x ((Q(x ) → R(x , y ))σx )
= ∀x (Q(x )σx → R(x , y )σx )
= ∀x (Q(x ) → R(x , b))
(Q(x ) → ∀x R(x , y ))σ = Q(x )σ → (∀x R(x , y ))σ
= Q(f (y )) → ∀x (R(x , y )σx )
= Q(f (y )) → ∀x R(x , b)

(∀x (Q(x ) → ∀y R(x , y )))σ = ∀x ((Q(x ) → ∀y R(x , y ))σx )
= ∀x (Q(x )σx → (∀y R(x , y ))σx )
= ∀x (Q(x ) → ∀y (R(x , y )σxy ))
= ∀x (Q(x ) → ∀y R(x , y ))

7 / 29

PD Tema 8: Deducción natural en lógica de primer orden

Sustituciones

Sustituciones libres

Sustituciones libres

Def.: Una sustitución se denomina libre para una fórmula cuando
todas las apariciones de variables introducidas por la sustitución
en esa fórmula resultan libres.

Ejemplos:

[y /x ] no es libre para ∃x (x < y )
∃x (x < y )[y /x ] = ∃x (x < x )
[y /g(y )] es libre para ∀x (P(x ) → Q(x , f (y )))
∀x (P(x ) → Q(x , f (y )))[y /g(y )]
= ∀x (P(x ) → Q(x , f (g(y ))))
∀x (P(x ) → Q(x , f (y )))[y /g(x )]
= ∀x (P(x ) → Q(x , f (g(x ))))

[y /g(x )] no es libre para ∀x (P(x ) → Q(x , f (y )))

Convenio: Al escribir F σ supondremos que σ es libre para F.

8 / 29

PD Tema 8: Deducción natural en lógica de primer orden

Reglas de deducción natural de cuantificadores

Tema 8: Deducción natural en lógica de primer orden

1. Sustituciones

2. Reglas de deducción natural de cuantificadores

Reglas del cuantificador universal
Reglas del cuantificador existencial
Demostración de equivalencias por deducción natural

3. Reglas de la igualdad

9 / 29

PD Tema 8: Deducción natural en lógica de primer orden

Reglas de deducción natural de cuantificadores

Reglas del cuantificador universal

Regla de eliminación del cuantificador universal

Regla de eliminación del cuantificador universal:

∀x F
F [x /t]

∀e

donde [x /t] es libre para F.

Nota: Analogía con ∧e1 y ∧e2.
Ejemplo: P(c),∀x [P(x ) → ¬Q(x )] ‘ ¬Q(c)

1
2
3
4

P(c)
premisa
∀x (P(x ) → ¬Q(x )) premisa
P(c) → ¬Q(c)
¬Q(c)

∀e 2
→e 3, 1

Nota: ∀x ∃y (x < y ) 6‘ ∃y (y < y ).

10 / 29

PD Tema 8: Deducción natural en lógica de primer orden

Reglas de deducción natural de cuantificadores

Reglas del cuantificador universal

Regla de introducción del cuantificador universal
x0

...

donde x0 es una variable nueva, que no aparece fuera de la caja.

F [x /x0]
∀x F

∀i

Nota: Analogía con ∧i.
∀x [P(x ) → ¬Q(x )],∀x P(x ) ‘ ∀x ¬Q(x )
∀x (P(x ) → ¬Q(x )) premisa
∀x P(x )
premisa
actual x0
supuesto
∀e 1, 3
P(x0) → ¬Q(x0)
∀e 2, 3
P(x0)
→e 4, 5
¬Q(x0)
∀x ¬Q(x )
∀i 3 − 6

1
2
3
4
5
6
7

11 / 29

PD Tema 8: Deducción natural en lógica de primer orden

Reglas de deducción natural de cuantificadores

Reglas del cuantificador existencial

Regla de introducción del cuantificador existencial

Regla de introducción del cuantificador existencial:

F [x /t] ∃i
∃x F

donde [x /t] es libre para F.
Nota: Analogía con ∨i1 y ∨i2.
Ejemplo 3: ∀x P(x ) ‘ ∃x P(x )
∀x P(x ) premisa
∀e 1
P(x0)
∃x P(x ) ∃i 2

1
2
3

12 / 29

PD Tema 8: Deducción natural en lógica de primer orden

Reglas de deducción natural de cuantificadores

Reglas del cuantificador existencial

Regla de eliminación del cuantificador existencial

x0 F [x /x0]

...
G

∃x F

∃e

donde x0 es una variable nueva, que no aparece fuera de la caja.

Nota: Analogía con ∨e.
Ejemplo: ∀x [P(x ) → Q(x )],∃x P(x ) ‘ ∃x Q(x )

G

1
2
3
4
5
6
7

∀x (P(x ) → Q(x )) premisa
∃x P(x )
premisa
supuesto
actual x0, P(x0)
P(x0) → Q(x0)
∀e 1, 3
→e 4, 3
Q(x0)
∃i 5
∃x Q(x )
∃x Q(x )
∃e 2, 3 − 6

13 / 29

PD Tema 8: Deducción natural en lógica de primer orden

Reglas de deducción natural de cuantificadores

Demostración de equivalencias por deducción natural

Equivalencias

Sean F y G fórmulas.

[1(a)] ¬∀x F ≡ ∃x ¬F
[1(b)] ¬∃x F ≡ ∀x ¬F

Sean F y G fórmulas.

[3(a)] ∀x F ∧ ∀x G ≡ ∀x (F ∧ G)
[3(b)] ∃x F ∨ ∃x G ≡ ∃x (F ∨ G)

Sean F y G fórmulas.

[4(a)] ∀x ∀y F ≡ ∀y ∀x F
[4(b)] ∃x ∃y F ≡ ∃y ∃x F

Sean F y G fórmulas y x una varible no libre en G.

[2(a)] ∀x F ∧ G ≡ ∀x (F ∧ G)
[2(b)] ∀x F ∨ G ≡ ∀x (F ∨ G)
[2(c)] ∃x F ∧ G ≡ ∃x (F ∧ G)
[2(d)] ∃x F ∨ G ≡ ∃x (F ∨ G)

14 / 29

PD Tema 8: Deducción natural en lógica de primer orden

Reglas de deducción natural de cuantificadores

Demostración de equivalencias por deducción natural

Equivalencia 1(a) →
¬∀x P(x ) ‘ ∃x ¬P(x )

premisa
supuesto
supuesto
supuesto
∃i 4, 3
¬e 2, 5
RAA 4 − 6
∀i 3 − 7
¬e 1, 8
RAA 2 − 9

15 / 29

¬∀x P(x )
¬∃x ¬P(x )
actual x0
¬P(x0)
∃x ¬P(x )

1
2
3
4
5
6 ⊥
7
8
9 ⊥
10 ∃x ¬P(x )

P(x0)
∀x P(x )

PD Tema 8: Deducción natural en lógica de primer orden

Reglas de deducción natural de cuantificadores

Demostración de equivalencias por deducción natural

Equivalencia 1(a) ←
∃x ¬P(x ) ‘ ¬∀x P(x )
∃x ¬P(x )
¬¬∀x P(x )
actual x0,¬P(x0)
∀x P(x )
P(x0)

1
2
3
4
5
6 ⊥
7 ⊥
8

¬∀x P(x )

premisa
supuesto
supuesto
¬¬e 2
∀e 4
¬e 3, 5
∃e 1, 3 − 6
RAA 2 − 7

16 / 29

PD Tema 8: Deducción natural en lógica de primer orden

Reglas de deducción natural de cuantificadores

Demostración de equivalencias por deducción natural

Equivalencia 1(a) ↔
¬∀x P(x ) ≡ ∃x ¬P(x )
¬∀x P(x )
∃x ¬P(x )
¬∀x P(x ) → ∃x ¬P(x ) →i 1 − 2
∃x ¬P(x )
supuesto
¬∀x P(x )
Lema 1(a) ←
∃x ¬P(x ) → ¬∀x P(x ) →i 4 − 5
¬∀x P(x ) ↔ ∃x ¬P(x ) ↔i 3, 6

supuesto
Lema 1(a) →

1
2
3
4
5
6
7

17 / 29

PD Tema 8: Deducción natural en lógica de primer orden

Reglas de deducción natural de cuantificadores

Demostración de equivalencias por deducción natural

Equivalencia 3(a) →
∀x (P(x ) ∧ Q(x )) ‘ ∀x P(x ) ∧ ∀x Q(x )
premisa
1
supuesto
2
∀e 1, 2
3
∧e1 3
4
∀i 2 − 4
5
supuesto
6
∀e 1, 6
7
∧e2 7
8
∀i 6 − 8
9
10 ∀x P(x ) ∧ ∀x Q(x ) ∧i 5, 9

∀x (P(x ) ∧ Q(x ))
actual x0
P(x0) ∧ Q(x0)
P(x0)
∀x P(x )
actual x1
P(x1) ∧ Q(x1)
Q(x1)
∀x Q(x )

18 / 29

PD Tema 8: Deducción natural en lógica de primer orden

Reglas de deducción natural de cuantificadores

Demostración de equivalencias por deducción natural

Equivalencia 3(a) ←
∀x P(x ) ∧ ∀x Q(x ) ‘ ∀x (P(x ) ∧ Q(x ))
∀x P(x ) ∧ ∀x Q(x ) premisa
actual x0
supuesto
∧e1 1
∀x P(x )
∀e 3, 2
P(x0)
∀x Q(x )
∧e2 1
∀e 5
Q(x0)
P(x0) ∧ Q(x0)
∧i 4, 6
∀i 2 − 7
∀x (P(x ) ∧ Q(x ))

1
2
3
4
5
6
7
8

19 / 29

PD Tema 8: Deducción natural en lógica de primer orden

Reglas de deducción natural de cuantificadores

Demostración de equivalencias por deducción natural

Equivalencia 3(a) ↔
∀x (P(x ) ∧ Q(x )) ≡ ∀x P(x ) ∧ ∀x Q(x )

1
2
3
4
5
6
7

supuesto
Lema 3(a) →

∀x (P(x ) ∧ Q(x ))
∀x P(x ) ∧ ∀x Q(x )
∀x (P(x ) ∧ Q(x )) → ∀x P(x ) ∧ ∀x Q(x ) →i 1 − 2
∀x P(x ) ∧ ∀x Q(x )
supuesto
∀x (P(x ) ∧ Q(x ))
Lema 3(a) ←
∀x P(x ) ∧ ∀x Q(x ) → ∀x (P(x ) ∧ Q(x )) →i 4 − 5
∀x (P(x ) ∧ Q(x )) ↔ ∀x P(x ) ∧ ∀x Q(x ) ↔i 3, 6

20 / 29

PD Tema 8: Deducción natural en lógica de primer or