Razonamiento automático (2010-11) Razonamiento automático (2010-11)

En esta teoría se presenta una formalización en Isabelle/Isar de los ejemplos del tema de deducción natural proposicional siguiendo la presentación de Huth y Ryan en su libro Logic in Computer Science y, más concretamente, a la forma como se explica en la asignatura de Lógica informática y que puede verse en las transparencias del tema 7.

La páginas en los teorema indican la página de las anteriores transparencias donde se encuentra la demostración.

header {* Deducción natural en la lógica de primer orden *}

theory LogicaDePrimerOrden
imports Main 
begin

section {* Reglas del cuantificador universal *}

text {*
  La regla de eliminación del cuantificador universal es
  · allI: ⟦∀x. P x; P x ⟹ R⟧ ⟹ R
  La regla de introducción del cuantificador universal es
  · allE: (⋀x. P x) ⟹ ∀x. P x
*}

lemma -- "p. 10"
  assumes 1: "P(c)" and 
          2: "∀x. P(x) ⟶ ¬Q(x)" 
  shows "¬Q(c)"
proof (rule notI)
  assume 3: "Q(c)"
  have "P(c) ⟶ ¬Q(c)" using 2 by (rule allE)
  hence "¬Q(c)" using 1 by (rule mp)
  thus False using 3 by (rule notE)
qed 

lemma -- "p. 11"
  assumes 1: "∀x. P(x) ⟶ Q(x)" and  
          2: "∀x. P(x)" 
  shows "∀x. Q(x)"
proof (rule allI)
  fix x
  have 3: "P(x) ⟶ Q(x)" using 1 by (rule allE)
  have 4: "P(x)" using 2 by (rule allE)
  show "Q(x)" using 3 4 by (rule mp)
qed

section {* Reglas del cuantificador existencial *}

text {*
  La regla de eliminación del cuantificador existencial es
  · exI: P x ⟹ ∃x. P x
  La regla de introducción del cuantificador existencial es
  · exE: ⟦∃x. P x; ⋀x. P x ⟹ Q⟧ ⟹ Q
*}

lemma -- "p. 12"
  assumes 1: "∀x. P(x)" 
  shows "∃x. P(x)"
proof -
  have 2: "P(x)" using 1 by (rule allE)
  show "∃x. P(x)" using 2 by (rule exI)
qed

lemma -- "p. 12"
  assumes 1: "∀x. P(x)" 
  shows "∃x. P(x)"
proof (rule exI) 
  show "P(x)" using 1 by (rule allE)
qed

lemma -- "p. 12"
  assumes 1: "∀x. P(x)" 
  shows "∃x. P(x)"
proof 
  show "P(x)" using 1 ..
qed

lemma -- "p. 13"
  assumes 1: "∀x. P(x) ⟶ Q(x)" and  
          2: "∃x. P(x)" 
  shows "∃x. Q(x)"
proof -
  obtain "a" where 3: "P(a)" using 2 by (rule exE)
  have 4: "P(a) ⟶ Q(a)" using 1 by (rule allE)
  have 5: "Q(a)" using 4 3 by (rule mp)
  show "∃x. Q(x)" using 5 by (rule exI)
qed

lemma 
  assumes 1: "∀x. Q(x) ⟶ R(x)" and  
          2: "∃x. P(x) ∧ Q(x)" 
  shows "∃x. P(x) ∧ R(x)"
proof -
  obtain x where 3: "P(x) ∧ Q(x)" using 2 by (rule exE)
  have 5: "P(x)" using 3 by (rule conjunct1)
  have 6: "Q(x) ⟶ R(x)" using 1 by (rule allE)
  have 7: "Q(x)" using  3 by (rule conjunct2)
  have 8: "R(x)" using 6 7 by (rule mp)
  have 9: "P(x) ∧ R(x)" using 5 8 by (rule conjI)
  show "∃x. P(x) ∧ R(x)" using 9 by (rule exI)
qed

lemma 
  assumes 1: "∃x. P(x)" and  
          2: "∀x.∀y. P(x) ⟶ Q(y)" 
  shows "∀y. Q(y)"
proof (rule allI)
  fix y
  obtain x where 3: "P(x)" using 1 by (rule exE)
  have 4: "∀y. P(x) ⟶ Q(y)" using 2 by (rule allE)
  have 5: "P(x) ⟶ Q(y)" using 4 by (rule allE)
  show "Q(y)" using 5 3 by (rule mp)
qed

section {* Equivalencias *}

-- "p. 15"
lemma equivalencia_1a1:
  assumes 1: "¬(∀x. P(x))"
  shows "∃x. ¬P(x)"
proof (rule ccontr)
  assume 2: "¬(∃x. ¬P(x))"
  note 1
  thus False
  proof (rule notE)
    show "∀x. P(x)"
    proof (rule allI)
      fix x
      show "P(x)"
      proof (rule ccontr)
        assume 3: "¬P(x)"
        have 4: "∃x. ¬P(x)" using 3 by (rule exI)
        show False using 2 4 by (rule notE)
      qed
    qed
  qed
qed

-- "p. 16"
lemma equivalencia_1a2:
  assumes 1: "∃x. ¬P(x)" 
  shows "¬(∀x. P(x))"
proof (rule ccontr)
  assume 2: "¬¬(∀x. P(x))"
  obtain x where 3: "¬P(x)" using 1 by (rule exE)
  have 4: "∀x. P(x)" using 2 by (rule notnotD)
  have 5: "P(x)" using 4 by (rule allE)
  show False using 3 5 by (rule notE)
qed

-- "p. 17"
theorem equivalencia_1a:
  "(¬(∀x. P(x))) = (∃x. ¬P(x))"
proof (rule iffI)
  { assume "¬(∀x. P x)"
    thus "∃x. ¬P x" by (rule equivalencia_1a1)}
next
  { assume "∃x. ¬P x"
    thus "¬(∀x. P x)" by (rule equivalencia_1a2) }
qed

-- "p. 18"
lemma equivalencia_3a1:
  assumes 1: "∀x. P(x) ∧ Q(x)" 
  shows "(∀x. P(x)) ∧ (∀x. Q(x))"
proof (rule conjI)
  show "∀x. P(x)"
  proof (rule allI)
    fix x
    have 2: "P(x) ∧ Q(x)" using 1 by (rule allE)
    show "P(x)" using 2 by (rule conjunct1) 
  qed
next
  show "∀x. Q(x)"
  proof (rule allI)
    fix x
    have 3: "P(x) ∧ Q(x)" using 1 by (rule allE)
    show "Q(x)" using 3 by (rule conjunct2)
  qed
qed

-- "p. 19"
lemma equivalencia_3a2:
  assumes 1: "(∀x. P(x)) ∧ (∀x. Q(x))" 
  shows "∀x. P(x) ∧ Q(x)"
proof (rule allI)
  fix x
  have 2: "∀x. P(x)" using 1 by (rule conjunct1)
  have 3: "∀x. Q(x)" using 1 by (rule conjunct2)
  have 4: "P(x)" using 2 by (rule allE)
  have 5: "Q(x)" using 3 by (rule allE)
  show "P(x) ∧ Q(x)" using 4 5 by (rule conjI)
qed

-- "p. 20" 
lemma equivalencia_3a:
  "(∀x. P(x) ∧ Q(x)) = ((∀x. P(x)) ∧ (∀x. Q(x)))"
proof (rule iffI)
  { assume "∀x. P(x) ∧ Q(x)"
    thus "(∀x. P(x)) ∧ (∀x. Q(x))" by (rule equivalencia_3a1) }
next
  { assume "(∀x. P(x)) ∧ (∀x. Q(x))"
    thus "∀x. P(x) ∧ Q(x)" by (rule equivalencia_3a2) }
qed

-- "p. 21"
lemma equivalencia_3b1: 
  assumes 1: "(∃x. P(x)) ∨ (∃x. Q(x))" 
  shows "∃x. P(x) ∨ Q(x)"
using 1
proof (rule disjE)
  { assume "∃x. P(x)"
    then obtain x where "P(x)" by (rule exE)
    hence "P(x) ∨ Q(x)" by (rule disjI1)
    thus "∃x. P(x) ∨ Q(x)" by (rule exI) }
next
  { assume "∃x. Q(x)"
    then obtain x where "Q(x)" by (rule exE)
    hence "P(x) ∨ Q(x)" by (rule disjI2)
    thus "∃x. P(x) ∨ Q(x)" by (rule exI) }
qed

-- "p. 22"
lemma equivalencia_3b2:
  assumes 1: "∃x. P(x) ∨ Q(x)" 
  shows "(∃x. P(x)) ∨ (∃x. Q(x))"
proof -
  obtain x where 2: "P(x) ∨ Q(x)" using 1 by (rule exE)
  thus "(∃x. P(x)) ∨ (∃x. Q(x))"
  proof (rule disjE)
    { assume "P(x)"
      hence "∃x. P(x)" by (rule exI)
      thus "(∃x. P(x)) ∨ (∃x. Q(x))" by (rule disjI1) }
  next
    { assume "Q(x)"
      hence "∃x. Q(x)" by (rule exI)
      thus "(∃x. P(x)) ∨ (∃x. Q(x))" by (rule disjI2) }
  qed
qed

-- "p. 23"
lemma equivalencia_3b:
  "((∃x. P(x)) ∨ (∃x. Q(x))) = (∃x. P(x) ∨ Q(x))"
proof (rule iffI)
  { assume "(∃x. P(x)) ∨ (∃x. Q(x))"
    thus "∃x. P(x) ∨ Q(x)" by (rule equivalencia_3b1) }
next
  { assume "∃x. P(x) ∨ Q(x)"
    thus "(∃x. P(x)) ∨ (∃x. Q(x))" by (rule equivalencia_3b2) }
qed

-- "p. 24"
lemma equivalencia_4b1:
  assumes 1: "∃x.∃y. P x y" 
  shows "∃y.∃x. P x y"
proof -
  obtain x where "∃y. P x y" using 1 by (rule exE)
  then obtain y where "P x y" by (rule exE)
  hence "∃x. P x y" by (rule exI)
  thus "∃y.∃x. P x y" by (rule exI)
qed

-- "p. 25"
theorem equivalencia_4b:
  "(∃x.∃y. P x y) = (∃y.∃x. P x y)"
proof (rule iffI)
  { assume "∃x.∃y. P x y"
    thus "∃y.∃x. P x y" by (rule equivalencia_4b1) }
next
  {assume "∃y.∃x. P x y"
    thus "∃x.∃y. P x y" by (rule equivalencia_4b1) }
qed

end