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)

Un sistema intuicionista de cálculo proposicional

Según Hilbert y Ackermann, el intuicionismo "rechaza por principio la noción de que a todas las aserciones matemáticas haya de corresponder uno de los valores, «verdadero» o «falso»", y eso debido a que "en su opinión [del intuicionismo] se oculte aquí el supuesto infundado de que sería posible resolver alguna vez todos los problemas matemáticos¹.

Por ende, para representar conexiones lógicas entre proposiciones en un sistema donde rija tal principio, el significado de los signos conectivos no será,, como lo son habitualmente, funciones veritativas.

En lugar de los valores verdad puede usarse el concepto de construcción de una proposición, es decir de demostración mediante razonamientos correctos desde este punto de vista. Así, a partir de «φ ∧ ψ» pueden construirse tanto «φ» como «ψ»; y de cualquiera de éstos últimos se puede construir «φ ∨ ψ», etc. (ver más adelante).

Hay ejemplos de fórmulas que en la lógica clásica son válidas universalmente, mas no para la intuicionista. Por ejemplo «A ∨ ¬A». Tampoco lo son, intuicionísticamente, las fórmulas «¬¬A → A», «(¬B → ¬A) → (A → B)», «A ∨ (A → B)», «(A → B) ∨ (B → A)» ni «(A → B) → ¬A ∨ B»; todas ellas válidas en el cálculo proposicional de, por ejemplo, este otro post.

_____________________

En lugar de fórmulas elementales o axiomas, partiremos de ciertas relaciones fundamentales de deductibilidad. A saber:

1. Φ_n es deducible de las hipótesis Φ₁, ..., Φn (n ≥ 1)

2. Φ ∧ Ψ es deducible de las hipótesis Φ, Ψ

3. Φ es deducible de Φ ∧ Ψ

4. Φ ∨ Ψ es deducible de Φ

5. Φ ∨ Ψ es deducible de Ψ

6. Ψ es deducible de Φ, Φ → Ψ

7. La fórmula arbitraria Ψ es deducible de Φ, ¬Φ



También existen las siguientes reglas:

I. Si «Ψ» es deducible de «Φ₁, ..., Φ_n», también lo es de toda permutación de «Φ₁, ..., Φ_n»

II. Si la fórmula «Γ» es deducible de «Ψ₁, ..., Ψ_k», y cada una de estas últimas fórmulas es deductible de «Φ₁, ..., Φ_n», «Γ» es asimismo deductible de «Φ₁, ..., Φ_n».

III. Si la fórmula «Δ» es deducible de «Φ₁, ..., Φ_n», «Ψ» y es deducible de «Φ₁, ..., Φ_n», «Γ», también es deducible, «Δ», de «Φ₁, ..., Φ_n», «Φ ∨ Ψ» (n ≥ 0).

IV. Si la fórmula «Γ» es deductible de «Φ₁, ..., Φ_n», «Ψ», también es la fórmula «Ψ → Γ» deductible de «Φ₁, ..., Φ_n» (n ≥ 0)

V. Si la fórmula «Γ» es deductible de «Φ₁, ..., Φ_n», «Ψ» y también «¬Γ» es deductible de las mismas hipótesis, la fórmula «¬Ψ» es deductible de «Φ₁, ..., Φ_n» (n ≥ 0)

(Seguir leyendo)
________
Notas.
1. Hilbert y Ackermann, Elementos de lógica teórica. Cap. 1, §10.