header {* 1ª relación de ejercicios *}
theory Relacion_1
imports Main
begin
text {*
---------------------------------------------------------------------
Demostrar los siguientes lemas usando sólo las reglas básicas de
deducción natural de la lógica proposicional.
---------------------------------------------------------------------
*}
lemma I: "A ⟶ A"
oops
lemma "A ∧ B ⟶ B ∧ A"
oops
lemma "A ∧ B ⟶ A ∨ B"
oops
lemma "(A ∨ B) ∨ C ⟶ A ∨ (B ∨ C)"
oops
lemma K: "A ⟶ (B ⟶ A)"
oops
lemma S: "(A ⟶ (B ⟶ C)) ⟶ ((A ⟶ B) ⟶ (A ⟶ C))"
oops
lemma "(A ⟶ B) ⟶ ((B ⟶ C) ⟶ (A ⟶ C))"
oops
lemma "¬¬A ⟶ A"
oops
lemma "A ⟶ ¬¬A"
oops
lemma "(¬A ⟶ B) ⟶ (¬B ⟶ A)"
oops
lemma "((A ⟶ B) ⟶ A) ⟶ A"
oops
lemma "A ∨ ¬A"
oops
lemma "(¬(A ∧ B)) = (¬A ∨ ¬B)"
oops
end
