Uso de teoremas en la deducción natural

Uso de teoremas en la deducción natural

de Jerónimo Ismael Acosta Monteavaro -
Número de respuestas: 4

Hola, me estaba preguntando si no existirá alguna forma de utilizar teoremas previamente demostrados en la construcción de los árboles. Quiero decir, si por ejemplo yo estuviera demostrando algo en geometría, podría detener mi demostración en el teorema de Pitágoras, asumirlo como un hecho, ya que se conoce la existencia de demostraciones para el teorema.
Entonces ¿Cómo podría hacer algo similar con la deducción natural? ¿Cómo sería específicamente la notación para algo así?
Serviría copiar y pegar en su lugar correspondiente al árbol de la demostración del teorema en cuestión, pero busco una forma de impedir precisamente eso, para así poder mejorar la prolijidad y evitarme problemas con los tamaños.
Otra pregunta: en caso de que efectivamente se pueda hacer algo del estilo ¿Puedo usarlo en un parcial? Y ¿Podría dar como demostrado un teorema que se vio en el curso, y así ahorrarme su demostración en el parcial? Por ejemplo, que no-no-Alfa implica Alfa, cosa que veo que se usa bastante y está demostrado como ejemplo en las diapositivas.

En respuesta a Jerónimo Ismael Acosta Monteavaro

Re: Uso de teoremas en la deducción natural

de Fernando Carpani -
Hola.
A ver...
 
Componer árboles es algo que se usa bastante en el curso. La sintaxis que se usa es la del "triangulito" con una fórmula abajo. Eso se usa en la presentación de las reglas:
Composición de derivaciones
 
Con respecto a usarlo en una evaluación, se puede siempre y cuando sea un uso claro, de una derivación que aparece en el parcial también. Esa derivación puede aparecer en otro ejercicio o parte, o la podés hacer para simplificarte algo dentro del mismo ejercicio.
Como consejo, usá la hoja apaisada sólo para las derivaciones. El resto lo hacés con la hoja vertical.
Con respecto al uso de "derivaciones conocidas", no se pueden usar. No hay derivaciones conocidas en el curso.
En las evaluaciones, las derivaciones que entreguen, deben:
  • Estar completas, desde sus hipótesis hasta su conclusión, exponiendo las cancelaciones con los índices correspondientes que referencian contra qué regla cancelan.
  • Presentar el nombre de cada regla.
  • El orden de los sub-árboles es importante. No es lo mismo poner una sub-derivación a la izquierda que a la derecha. Son derivaciones distintas, una de ellas podría estar incorrecta.
  • Las reglas de eliminación deben tener la fórmula que se está eliminando en su árbol de más a la izquierda.
  • En la introducción del "si y solo si", la primer sub-derivación (la de la izquierda) refleja la implicación que va de izquierda a derecha (el "directo") y la otra sub-derivación, refleja el "recíproco".
 
Te aconsejo que leas los documentos que usamos para la clase del teórico que deberían estar todos publicados. Y cualquier otra duda, preguntá de nuevo.
 
Saludos
Adjunto CompDeriv.png
En respuesta a Fernando Carpani

Re: Uso de teoremas en la deducción natural

de Jerónimo Ismael Acosta Monteavaro -
Bueno, de hecho me surgió otra duda:
Supongamos que ya tengo un árbol que demuestra cierta consecuencia sintáctica, en el caso particular del que salió mi duda, sería la siguiente

Entonces, como parte de otra demostración, lo utilicé de esta manera:

Si no te entendí mal, esa notación de utilizar el triángulo adentro de un árbol es correcta ¿No? Además de confirmarlo, quería saber si es correcto dar como sobreentendido que ahí Fi y no-Psi juegan el papel de los Alfa y Beta que se usaron para demostrar la derivación, o si debería especificarlo de alguna forma; quizá debería hacer una nueva derivación que use específicamente Fi y no-Psi para que sea válido, no estoy seguro.
En respuesta a Jerónimo Ismael Acosta Monteavaro

Re: Uso de teoremas en la deducción natural

de Fernando Carpani -
Hola.
Si...
Yo creo que es correcto lo que decís.

No es usual que lo veamos, pero es correcto.

Lo que si la derivación D1, no la tenes que tener hecha por allí. Típicamente, de una parte de un ejercicio, o se da como una hipótesis, etc...
No hay Derivaciones Conocidas, como si hay Equivalencias Conocidas.

Habría, por una cuestión de claridad y para simplificar la corrección, aclarar que es la derivación D1 en donde se sustituyó \alpha por \varphi y a \beta por \neg \psi...

Sólo por eso.
Saludos
FDO.