Autor Tema: Demostración aplicativa Isabelle

0 Usuarios y 1 Visitante están viendo este tema.

15 Abril, 2021, 10:26 am
Leído 335 veces

Bobby Fischer

  • $$\Large \color{#c88359}\pi\,\pi\,\pi\,\pi$$
  • Mensajes: 646
  • País: es
  • Karma: +1/-0
  • Sexo: Masculino
    • chess.com
Hola, ¿puede alguien ayudarme a probar esto en Isabelle?

Gracias,

Saludos.

lemma "Prueba":
 "⟦∀x. (P x ⟶ Q x); ∃x. P x ⟧ ⟹ ∃x. Q x"
  apply (rule exI)
  apply (rule mp)
   apply (erule allE)
   apply (erule exE)
   apply assumption

15 Abril, 2021, 05:42 pm
Respuesta #1

geómetracat

  • Moderador Global
  • Mensajes: 2,350
  • País: es
  • Karma: +0/-0
  • Sexo: Masculino
¿Qué tal algo así?

lemma "Prueba":  "⟦∀x. (P x ⟶ Q x); ∃x. P x ⟧ ⟹ ∃x. Q x"
  apply (erule exE)
  apply (erule_tac x="x" in allE)
  apply (rule exI)
  apply (erule mp)
  apply assumption

Es la primera vez que uso Isabelle, así que no sé si es lo más óptimo.
La idea es la siguiente: la primera línea elimina el existencial en la premisa \[ \exists x Px \] para obtener \[ Px \] como premisa. La segunda línea elimina el cuantificador universal en \[ \forall x (Px\to Qx) \] y obtienes como premisa \[ Px \to Qx \] (fíjate que es esencial que aquí estamos instanciando con la misma variable que el \[ Px \] que hemos obtenido antes). La tercera línea permite pasar de probar \[ \exists x Qx \] a probar \[ Qa \] para alguna variable \[ a \]. Y finalmente las últimas dos líneas prueban \[ Qx \] a partir de las premisas \[ Px \to Qx \] y \[ Px \] usando modus ponens.
La ecuación más bonita de las matemáticas: \( d^2=0 \)