Diferencia entre revisiones de «Lógica de orden superior»
Página creada con «En matemáticas y lógica, una '''lógica de orden superior''' (abreviada LOS) es una forma de lógica de predicados que se distingue de la lógica de primer orden por cuantificadores adicionales y, a veces, semántica de lógica. Las lógicas de orden superior con su semántica estándar son más expresivas, pero sus propiedades son menos adecuadas que las de la lógica de primer orden desde la perspectiva de la teoría de mode…» Etiqueta: Enlaces a desambiguaciones |
(Sin diferencias)
|
Revisión del 20:03 3 ago 2023
En matemáticas y lógica, una lógica de orden superior (abreviada LOS) es una forma de lógica de predicados que se distingue de la lógica de primer orden por cuantificadores adicionales y, a veces, semántica de lógica. Las lógicas de orden superior con su semántica estándar son más expresivas, pero sus propiedades son menos adecuadas que las de la lógica de primer orden desde la perspectiva de la teoría de modelos.
El término "lógica de orden superior" se usa comúnmente para significar lógica de predicados simples de orden superior. Aquí "simple" indica que la teoría de tipos subyacente es la "teoría de tipos simples", también llamada "teoría simple de tipos". Leon Chwistek y Frank P. Ramsey propusieron esto como una simplificación de la complicada y torpe "teoría ramificada de tipos" especificada en los "Principia Mathematica" de Alfred North Whitehead y Bertrand Russell. A veces también se pretende excluir los tipos polimórfico y [[tipo dependiente|dependiente].[1]
Alcance de la cuantificación
La lógica de primer orden cuantifica solo variables que varían sobre individuos; lógica de segundo orden, además, también cuantifica sobre conjuntos; La lógica de tercer orden también cuantifica sobre conjuntos de conjuntos, y así sucesivamente.
La lógica de orden superior es la unión de la lógica de primer, segundo, tercero-, ..., de orden n); "Es decir", la lógica de orden superior admite la cuantificación sobre conjuntos que están anidados arbitrariamente profundamente.
Semántica
Hay dos semánticas posibles para la lógica de orden superior.
En el "estándar" o "semántica completa", los cuantificadores sobre objetos de tipo superior abarcan "todos" los objetos posibles de ese tipo. Por ejemplo, un cuantificador sobre conjuntos de individuos abarca todo el conjunto de potencias del conjunto de individuos. Por lo tanto, en semántica estándar, una vez que se especifica el conjunto de individuos, esto es suficiente para especificar todos los cuantificadores. LOS con semántica estándar es más expresivo que la lógica de primer orden. Por ejemplo, las LOS admiten axiomatizaciones del teorema de categoricidad de Morley de los números naturales y de los números reales, que son imposibles con la lógica de primer orden. Sin embargo, por un resultado de Kurt Gödel, LOS con semántica estándar no admite una efectiva, sonido, y completo cálculo de prueba.[2] Las propiedades de la teoría del modelo de LOS con semántica estándar también son más complejas que las de la lógica de primer orden. Por ejemplo, el número de Löwenheim de lógica de segundo orden ya es mayor que el primer cardinal medible, si tal cardinal existe.[3] El número de Löwenheim de lógica de primer orden, en contraste, es א0, el cardinal infinito más pequeño.
En la semántica de Henkin, se incluye un dominio separado en cada interpretación para cada tipo de orden superior. Así, por ejemplo, los cuantificadores sobre conjuntos de individuos pueden variar solo sobre un subconjunto del conjunto de potencias del conjunto de individuos. LOS con esta semántica es equivalente a la lógica de primer orden de muchos ordenes, en lugar de ser más fuerte que la lógica de primer orden. En particular, LOS con semántica de Henkin tiene todas las propiedades teóricas de modelos de la lógica de primer orden, y tiene un sistema de prueba completo, sólido y efectivo heredado de la lógica de primer orden.
Propiedades
Las lógicas de orden superior incluyen las ramificaciones de Church's teoría simple de tipos[4] y las diversas formas de teoría intuicionista de tipos. Gérard Huet ha demostrado que unifibilidad es indecidible en un sabor de lógica de tercer orden teoría de tipos, [5][6][7][8] es decir, no puede haber ningún algoritmo para decidir si una ecuación arbitraria entre términos de segundo orden (y mucho menos arbitrarios de orden superior) tiene una solución.
Hasta una cierta noción de isomorfismo, la operación del conjunto de potencias es definible en lógica de segundo orden. Usando esta observación, Jaakko Hintikka estableció en 1955 que la lógica de segundo orden puede simular lógicas de orden superior en el sentido de que para cada fórmula de una lógica de orden superior, uno puede encontrar una fórmula de equisatisfacibilidad | equisatisfacible para ella en lógica de segundo orden http://plato.stanford.edu/entries/logic-higher-order/#4><.Entrada SEP en LOS]</ref>
El término "lógica de orden superior" se asume en algún contexto para referirse a la lógica de orden superior "clásica". Sin embargo, también se ha estudiado la lógica de orden superior modal. Según varios lógicos, La prueba ontológica de Gödel se estudia mejor (desde una perspectiva técnica) en tal contexto.[9]
Véase también
- Lógica de orden cero (lógica proposicional)
Referencias
- ↑ Jacobs, 1999, capítulo 5
- ↑ Shapiro 1991, p. 87.
- ↑ Menachem Magidor y Jouko Väänänen. "On Löwenheim-Skolem-Tarski numbers for extensions of first order logic", Informe No. 15 (2009/2010) del Instituto Mittag-Leffler.
- ↑ Alonzo Church, Una formulación de la teoría simple de tipos, The Journal of Symbolic Logic 5(2):56–68 (1940)
- ↑ Plantilla:Citar diario
- ↑ Plantilla:Citar tesis
- ↑ Plantilla:Citar revista
- ↑ «Unificación de orden superior 30 años después». Actas, 15ª Conferencia Internacional TPLOS. LNCS 2410. Springer. 2002. pp. 3-12. Parámetro desconocido
|editor1-primero=ignorado (ayuda); Parámetro desconocido|último=ignorado (se sugiere|apellido=) (ayuda); Parámetro desconocido|editor1-último=ignorado (ayuda); Parámetro desconocido|primero=ignorado (se sugiere|nombre=) (ayuda) - ↑ Fitting, Melvin (2002). Types, Tableaus, and Gödel's God. Springer Science & Business Media. p. 139. ISBN 978-1-4020-0604-3. «El argumento de Gödel es modal y al menos de segundo orden, ya que en su definición de Dios hay una cuantificación explícita sobre las propiedades. [...] [AG96] mostró que uno podía ver una parte del argumento no como de segundo orden, sino como de tercer orden.»
Bibliografía
- Andrews, Peter B. (2002). An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, 2nd ed, Kluwer Academic Publishers, ISBN 1-4020-0763-9
- Stewart Shapiro, 1991, "Foundations Without Foundationalism: A Case for Second-Order Logic". Oxford University Press., ISBN 0-19-825029-0
- Stewart Shapiro, 2001, "Classical Logic II: Higher Order Logic," in Lou Goble, ed., The Blackwell Guide to Philosophical Logic. Blackwell, ISBN 0-631-20693-0
- Lambek, J. and Scott, P. J., 1986. Introduction to Higher Order Categorical Logic, Cambridge University Press, ISBN 0-521-35653-9
- Jacobs, Bart (1999). Categorical Logic and Type Theory. Studies in Logic and the Foundations of Mathematics 141. North Holland, Elsevier. ISBN 0-444-50170-3.
- Benzmüller, Christoph; Miller, Dale (2014). «Automation of Higher-Order Logic». En Gabbay, Dov M.; Siekmann, Jörg H.; Woods, John, eds. Handbook of the History of Logic, Volume 9: Computational Logic. Elsevier. ISBN 978-0-08-093067-1.
Enlaces externos
- Andrews, Peter B, Church's Type Theory in Stanford Encyclopedia of Philosophy.
- Miller, Dale, 1991, "Logic: Higher-order," Encyclopedia of Artificial Intelligence, 2nd ed.
- Herbert B. Enderton, Second-order and Higher-order Logic in Stanford Encyclopedia of Philosophy, published Dec 20, 2007; substantive revision Mar 4, 2009.