Estoy leyendo el artículo de Wikipedia sobre la Deducción Natural. En la sección 6, la presentación de intr y elim reglas para los cuantificadores universal y existencial, se menciona un concepto llamado eigenvariable/parámetro sin más discusión. ¿Qué es? ¿Cuál es la diferencia entre el eigenvariable/parámetro $a$ y la variable vinculada $x$ introducido por $\forall$ o $\exists$? ¿Qué es y para que sirve? El lado de las condiciones para la $\forall$ intr y $\exists$ elim reglas también me desconcertó. Alguien podría explicar un poco más? Gracias.
Respuestas
¿Demasiados anuncios?
carmas
Puntos
11
El eigenvariable la condición se utiliza cuando se quieren introducir la forall conector.
Si desea introducir forall una, entonces usted necesita para asegurarse de que no es libre como en los supuestos. Por lo tanto, usted puede ser obligado a cambiar el nombre de un libre una de las hipótesis con nuevo nombre.
En http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.94.9463&rep=rep1&type=pdf por Alwen Tiu se puede leer :
En la prueba de búsqueda de un universal cuantificado fórmula, por ejemplo, ∀x.Bx, la cuantificado la variable x se sustituye por una nueva constante c, y la prueba de búsqueda se continúa en la Bc. Estas constantes se llaman eigenvariables, y en la tradicional intuitionistic o la lógica clásica, juegan el papel de ámbito constantes como son creado dinámicamente como prueba de búsqueda avanza y no se crean instancias durante la prueba de búsqueda.
Vea la página 2 para obtener más detalles
La costumbre de la formalización de la lógica de primer orden necesita distinguir entre las letras que representan las cosas que puede ser sustituido por cualquier término y las letras que corresponden a condiciones particulares. El eigenvariables son el segundo tipo de letra, que no puede ser sustituido en el forall-intro / existe-elim reglas.
Este es un concepto difícil cuando el aprendizaje de la lī ogica y el movimiento de deducción natural tiene la capacidad de confundir las cosas aún más. Para conseguir una manija en las reglas de inferencia, la mayoría de las personas se encuentran con la necesidad de ser un poco formalista, acerca de la distinción, la visualización de la distinción como un marcador sintáctico diciendo que son las hojas de una fórmula que puede ser sustituido. Pero en este formalista nivel, usted realmente no comprender el por qué de la misma.
La clave es que los dos tipos de letra puede ser visto de variables que se derivan de su significado, que en la sentencia se expresa en ese punto de la derivación. La semántica de las variables tiene su obligados, con los habituales de variables universalmente cuantificado y eigenvariables ser existencialmente cuantificadas. Las constantes entonces son equivalentes a las constantes de Skolem que surgen de la Skolemisation de la fórmula que expresan el juicio.
El de arriba es complicado, y correctamente agarrar requiere que (i) se siente cómodo con la aplicación de Skolemisation (ver Wikipedia en Skolem formas normales para un decente discusión), y (ii) determinar cómo se aplican a expresar el criterio en cada fórmula en una deducción natural de la prueba. Pero entonces, esto no es más que la complejidad de variables y constantes en la lógica de primer orden.
Sería bueno recomendar un texto que cubre esta tierra, pero ninguno a la mente.
