Sustitutividad de la equivalencia, segunda parte.

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