Lógica de segundo orden
# Lógica de segundo orden

Una lógica de segundo orden es una extensión de una lógica de primer orden en la que se añaden variables que representan propiedades, funciones y relaciones, y cuantificadores que operan sobre esas variables. Así se expande el poder expresivo del lenguaje sin tener que agregar nuevos símbolos lógicos.

# Lógica de segundo orden
## Introducción

La lógica de segundo orden surgió de la presentación inicial de la lógica de predicados de Gottlob Frege.Ya distinguía dos tipos de cuantificaciones diferentes(de variables o de predicados) pero no los separaba como lógicas distintas. Cuando Bertrand Russell enunció la Paradoja de Russell, entonces se empezó a diferenciar entre la lógica de primer orden y la lógica de segundo orden y también se refleja en el axioma de inducción de la aritmética de Giuseppe Peano:
    Para cualquier conjunto X de números enteros, si $0\in X$ y además $n\in X\Rightarrow n+1\in X$, entonces se tiene que $X=\mathbb {N}$
La expresión "para cualquier conjunto" requiere un lenguaje en el que los cuantificadores puedan abarcar no solo a variables que representan elementos concretos sino también a relaciones o funciones. Así el predicado $a\in X$ se representa mediante el símbolo ${\tilde {X}}(a)$, el axioma de inducción se puede representar formalmente como:
   $\forall {\tilde {X}}\ (({\tilde {X}}(0)\land \forall x({\tilde {X}}(x)\to {\tilde {X}}(x+1))\to \forall y{\tilde {X}}(y))$
Además, una lógica de segundo orden también puede cuantificar sobre propiedades. Gracias a eso puede expresar, por ejemplo, que todo individuo o tiene una propiedad o no la tiene:
   $\forall P\,\forall x\,(Px\lor \neg Px)$
O el principio de identidad de los indiscernibles:
    $\forall x\,\forall y\,{\Big\forall P(Px\leftrightarrow Py)\to (x=y){\Big )}$
Sin embargo, lo que se gana en poder expresivo se pierde en metateoría. Existen propiedades metateóricas generalmente consideradas deseables que las lógicas de segundo orden no tienen y las lógicas de primer orden sí. Por ejemplo, las lógicas de segundo orden (con semántica estándar) son incompletas. Quiere decir que no puede haber ningún sistema deductivo finito a partir del cual se puedan demostrar todas las verdades lógicas expresables en el lenguaje. Esto es: el conjunto de las verdades del sistema es mayor que el conjunto de las verdades demostrables en el sistema. Esto se debe a que las lógicas de segundo orden tienen el poder expresivo suficiente para ser afectadas por los teoremas de incompletitud de Gödel.

# Lógica de segundo orden
## Propiedades metalógicas

La lógica de segundo orden tiene un poder expresivo mayor que la lógica de primer orden. Ese mayor poder expresivo permite axiomatizar sistemas matemáticos más complejos. Es decir, hay proposiciones no formalizables exactamente utilitizando el formalismo de la lógica de primer orden que sí pueden ser formalizadas correctamente con la lógica de segundo orden. Sin duda ese último hecho constituye una ventaja, sin embargo, el uso de lógicas de segundo orden comporta ciertas dificultades:
* El teorema de compacidad, que afirma que un conjunto de proposiciones lógicas de una lógica de primer orden es satisfactible si y solo si cualquier subconjunto finito de estas proposiciones es satisfactible, no es válido para una lógica de segundo orden.
* El teorema de Löwenheim-Skolem que afirma que una lógica de primer orden con una cantidad finita de símbolos diferentes admite un modelo numerable no es válido para una lógica de segundo orden.
El hecho de que estos dos teoremas, muy útiles en ciertas aplicaciones, no se pueden generalizar a una lógica de segundo orden reducen la utilidad para esas aplicaciones de las lógicas de segundo orden. Debido a esos problemas se han buscado sistemas lógicos intermedios que generalicen la lógica de primer orden sin llegar a ser tan expresiva como una lógica de segundo orden. Los teoremas de Lindström proporcionan información sobre lo que cabe esperar de algunos de dichos sistemas.

# Lógica de segundo orden
## Detalles formales

Existen diversos tipos de lógicas de segundo orden según el tipo de variables adicionales introducidas respecto a las existentes en la lógica del primer orden. Es decir, existen diferentes formas de extender una lógica de primer orden a una lógica de segundo orden entre ellas:
* La lógica de segundo orden monádica (LSOM), en la que se añaden solo variables para subconjuntos de un cierto dominio.
* La lógica de segundo orden completa (LSOC), en la que se introducen todos los tipos de variables posibles y los cuantificadores pueden referirse, por tanto, a cualquiera de ellas.
Una lógica de segundo orden incluye cuantificadores de varios tipos ($\exists _{1},\forall _{1},\exists _{2},\forall _{2}$), además de cuantificadores de primer orden que requieren variables como las de la lógica de primer orden, existen cuantificadores para subconjuntos o propiedades, que no pueden aparecer en una lógica de primer orden. De la misma manera en la lógica de primer orden, la lógica de segundo orden puede contener signos no-lógicos para construir un lenguaje de segundo orden específico. La lógica de segundo orden contine fórmulas de primer orden y fórmulas de segundo orden. Una fórmula de lógica de segundo orden se llama fórmula de primer orden (y se considera un elemento del conjunto $\Sigma _{0}^{1}$ o del conjunto $\Pi _{0}^{1}$) si todos sus cuantificadores cuantifcan variables de primer orden (pudiendo contener además variables de segundo orden libres). Una fórmula de segundo orden existencial es una fórmula del conjunto $\Sigma _{1}^{1}$ que contiene además algunos cuantificadores existenciales sobre variables de segundo orden, es decir, $\exists _{2}R_{0}\ldots \exists _{2}R_{m}\phi$, donde $\phi$ es una fórmula de primer orden. El conjunto de fórmulas existenciales de segundo orden que contiene solo existenciales $\exists _{2}$ se designa como $\Sigma _{1}^{1}$ o incluso ∃SO. Las fórmulas de $\Pi _{1}^{1}$ se definen dualmente, son el conjunto de fórmulas de segundo orden que contienen solo cuantificadores $\forall _{2}$. Pueden formarse conjuntos más complicados definidos recursivamente para cualquier k > 0, como $\Sigma _{k+1}^{1}$ formado por fórmulas de la forma $\exists R_{0}\ldots \exists R_{m}\phi$, donde $\phi$ es una fórmula del tipo $\Pi _{k}^{1}$. (Ver jerarquía analítica para una construcción análoga de la aritmética de segundo orden.)