Proposiciones intuicionísticamente válidas

Las siguientes proposiciones son válidas en el cálculo intuicionista:

i) A → ¬¬A

ii) A → ((A → B) → B))

iii) A ∧ (A → B) → B

iv) (A → B) → (¬B → ¬A)

v) (A → B) → ((B → C) → (A → C))

vi) ¬¬¬A → ¬A

vii) ¬A → ¬¬¬A

viii) ¬A → ¬(A ∧ B)

ix) ¬¬(A ∨ ¬A)

x) ¬(A ∨ B) → ¬A

xi) ¬(A ∨ B) → ¬A ∧ ¬B

xii) ¬A ∨ B → (A → B)

Podría demostrarse que también lo son en el cálculo proposicional "clásico". Por otra parte, las siguientes son, al contrario, válidas para la lógica clásica, pero no son demostrables en la intuicionista:

xiii) A ∨ ¬A (Ley de tercero excluído)

xiv) ¬¬A → A

xv) (¬B → ¬A) → (A → B)

xvi) ¬(A ∧ B) → ¬A ∨ ¬B

xvii) A ∨ (A → B)

xviii) (A → B) ∨ (B → A)

xix) (A → B) → ¬A ∨ B


(Seguir leyendo)

_________________

Figura como ejercicio Nro. 14 de Hilbert-Ackermann (1928) la demostración de (i) a (xii) según el sistema intuicionista que se encuentra en este link. El resto de las proposciones podrán responderse sirviéndose de éste otro método.