Rel 5

header {* R5: Eliminación de conectivas *}

theory R5
imports Main 
begin

text {*
  --------------------------------------------------------------------- 
  El objetivo de esta es relación es demostrar cómo a partir de las
  conectivas False, ∧ y ⟶ pueden definirse las restantes.
  --------------------------------------------------------------------- 
*}


text {* --------------------------------------------------------------- 
  Ejercicio 1. Definir ⟷ usando ∧ y ⟶; es decir, sustituir en
      (A ⟷ B) = indefinida
  la indefinida por una fórmula que sólo usa las conectivas ∧ y ⟷ y
  demostrar la equivalencia. 
  ------------------------------------------------------------------ *}

text {* --------------------------------------------------------------- 
  Ejercicio 2. Definir ¬ usando ⟶ y False; es decir, sustituir en
      (¬A) = indefinida
  la indefinida por una fórmula que sólo usa las conectivas ⟶ y False 
  y demostrar la equivalencia. 
  ------------------------------------------------------------------ *}

text {* --------------------------------------------------------------- 
  Ejercicio 3. Definir ∨ usando ⟶ y False; es decir, sustituir en
      (A ∨ B) = indefinida
  la indefinida por una fórmula que sólo usa las conectivas ⟶ y False 
  y demostrar la equivalencia. 
  ------------------------------------------------------------------ *}

text {* --------------------------------------------------------------- 
  Ejercicio 4. Encontrar una fórmula equivalente a 
     (A ∨ (B ∧ C)) ⟷ A
  que sólo use las conectivas False, ∧ y ⟶ y demostrar la 
  equivalencia.   
  ------------------------------------------------------------------ *}

end