Ahora consideremos, siguiendo con el post anterior sobre la sustitutividad de la equivalencia, que se realiza la sustitución y hay alguna ocurrencia en A de algún →, ~ o ∀.
Existen tres casos:
1) A es A₁ → A₂,
2)A es ~A₁ y
3) A es ∀xA₁.
Primer caso: A es A₁ → A₂
Aquí (salvo en el caso a, ver post anterior) B es B₁ → B₂ donde B₁ y B₂ resultan por sustitución de M por N en A₁ y A₂. Por hipótesis de inducción:
*1) ∀x₁x₂...nₙ[M ≡ N] →. A₁ ≡ B₁ y
*2) ∀x₁x₂...nₙ[M ≡ N] →. A₂ ≡ B₂
Necesitamos probar, entonces, que de (*1) y (*2) se sigue el teorema.
Primero probemos T₁:
p → q →. r → s →. q → r →. s → t
Cuando figuren dos letras proposicionales una al lado de la otra así: pq, significará [p → q].
a) pq →. qr →. ps
transitividad de →
b) ps →. st →. pt
transitividad de →
c) [ps →. st → pt] →. qr → ps →. qr →. st → pt
transitividad de →
d) qr → ps →. qr →. st → pt
modus ponens (c y b)
e) pq →. qs →. st → pt
Regla de transitividad, (a y d)
f) p → qr →. q → pr
ley de conmutación
g) [qs →. st → pt] →. st →. qs → pt
R2, (f)
h) pq →. st →. qs → pt
Regla de transitividad (e y g)
Ahora probemos T₂:
[p →. q → rs] →. pq →. pr → ps
a) [p →. r → s] →. pr → ps
Axioma 2
b) [p →. q → rs] →. pq →. p → rs
Axioma 2
c) [p → rs →. pr → ps] →. [pq →. p → rs] →. pq →. pr → ps
ley de transitividad de → 2
d) [pq →. p → rs] →. pq →. pr → ps
modus ponens (c y a)
e) [p →. q → rs] →. pq →. pr → rs
Regla de transitividd, (b y d)
Ahora escojamos cinco fórmulas cuales quiera A₁, A₂, B₁, B₂ y C tales que sea
*11) ⊢ C →. A₁ → B₁, ⊢ C →. A₂ → B₂
*12) ⊢ C →. A₂ → B₂ y ⊢ C →. A₂ → B₂
(es decir ⊢ C →. A₁ ≡ B₁ y ⊢ C →. A₂ ≡ B₂)
Tenemos:
a) B₁ → A₁ →. A₂ → B₂ →. A₁ → A₂ →. B₁ → B₂ y
b) A₁ → B₁ →. B₂ → A₂ →. B₁ → B₂ →. A₁ → A₂
ambos por regla 2, T₁.
Sustituyendo en T₂, obtenemos (c) y (d):
c) [C →. B₁A₁ →. A₂B₂ →. A₁A₂ → B₁B₂] →. C → B₁A₁ →. C → A₂B₂ →. C →. A₁A₂ → B₁B₂
d) [C →. A₁B₁ →. B₂A₂ →. B₁B₂ → A₁A₂] →. C → A₁B₁ →. C → B₂A₂ →. C →. B₁B₂ → A₁A₂
Luego:
e) C →. B₁A₁ →. A₂B₂ →. A₁A₂ → B₁B₂
Lema 1, (a)
f) C →. A₁B₁ →. B₂A₂ →. B₁B₂ → A₁A₂
Lema 1, (b)
Y entonces
h) C → B₁A₁ →. C → A₂B₂ →. C →. A₁A₂ → B₁B₂
i) C → A₁B₁ →. C → B₂A₂ →. C →. B₁B₂ → A₁A₂
ambos por modus ponens (c y e) y (d y f). Esto se cumple para cualesquiera fórmulas (bf) C, A₁, A₂, B₁ y B₂.
Ahora sustituímos C por ∀x₁x₂...nₙ[M ≡ N] (regla de sust.), con lo cual obtenemos:
h') [∀x₁x₂...nₙ[M ≡ N] →. B₁ → A₁] →. [∀x₁x₂...nₙ[M ≡ N] →. A₂ → B₂] →. ∀x₁x₂...nₙ[M ≡ N] →. A₁ → A₂ →. B₁ → B₂
i') [∀x₁x₂...nₙ[M ≡ N] →. A₁ → B₁] →. [∀x₁x₂...nₙ[M ≡ N] →. B₂ → A₂] →. ∀x₁x₂...nₙ[M ≡ N] →. B₁ → B₂ → A₁ → A₂
Entonces (recuérdense las hipótesis de la inducción *1 y *2):
j) [∀x₁x₂...nₙ[M ≡ N] →. A₂ → B₂] →. ∀x₁x₂...nₙ[M ≡ N] →. A₁ → A₂ →. B₁ → B₂
modus ponens, (h' y *1)
k) ∀x₁x₂...nₙ[M ≡ N] →. A₁ → A₂ →. B₁ → B₂
modus ponens, (j y *2)
l) [∀x₁x₂...nₙ[M ≡ N] →. B₂ → A₂] →. ∀x₁x₂...nₙ[M ≡ N] →. B₁ → B₂ → A₁ → A₂
modus ponens, (i' y *1)
m) ∀x₁x₂...nₙ[M ≡ N] →. B₁ → B₂ → A₁ → A₂
modus ponens (l y *2)
Y como A es A₁ → A₂ y B es B₁ → B₂, luego hemos probado:
n) ∀x₁x₂...nₙ[M ≡ N] →. A ≡. B
Ahora el segundo caso: A es ~A₁
Así, B es ~B₁ y nuestra hipótesis de inducción establece que
*) ∀x₁x₂...nₙ[M ≡ N] →. A₁ ≡ B₁
Debemos probar
[C →. q ≡ r] →. C → ~q ≡ ~r
y sustutuir C por la hipótesis, q por A₁ y r por B₁ para obtener por modus ponens lo que queremos, de modo similar al primer caso.
Sabemos por el axioma 3 y por modus tolens que:
a) q ≡ r →. ~q ≡ ~r
Por otra parte:
b) p → q →. C →. p → q
Axioma 1
c) [C →. p → q] →. C → p →. C → q
Axioma 2
d) [C →. q ≡ r →. ~q ≡ ~r] →. C → q ≡ r →. C →. ~q ≡ ~r
Sustituyendo en (b)
e) C →. q ≡ r →. ~q ≡ ~r
lema 1, (a)
f) C → q ≡ r →. C →. ~q ≡ ~r
modus ponens (d y e)
Finalmente, nos queda el tercer caso: A es ∀xA₁
Aquí, B es ∀xB₁. hay que probar:
A ≡ₓ B →. (x)A ≡ (x)B
Y con eso obtenemos la prueba utilizando la transitivida de →.
Sabemos, desde luego, que:
a) A ≡ B →. A → B y
b) A ≡ B →. B → A , por la definición de ≡.
c) ∀x[A ≡ B] →. A → B
regla 5 y reflexividad de →
d) ∀x[A ≡ B] →. ∀x[A → B]
Lema 4
e) (x)A → A
regla 5
f) [p →. q → r] →. s → q →. p → s → r
ver prueba
g) [A ≡ₓ B →. A → B] →. (x)A → A →. [A ≡ₓ B →. (x)A → B]
sust, (f)
h) (x)A → A →. [A ≡ₓ B →. (x)A → B]
modus ponens, (g y c)
i) A ≡ₓ B →. (x)A → B
modus ponens, (h y e)
j) A ≡ₓ B →. (x)A →ₓ B
lema 4, i
k) (x)A →ₓ B →. (x)A → (x)B
Axioma 4
l) A ≡ₓ B →.(x)A → (x)B
Regla de transitividad
No hay comentarios:
Publicar un comentario