theory Relacion_9
imports Main
begin
section {* Deducción natural proposicional *}
text {* Los ejercicios de esta relación deben de resolverse usando sólo
las reglas básicas de la deducción natural proposicional:
· conjI: ⟦P; Q⟧ ⟹ P ∧ Q
· conjunct1: P ∧ Q ⟹ P
· conjunct2: P ∧ Q ⟹ Q
· notnotD: ¬¬ P ⟹ P
. notnotI: P ⟹ ¬¬ P
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q
· mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F
· impI: (P ⟹ Q) ⟹ P ⟶ Q
· disjI1: P ⟹ P ∨ Q
· disjI2: Q ⟹ P ∨ Q
· disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R
· FalseE: False ⟹ P
· notE: ⟦¬P; P⟧ ⟹ R
· notI: (P ⟹ False) ⟹ ¬P
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
· iffD1: ⟦Q = P; Q⟧ ⟹ P
· iffD2: ⟦P = Q; Q⟧ ⟹ P
· ccontr: (¬P ⟹ False) ⟹ P
*}
lemma notnotI: "P ⟹ ¬¬ P"
by auto
lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto
lemma ejercicio_1:
assumes 1: "p ⟶ q" and
2: "p"
shows "q"
oops
lemma ejercicio_2:
assumes 1: "p⟶q" and
2: "q⟶r" and
3: "p"
shows "r"
oops
lemma ejercicio_3:
assumes 1: "p⟶(q⟶r)" and
2: "p⟶q" and
3: "p"
shows "r"
oops
lemma ejercicio_4:
assumes 1: "p⟶q" and
2: "q⟶r"
shows "p⟶r"
oops
lemma ejercicio_5:
"p⟶(q⟶r) ⟹ q⟶(p⟶r)"
oops
lemma ejercicio_6:
"p⟶(q⟶r) ⟹ (p⟶q)⟶(p⟶r)"
oops
lemma ejercicio_7:
"p ⟹ q⟶p"
oops
lemma ejercicio_8:
"p⟶(q⟶p)"
oops
lemma ejercicio_9:
"p⟶q ⟹ (q⟶r)⟶(p⟶r)"
oops
lemma ejercicio_10:
"p⟶(q⟶(r⟶s)) ⟹ r⟶(q⟶(p⟶s))"
oops
lemma ejercicio_11:
"(p⟶(q⟶r))⟶((p⟶q)⟶(p⟶r))"
oops
lemma ejercicio_12:
"(p⟶q)⟶r ⟹ p⟶(q⟶r)"
oops
lemma ejercicio_13:
"⟦p; q⟧ ⟹ p∧q"
oops
lemma ejercicio_14:
"p∧q ⟹ p"
oops
lemma ejercicio_15:
"p∧q ⟹ q"
oops
lemma ejercicio_16:
"p∧(q∧r) ⟹ (p∧q)∧r"
oops
lemma ejercicio_17:
"(p∧q)∧r ⟹ p∧(q∧r)"
oops
lemma ejercicio_18:
"p∧q ⟹ p⟶q"
oops
lemma ejercicio_19:
"(p⟶q)∧(p⟶r) ⟹ p⟶q∧r"
oops
lemma ejercicio_20:
"p⟶q∧r ⟹ (p⟶q)∧(p⟶r)"
oops
lemma ejercicio_21:
"p⟶(q⟶r) ⟹ p∧q⟶r"
oops
lemma ejercicio_22:
"p∧q⟶r ⟹ p⟶(q⟶r)"
oops
lemma ejercicio_23:
"(p⟶q)⟶r ⟹ p∧q⟶r"
oops
lemma ejercicio_24:
"p∧(q⟶r) ⟹ (p⟶q)⟶r"
oops
lemma ejercicio_25:
"p ⟹ p∨q"
oops
lemma ejercicio_26:
"q ⟹ p∨q"
oops
lemma ejercicio_27:
"p∨q ⟹ q∨p"
oops
lemma ejercicio_28:
"q⟶r ⟹ p∨q⟶p∨r"
oops
lemma ejercicio_29:
"p∨p ⟹ p"
oops
lemma ejercicio_30:
"p ⟹ p∨p"
oops
lemma ejercicio_31:
"p∨(q∨r) ⟹ (p∨q)∨r"
oops
lemma ejercicio_32:
"(p∨q)∨r ⟹ p∨(q∨r)"
oops
lemma ejercicio_33:
"p∧(q∨r) ⟹ (p∧q)∨(p∧r)"
oops
lemma ejercicio_34:
"(p∧q)∨(p∧r) ⟹ p∧(q∨r)"
oops
lemma ejercicio_35:
"p∨(q∧r) ⟹ (p∨q)∧(p∨r)"
oops
lemma ejercicio_36:
"(p∨q)∧(p∨r) ⟹ p∨(q∧r)"
oops
lemma ejercicio_37:
"(p⟶r)∧(q⟶r) ⟹ p∨q⟶r"
oops
lemma ejercicio_38:
"p∨q⟶r ⟹ (p⟶r)∧(q⟶r)"
oops
lemma ejercicio_39:
"p ⟹ ¬¬p"
oops
lemma ejercicio_40:
"¬p ⟹ p⟶q"
oops
lemma ejercicio_41:
"p⟶q ⟹ ¬q⟶¬p"
oops
lemma ejercicio_42:
"⟦p∨q; ¬q⟧ ⟹ p"
oops
lemma ejercicio_43:
"⟦p∨q; ¬p⟧ ⟹ q"
oops
lemma ejercicio_44:
"p∨q ⟹ ¬(¬p∧¬q)"
oops
lemma ejercicio_45:
"p∧q ⟹ ¬(¬p∨¬q)"
oops
lemma ejercicio_46:
"¬(p∨q) ⟹ ¬p∧¬q"
oops
lemma ejercicio_47:
"¬p∧¬q ⟹ ¬(p∨q)"
oops
lemma ejercicio_48:
"¬p∨¬q ⟹ ¬(p∧q)"
oops
lemma ejercicio_49:
"¬(p∧¬p)"
oops
lemma ejercicio_50:
"p∧¬p ⟹ q"
oops
lemma ejercicio_51:
"¬¬p ⟹ p"
oops
lemma ejercicio_52:
"p∨¬p"
oops
lemma ejercicio_53:
"((p⟶q)⟶p)⟶p"
oops
lemma ejercicio_54:
"¬q⟶¬p ⟹ p⟶q"
oops
lemma ejercicio_55:
"¬(¬p∧¬q) ⟹ p∨q"
oops
lemma ejercicio_56:
"¬(¬p∨¬q) ⟹ p∧q"
oops
lemma ejercicio_57:
"¬(p∧q) ⟹ ¬p∨¬q"
oops
lemma ejercicio_58:"(p⟶q)∨(q⟶p)"
oops
end
