LMF Tema 8: Deducción natural en lógica de primer orden
Lógica matemática y fundamentos (2016–17)
Tema 8: Deducción natural en lógica de primer orden
José A. Alonso Jiménez
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
LMF 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
LMF 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
LMF 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
LMF 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
LMF 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
LMF 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
LMF 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
LMF 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
LMF 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
LMF 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
LMF 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
LMF 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
LMF 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
LMF 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)
LMF 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
LMF 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
LMF 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
LMF 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
LMF 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
LMF 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(b) →
∃x P(x) ∨ ∃x Q(x) ‘ ∃x (P(x) ∨ Q(
Comentarios de: Tema 8: Deducción natural en lógica de primer orden - Lógica matemática y fundamentos (2016–17) (0)
No hay comentarios