Algunas demostraciones sin el «tercero excluído»

En éste post habíamos puesto una lista de fórmulas válidas en el cálculo intuicionista, que pueden ser demostradas con el sistema deductivo que se presentó en este otro post, como un ejercicio para el lector.

A fin de alentar al lector a completar la tarea, se muestran abajo demostraciones de los primeras cuatro. Para poder leerlas remítase al segundo post citado donde figuran las "relaciones de deducibilidad" y las "reglas" (RD. y R. de la columna derecha).



TEOREMA i)      ⊢ A → ¬¬A

a)  ¬A, A ⊢ A               RD.1
b)  A, ¬A ⊢ A               R.I, a
c)  A, ¬A ⊢ ¬A             RD.1
d)  A ⊢ ¬¬A                 R.V. b, c.



TEOREMA ii)        ⊢ A → ((A → B) → B))

a)    A, A → B ⊢ B                 RD. (6)
b)    A ⊢ (A → B) → B            Regla IV, a.
c)    ⊢ A → ((A → B) → B))     Regla IV




TEOREMA iii)     ⊢ A ∧ (A → B) → B

a)  A, A → B ⊢ B                 RD.6
b)  A ∧ (A → B) ⊢ A            RD.3
c)  A ∧ (A → B) ⊢ A → B      RD.3
d)  A ∧ (A → B) ⊢ B            R.II, a, b, c.



TEOREMA iv)    ⊢ (A → B) → (¬B → ¬A)

Para este teorema demostraremos primero un Lema:

LEMA I:    si Φ ⊢ Ψ, entoces Φ, Χ ⊢ Ψ

a)  Φ ⊢ Ψ                     hipótesis
b)  Χ, Φ ⊢ Φ                 RD.1
c)  Χ, Φ ⊢ Ψ                 R.II, a, b
d)  Φ, Χ ⊢ Ψ                 R.I, c


a)  A, A → B ⊢ B                 RD.6
b)  A, A → B, ¬B ⊢ ¬B        RD.1
c)  A → B, ¬B, A ⊢ ¬B        R.I, b.
d)  A, A → B, ¬B ⊢ B           Lema I, a.
e)  A → B, ¬B, A ⊢ B           R.I, d.
f)  A → B, ¬B ⊢ ¬A             R.V, c, e.
g)  A → B ⊢ ¬B → ¬A          R.IV, f.
h)  (A → B) → (¬B → ¬A)     R.IV, g.


(Seguir leyendo)