¿Cómo se especifica la semántica completa de SOL y HOL?

En relación con esta pregunta sobre el carácter "fundamental" de los posibles sistemas lógicos, me di cuenta de que solo tenía una comprensión intuitiva (y, por lo tanto, inadecuada) de la forma en que las lógicas superiores a FOL pueden especificar sin ambigüedades el tipo de semántica que constituye la intención . interpretación de sus formalismos, dentro de los propios formalismos . Esta es una pregunta bastante significativa, ya que la capacidad de un sistema automatizado de razonamiento en el nivel del lenguaje objeto solo puede reconocer lo que está codificado en el formalismo mismo, en ese nivel; y así, aquellos enfoques que parten de la construcción de un modelo en el meta-nivel, quedan a priori descartados en el sentido que aquí describo.

En lo que estoy pensando es en los sistemas informáticos que razonan con la lógica, como los asistentes de prueba basados ​​en HOL, como Isabelle .

Entonces, ¿cómo se especifica la semántica prevista de SOL y HOL en un sistema informático?

PD : Me he dado cuenta de que este tema no es realmente nuevo en este sitio y ha sido mencionado en otras preguntas como esta .

Consulte también el agradable artículo de descripción general de HOL "Las siete virtudes de la teoría de tipos simples" de. W. Farmer ( imps.mcmaster.ca/doc/seven-virtues.pdf )

Respuestas (3)

Desde el punto de vista de la derivabilidad y la sintaxis, no hay distinción entre la semántica completa de orden superior y la semántica de primer orden (Henkin). Esta es, en cierto sentido, la razón por la que no existe un teorema de completitud para la semántica completa, porque el teorema de completitud hace coincidir la derivabilidad con la semántica de Henkin, por lo que cualquier semántica genuinamente diferente no coincidirá con la derivabilidad. Las cosas sintácticas como los asistentes de prueba, que solo se preocupan por la derivabilidad, son algo indiferentes a los problemas semánticos.

Creo que el principal beneficio de usar lógica de orden superior en asistentes de prueba es que facilita la formalización de teoremas que han sido probados en matemáticas ordinarias. Incluso si estos teoremas pudieran formalizarse, por ejemplo, en la aritmética de Peano, mediante la creación de pruebas completamente nuevas, a menudo es más fácil modificar la prueba existente para que funcione en una lógica de orden superior.

Creo que has captado lo que estoy preguntando. En esencia, todo el concepto de "semántica completa" es lo que me preocupa. ¿Cómo puede tomarse como un término "bien definido", si las lógicas de orden superior que cumplen con la categoricidad necesitan una metateoría de FO con sabor a teoría de conjuntos para probar la categoricidad de lo que "dicen" con su "poder más expresivo"? ¿De dónde viene la "expresividad", si ha utilizado una teoría de conjuntos no categóricos para demostrarlo? Si lo hago bien, parece ser casi el mismo problema que cuando se considera el "universo estándar" de la teoría de conjuntos. ¿Es solo intuición? ¿Qué hay de "formal" en eso?
Correcto, la lógica de orden superior con semántica completa no es "formal" en ese sentido, y el tema está muy relacionado con el tema del "modelo estándar" de la teoría de conjuntos.
Muchas gracias. Esta pregunta estaba relacionada con otra que cito en el primer párrafo; el sentido de la palabra "fundamental" que usé allí es más o menos el mismo que hemos discutido aquí bajo el adjetivo "formal", excepto por el significado agregado de poder "simular" otras lógicas desde un punto de vista matemático (por ejemplo, la lógica difusa se puede formalizar en una teoría matemática de FO que admite los números reales y define la "pertenencia difusa" como un par ordenado).
Realmente agradecería si pudiera dejar una respuesta allí , porque no encontré ninguna de las actuales satisfactoria.

Hasta donde yo sé, los sistemas de prueba por computadora no se preocupan en absoluto por la semántica. Su tarea es construir y verificar pruebas formales que sigan las reglas sintácticas de lo que constituye una derivación válida, y luego depende del usuario humano convencerse de que el sistema formal corresponde a su intuición sobre la semántica.

(Bueno, algunos asistentes de prueba sí se preocupan por la semántica algunas veces, por ejemplo, si contienen procedimientos de decisión basados ​​en cálculos para teorías específicas, como campos ordenados o aritmética de Presburger. Pero luego, dependiendo del nivel de paranoia utilizado en el desarrollo -- el papel de estas partes de subpartes semánticas suele ser solo sugerir una prueba sintáctica que se puede verificar de forma independiente).

Lo que me confunde es que, incluso si su argumento es absolutamente sólido (las computadoras solo siguen reglas sintácticas y no se preocupan por la semántica), entonces parece seguir que cada lógica de orden superior a FOL se calcula necesariamente como si fuera un FOL de orden múltiple (es decir, no reconoce, por ejemplo, que las variables de segundo orden se extienden sobre subconjuntos del mismo conjunto sobre el que se extienden las variables de primer orden). Sin embargo, sospecho que me estoy perdiendo algo aquí.
@Mono: es cierto que el carácter sintáctico de la verificación de pruebas para HOL es el mismo que para un FOL ordenado por muchos. Lo que caracteriza a HOL es que normalmente hay axiomas lógicos específicos y/o reglas de inferencia que tratan con variables de orden superior y aseguran, por ejemplo, que todo lo que es definible y una fórmula explícita también se considera cuando cuantificamos una variable de orden superior de una firma adecuada. ...(continuación)
... Somos libres de considerar estas reglas especiales como parte de la teoría propiamente dicha en lugar de parte de la lógica, y el resultado sería una teoría de primer orden que podría probar lo mismo, esencialmente la teoría original de orden superior. La teoría estaría incrustada en una versión (posiblemente débil) de la teoría de conjuntos de primer orden. La posición de que toda la lógica de orden superior es solo una abreviatura de la teoría de conjuntos fue defendida por Quine, y prevaleció en gran medida hasta que el advenimiento de los sistemas prácticos de prueba por computadora dejó en claro cuán engorroso es reducir todo explícitamente a primer orden todo el tiempo.
Tenga en cuenta también que el hecho de que los axiomas lógicos para las variables de orden superior sean siempre los mismos (en contraste con si fueran solo partes incidentales de la teoría del tema) hace que sea más práctico para los desarrolladores de asistentes de prueba proporcionar estrategias generales para casos especiales. usándolos que permiten a los usuarios especificar patrones de razonamiento comunes fácilmente.
Bueno, supongo que el tipo de axiomas lógicos a los que te refieres son, por ejemplo, los axiomas de comprensión y elección en SOL. Si entendí lo que dijo, tanto SOL como HOL se pueden combinar de manera efectiva con un MS-FOL adecuado; por lo tanto, ¿podría argumentarse que la única diferencia entre estos se basa en la forma en que se formalizan las variables de "orden superior" (en el primero por comprensión, y en el segundo por la firma adecuada del modelo de clasificación múltiple, es decir, la clasificación de los aridades de funciones y relaciones)? Es que la formalización del FO es engorrosa , ¿y no hay nada más?
Además: ¿no es entonces la categoricidad absoluta (es decir, el resultado reclamado para teorías como la formalización SO de los reales bajo su semántica completa) una propiedad significativa para teorías basadas en cualquier orden lógico, si necesitamos (por ejemplo) un FO adicional? establecer un metalenguaje teórico no categórico para producir un modelo para él, que en ese momento puede demostrarse que es único en referencia a sus axiomas? O lo que equivale a la misma conclusión: ¿no es entonces sólo la categoricidad relativa una propiedad significativa de una teoría formal bajo cualquier lógica?
@Mono: No me queda claro por qué de repente estás hablando de categoricidad y modelos: esas son propiedades semánticas que no les importan a los verificadores/asistentes de pruebas. Lo único que les importa es la existencia de una prueba válida en algún sistema formal; si el sistema formal corresponde a alguna noción semántica de modelo no es su problema.
@Mono: Al igual que Henning, creo que esa es una pregunta aparte. Pero, de hecho, ha encontrado un punto clave sobre la semántica completa de segundo orden, a saber, que simplemente trasladan el problema de la categoricidad de la teoría del objeto a la metateoría. El efecto de la semántica completa es simplemente excluir de la consideración muchos de los modelos que se consideran en la lógica de primer orden. Si excluimos suficientes de ellas, las teorías que solían tener muchos modelos podrían terminar siendo categóricas, ¡o podrían no tener modelos en absoluto! Pero eso no es porque la teoría haya cambiado, es porque hemos eliminado muchos modelos posibles.
@HenningMakholm: Traje el tema de la categorización y los modelos solo porque eso es lo que quería preguntar originalmente (sobre la semántica completa de las lógicas superiores a FOL). Si la sintaxis HOL siempre es "traducible" a una sintaxis de teoría de conjuntos FO, ya sea de clasificación única como ZFC o de clasificación múltiple, como la axiomatización de clasificación doble de NBG, y entonces lo único que HOL hace es formalizar la deducción. sistemas menos engorrosos (al único costo de "mover la línea" de lo que se puede argumentar filosóficamente que es el límite entre la lógica y las matemáticas), entonces debe agregar esto a su respuesta.
@CarlMummert: todo el problema es que estoy hablando de la formalización de la semántica de una lógica dentro de ella, solo porque me parece que es la única forma significativa de afirmar la categoricidad (si es posible). En FOL eso no implica un metanivel, porque su integridad garantiza la coincidencia entre la demostrabilidad y la satisfacción por (al menos) un modelo. Pero en lógicas de orden superior, el fracaso de la completitud significa que su semántica debe considerarse necesariamente desde un metanivel; y entonces, como usted dice, la eliminación de posibles modelos debe hacerse a ese nivel.
Entonces, no puedo ver por qué la oración " SOL puede definir los reales como el único campo de Arquímedes completo hasta el isomoprismo " puede tomarse formalmente como significativa. Si escribimos una teoría SO, y luego agregamos un sistema deductivo FO aumentado con axiomas de comprensión y elección, resulta que pierde poder expresivo (y se vuelve equivalente a FOL por el teorema de Lindström ) ; pero si no incluimos esos axiomas, entonces "es categórico" y "más expresivo", pero solo cuando se le proporciona un modelo desde un metanivel y no "por sí mismo".

Quiero aclarar algo: HOL no es simplemente FOL multiordenado

La diferencia clave está en la expresividad de los dos sistemas. FOL no puede expresar un cierre transitivo. Aquí hay una buena nota que explica por qué. Por otro lado, HOL puede expresar un cierre transitivo. Aquí está el código fuente de la implementación de Isabelle/HOL si está interesado.

EDICIÓN 1 : tenga en cuenta la advertencia en los comentarios: FOL extendido con ZF o maquinaria de la aritmética puede expresar un cierre transitivo. Sin embargo, que ningún cálculo extendido pueda hacer esto no es lo que estoy afirmando aquí.

EDICIÓN 2 : Del mismo modo, es inapropiado hacer uso ciego de la intuición de la semántica de Henkin para su lógica de orden superior, ya que su aplicación a HOL basados ​​en computadora no es sencilla . Por un lado, los asistentes de prueba se basan en HOL de Church, que es anterior al trabajo de Henkin y tiene sus propias peculiaridades. La semántica para HOL de Church se puede dar usando estructuras aplicativas, según Harvey Friedman (1975) y artículos posteriores.

[¿Cómo] se especifica la semántica prevista de SOL y HOL en un sistema informático?

Realmente no puede especificar la semántica , como han señalado otros, pero hay diferentes formas en que X ∈ A se analiza en sintaxis base.

En Isabelle, puede cargar Isabelle/ZF o Isabelle/HOL. Dependiendo del sistema que cargue, X ∈ A se interpreta de otra manera.

En Isabelle/ZF, es el significado que aprendiste en la clase de teoría de conjuntos: ∈ es una relación binaria en FOL y obedece a varios axiomas de la teoría de conjuntos.

En Isabelle/HOL, S :: 'x set(es decir, " Ses un conjunto de objetos de tipo 'x") es realmente solo un envoltorio para un objeto de tipo f :: 'x -> bool(es decir, " fes una función indicadora que lleva 'xa Verdadero/Falso"). La comprensión de conjuntos y la pertenencia se definen efectivamente por la equivalencia a ∈ { X   |   PAG ( X ) } ⟺ PAG ( a ) . Puedes leer sobre esto en la fuente de Isabelle/HOL si te gustan ese tipo de cosas.

Tanto en Isabelle/ZF como en Isabelle/HOL, la sintaxis familiar { X ∈ S   |   ϕ ( X ) } también se interpreta como azúcar sintáctico. En ambos casos, es responsabilidad del analizador compilar la sintaxis extendida en la sintaxis base; y cómo se hace difiere según la base.

Finalmente, mientras que los asistentes de prueba por computadora generalmente no están acostumbrados a razonar sobre su propia semántica, hay una excepción. John Harrison desarrolló dos pruebas de consistencia relativa de HOL-Light dentro de HOL-Light aquí .

Primero demuestra cómo construir un modelo completo de HOL-Light sin el axioma del infinito en HOL-Light. Luego muestra cómo construir un modelo completo de todo HOL-Light en HOL-Light extendido con un cardenal fuertemente inaccesible.

La afirmación "FOL no puede expresar el cierre transitivo" es algo vaga. ZFC ciertamente puede definir el cierre transitivo de una relación y es una teoría de primer orden. Cualquier cosa que pueda expresarse en HOL puede expresarse, exactamente con la misma oración, en FOL. La única diferencia está en la semántica, pero HOL tiene varias semánticas, la más débil de las cuales tiene la misma fuerza que FOL. Todo lo que hace Isabelle es compatible con esta semántica; Isabelle no tiene forma de saber qué semántica uso para interpretar su salida. Si uso la semántica de Henkin, Isabelle tendrá las mismas limitaciones semánticas que FOL.
@Carl Mummert: Supongo que debería hacer una distinción. Mientras que en ZF puede expresar el cierre transitivo de una relación entre conjuntos, no puede expresar el cierre de relaciones lógicas como en ∈ ; FOL no puede hacer eso. Por otro lado, Isabelle/HOL no tiene este problema. Asimismo, Isabelle/HOL no solo codifica el cálculo de orden superior de Henkin; también incluye extensiones como el axioma de elección. Isabelle/HOL se puede incrustar en ZFC, pero no es lo mismo ser incrustable en FOL simpliciter (como el cálculo de orden superior de Henkin).
El método de Henkin funciona con axiomas de elección y comprensión arbitrarios añadidos; de hecho, estos se usan típicamente en la lógica de segundo orden, incluso con la semántica de Henkin. Además, ciertamente es posible expresar, dentro de ZFC, el cierre transitivo de un conjunto o clase arbitraria A bajo la ∈ relación: un conjunto b está en la clausura transitiva de A si y solo si hay una cadena finita b ∈ a norte + 1 ∈ a norte ∈ ⋯ ∈ a 1 dónde a 1 ∈ A . Eso se puede escribir como una sola oración de ZFC.
(Esa es la clausura transitiva en el sentido de la teoría de conjuntos. Para la clausura transitiva en el sentido de la teoría del orden, pondríamos b ∈ ∗ a si hay una cadena finita b ∈ a norte + 1 ∈ ⋯ ∈ a 1 = a dónde a norte + 1 , a norte , … , a 1 están todos en A . Esta es nuevamente una sola oración de ZFC. En general, si podemos definir la clausura transitiva de cualquier relación R entonces podemos definir la clausura transitiva de ∈ simplemente reemplazando R con ∈ en la definición).
@Carl Mummert: Bien, ahora que me desperté un poco, veo tu definición de cierre de ∈ es correcto. De todos modos, los asistentes informáticos de HOL no tienen axiomas de comprensión. Además, tienen términos lambda; son una tradición diferente de las cosas de lápiz y papel de Henkin. Realmente no veo cuál es el algoritmo para incrustar HOL de computadora en FOL de clasificación múltiple; tal vez usted puede dar una cita?
Creo que el problema es que FOL no es una sola lógica. Hay muchas lógicas de "primer orden" con sintaxis ligeramente diferente. Todos son de primer orden en el sentido de que tienen sistemas deductivos efectivos, semántica que utiliza estructuras ordinarias de primer orden y teoremas de completitud. El FOL que la gente suele ver primero no tiene tipos, λ términos o cuantificadores establecidos, pero estos son fáciles de agregar mientras se preserva la integridad. Generalmente λ los términos solo se ven en la teoría de la prueba o en entornos computacionales, por ejemplo, en la aritmética de orden superior, como en la Teoría de prueba aplicada de Kohlenbach .
Bien; Los asistentes a prueba de HOL se basan en la formulación anterior de Church anterior a la de Henkin. Parece que una incrustación de HOL de Church en FOL exige incrustar el álgebra de términos de HOL, por lo que tendría que introducir una @aplicación representada por operación binaria polimórfica. Parece que Harvey Friedman resolvió esto en los años 70. No hace falta decir que no creo que la intuición del HOL de Henkin sea directamente aplicable a los HOL basados ​​en computadora. Obtuve la mayor parte de esto después de hojear esta tesis de maestría: ps.uni-saarland.de/theses/kaminski/mthesis/kaminski-mthesis.pdf
¿Cómo se especifica la semántica completa de SOL y HOL?
RespuestasAquíPolítica de privacidad1y, 0v