Saltar al contenido principal
LibreTexts Español

11.3: Lógica de segundo orden

  • Page ID
    103594
  • \( \newcommand{\vecs}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} } \)

    \( \newcommand{\vecd}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash {#1}}} \)

    \( \newcommand{\id}{\mathrm{id}}\) \( \newcommand{\Span}{\mathrm{span}}\)

    ( \newcommand{\kernel}{\mathrm{null}\,}\) \( \newcommand{\range}{\mathrm{range}\,}\)

    \( \newcommand{\RealPart}{\mathrm{Re}}\) \( \newcommand{\ImaginaryPart}{\mathrm{Im}}\)

    \( \newcommand{\Argument}{\mathrm{Arg}}\) \( \newcommand{\norm}[1]{\| #1 \|}\)

    \( \newcommand{\inner}[2]{\langle #1, #2 \rangle}\)

    \( \newcommand{\Span}{\mathrm{span}}\)

    \( \newcommand{\id}{\mathrm{id}}\)

    \( \newcommand{\Span}{\mathrm{span}}\)

    \( \newcommand{\kernel}{\mathrm{null}\,}\)

    \( \newcommand{\range}{\mathrm{range}\,}\)

    \( \newcommand{\RealPart}{\mathrm{Re}}\)

    \( \newcommand{\ImaginaryPart}{\mathrm{Im}}\)

    \( \newcommand{\Argument}{\mathrm{Arg}}\)

    \( \newcommand{\norm}[1]{\| #1 \|}\)

    \( \newcommand{\inner}[2]{\langle #1, #2 \rangle}\)

    \( \newcommand{\Span}{\mathrm{span}}\) \( \newcommand{\AA}{\unicode[.8,0]{x212B}}\)

    \( \newcommand{\vectorA}[1]{\vec{#1}}      % arrow\)

    \( \newcommand{\vectorAt}[1]{\vec{\text{#1}}}      % arrow\)

    \( \newcommand{\vectorB}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} } \)

    \( \newcommand{\vectorC}[1]{\textbf{#1}} \)

    \( \newcommand{\vectorD}[1]{\overrightarrow{#1}} \)

    \( \newcommand{\vectorDt}[1]{\overrightarrow{\text{#1}}} \)

    \( \newcommand{\vectE}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash{\mathbf {#1}}}} \)

    \( \newcommand{\vecs}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} } \)

    \( \newcommand{\vecd}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash {#1}}} \)

    \(\newcommand{\avec}{\mathbf a}\) \(\newcommand{\bvec}{\mathbf b}\) \(\newcommand{\cvec}{\mathbf c}\) \(\newcommand{\dvec}{\mathbf d}\) \(\newcommand{\dtil}{\widetilde{\mathbf d}}\) \(\newcommand{\evec}{\mathbf e}\) \(\newcommand{\fvec}{\mathbf f}\) \(\newcommand{\nvec}{\mathbf n}\) \(\newcommand{\pvec}{\mathbf p}\) \(\newcommand{\qvec}{\mathbf q}\) \(\newcommand{\svec}{\mathbf s}\) \(\newcommand{\tvec}{\mathbf t}\) \(\newcommand{\uvec}{\mathbf u}\) \(\newcommand{\vvec}{\mathbf v}\) \(\newcommand{\wvec}{\mathbf w}\) \(\newcommand{\xvec}{\mathbf x}\) \(\newcommand{\yvec}{\mathbf y}\) \(\newcommand{\zvec}{\mathbf z}\) \(\newcommand{\rvec}{\mathbf r}\) \(\newcommand{\mvec}{\mathbf m}\) \(\newcommand{\zerovec}{\mathbf 0}\) \(\newcommand{\onevec}{\mathbf 1}\) \(\newcommand{\real}{\mathbb R}\) \(\newcommand{\twovec}[2]{\left[\begin{array}{r}#1 \\ #2 \end{array}\right]}\) \(\newcommand{\ctwovec}[2]{\left[\begin{array}{c}#1 \\ #2 \end{array}\right]}\) \(\newcommand{\threevec}[3]{\left[\begin{array}{r}#1 \\ #2 \\ #3 \end{array}\right]}\) \(\newcommand{\cthreevec}[3]{\left[\begin{array}{c}#1 \\ #2 \\ #3 \end{array}\right]}\) \(\newcommand{\fourvec}[4]{\left[\begin{array}{r}#1 \\ #2 \\ #3 \\ #4 \end{array}\right]}\) \(\newcommand{\cfourvec}[4]{\left[\begin{array}{c}#1 \\ #2 \\ #3 \\ #4 \end{array}\right]}\) \(\newcommand{\fivevec}[5]{\left[\begin{array}{r}#1 \\ #2 \\ #3 \\ #4 \\ #5 \\ \end{array}\right]}\) \(\newcommand{\cfivevec}[5]{\left[\begin{array}{c}#1 \\ #2 \\ #3 \\ #4 \\ #5 \\ \end{array}\right]}\) \(\newcommand{\mattwo}[4]{\left[\begin{array}{rr}#1 \amp #2 \\ #3 \amp #4 \\ \end{array}\right]}\) \(\newcommand{\laspan}[1]{\text{Span}\{#1\}}\) \(\newcommand{\bcal}{\cal B}\) \(\newcommand{\ccal}{\cal C}\) \(\newcommand{\scal}{\cal S}\) \(\newcommand{\wcal}{\cal W}\) \(\newcommand{\ecal}{\cal E}\) \(\newcommand{\coords}[2]{\left\{#1\right\}_{#2}}\) \(\newcommand{\gray}[1]{\color{gray}{#1}}\) \(\newcommand{\lgray}[1]{\color{lightgray}{#1}}\) \(\newcommand{\rank}{\operatorname{rank}}\) \(\newcommand{\row}{\text{Row}}\) \(\newcommand{\col}{\text{Col}}\) \(\renewcommand{\row}{\text{Row}}\) \(\newcommand{\nul}{\text{Nul}}\) \(\newcommand{\var}{\text{Var}}\) \(\newcommand{\corr}{\text{corr}}\) \(\newcommand{\len}[1]{\left|#1\right|}\) \(\newcommand{\bbar}{\overline{\bvec}}\) \(\newcommand{\bhat}{\widehat{\bvec}}\) \(\newcommand{\bperp}{\bvec^\perp}\) \(\newcommand{\xhat}{\widehat{\xvec}}\) \(\newcommand{\vhat}{\widehat{\vvec}}\) \(\newcommand{\uhat}{\widehat{\uvec}}\) \(\newcommand{\what}{\widehat{\wvec}}\) \(\newcommand{\Sighat}{\widehat{\Sigma}}\) \(\newcommand{\lt}{<}\) \(\newcommand{\gt}{>}\) \(\newcommand{\amp}{&}\) \(\definecolor{fillinmathshade}{gray}{0.9}\)

    Template:MathJaxZach

    El lenguaje de la lógica de segundo orden permite cuantificar no solo sobre un dominio de individuos, sino también sobre las relaciones en ese dominio. Dado un lenguaje de primer orden\(\Lang{L}\), para cada\(k\) uno agrega variables\(R\) que oscilan sobre relaciones\(k\) arias, y permite cuantificar sobre esas variables. Si\(R\) es una variable para una relación\(k\) -aria, y\(t_1\),...,\(t_k\) son términos ordinarios (de primer orden),\(\Atom{R}{t_1,\dots,t_k}\) es una fórmula atómica. De lo contrario, el conjunto de fórmulas se define igual que en el caso de la lógica de primer orden, con cláusulas adicionales para la cuantificación de segundo orden. Tenga en cuenta que solo tenemos el predicado de identidad para términos de primer orden: si\(R\) y\(S\) son variables de relación de la misma aridad\(k\), podemos\(\eq[R][S]\) definir como una abreviatura de\[\lforall{x_1 \dots}{\lforall{x_k}{(\Atom{R}{x_1, \dots, x_k} \liff \Atom{S}{x_1, \dots, x_k})}}.\nonumber\]

    Las reglas para la lógica de segundo orden simplemente extienden las reglas del cuantificador a las nuevas variables de segundo orden. Aquí, sin embargo, hay que tener un poco de cuidado para explicar cómo estas variables interactúan con los símbolos predicados de\(\Lang{L}\), y con fórmulas de manera\(\Lang{L}\) más general. Como mínimo, las variables de relación cuentan como términos, entonces uno tiene inferencias de la forma\[A(R) \Proves \lexists{R}{A(R)}\nonumber\] Pero si\(\Lang{L}\) es el lenguaje de la aritmética con un símbolo de relación constante\(<\), también se esperaría que la siguiente inferencia fuera válida: \[x < y \Proves \lexists{R}{\Atom{R}{x,y}}\nonumber\]o para una fórmula dada\(A\),\[A(x_1, \dots, x_k) \Proves \lexists{R}{\Atom{R}{x_1,\dots,x_k}}\nonumber\] Más generalmente, podríamos querer permitir inferencias de la forma\[\Subst{A}{\lambd[\vec x][B(\vec x)]}{R} \Proves \lexists{R}{A}\nonumber\] donde\(\Subst{A}{\lambd[\vec x][B(\vec x)]}{R}\) denota el resultado de reemplazar cada fórmula atómica de la forma\(\Obj{R}{t_1,\dots,t_k}\) en \(A\)por\(B(t_1, \dots, t_k)\). Esta última regla equivale a tener un esquema de comprensión, es decir, un axioma de la forma\[\lexists{R}{\lforall{x_1, \dots, x_k}{(A(x_1, \dots, x_k) \liff \Atom{R}{x_1, \dots, x_k})}},\nonumber\] uno para cada fórmula\(A\) en el lenguaje de segundo orden, en el que no\(R\) es una variable libre. (Ejercicio: mostrar que si\(R\) se permite que ocurra en\(A\), ¡este esquema es inconsistente!)

    Cuando los logísticos se refieren a los “axiomas de la lógica de segundo orden” suelen significar la extensión mínima de la lógica de primer orden mediante reglas de cuantificador de segundo orden junto con el esquema de comprensión. Pero a menudo es interesante estudiar subsistemas más débiles de estos axiomas y reglas. Por ejemplo, nótese que en toda su generalidad el esquema axiómico de comprensión es impredicativo: permite afirmar la existencia de una relación\(\Atom{R}{x_1, \dots, x_k}\) que se “define” por una fórmula con cuantificadores de segundo orden; y estos cuantificadores van sobre el conjunto de todas esas relaciones, a conjunto que se incluye a\(R\) sí mismo! Alrededor del cambio del siglo XX, una reacción común a la paradoja de Russell fue culpar a tales definiciones, y evitarlas en el desarrollo de las bases de las matemáticas. Si se prohíbe el uso de cuantificadores de segundo orden en la fórmula\(A\), se tiene una forma predicativa de comprensión, que es algo más débil.

    Desde el punto de vista semántico, se puede pensar que una estructura de segundo orden consiste en una estructura de primer orden para el lenguaje, aunada a un conjunto de relaciones sobre el dominio sobre el que se ubican los cuantificadores de segundo orden (más precisamente, para cada uno\(k\) hay un conjunto de relaciones de aridad \(k\)). Por supuesto, si la comprensión está incluida en el sistema de prueba, entonces tenemos el requisito agregado de que hay suficientes relaciones en la “parte de segundo orden” para satisfacer los axiomas de comprensión; de lo contrario, ¡el sistema de prueba no es sólido! Una manera fácil de asegurar que haya suficientes relaciones alrededor es tomar la parte de segundo orden para que consista en todas las relaciones en la parte de primer orden. Tal estructura se llama completa, y, en cierto sentido, es realmente la “estructura pretendida” para el lenguaje. Si restringimos nuestra atención a estructuras completas tenemos lo que se conoce como la semántica completa de segundo orden. En ese caso, especificar una estructura se reduce a especificar la parte de primer orden, ya que el contenido de la parte de segundo orden se deriva implícitamente de eso.

    Para resumir, hay cierta ambigüedad a la hora de hablar de lógica de segundo orden. En términos del sistema de prueba, uno podría tener en mente

    1. Un sistema de prueba de segundo orden “mínimo”, junto con algunos axiomas de comprensión.

    2. El sistema de prueba de segundo orden “estándar”, con plena comprensión.

    En cuanto a la semántica, uno podría estar interesado en

    1. La semántica “débil”, donde una estructura consiste en una parte de primer orden, junto con una parte de segundo orden lo suficientemente grande como para satisfacer los axiomas de comprensión.

    2. La semántica “estándar” de segundo orden, en la que se consideran sólo estructuras completas.

    Cuando los logísticos no especifican el sistema de prueba o la semántica que tienen en mente, generalmente se refieren al segundo ítem de cada lista. La ventaja de usar esta semántica es que, como veremos, nos da descripciones categóricas de muchas estructuras matemáticas naturales; al mismo tiempo, el sistema de prueba es bastante fuerte, y sonido para esta semántica. El inconveniente es que el sistema de prueba no está completo para la semántica; de hecho, ningún sistema de prueba efectivamente dado está completo para la semántica completa de segundo orden. Por otra parte, veremos que el sistema de prueba está completo para la semántica debilitada; esto implica que si una oración no es demostrable, entonces hay alguna estructura, no necesariamente la completa, en la que es falsa.

    El lenguaje de la lógica de segundo orden es bastante rico. Se pueden identificar relaciones unarias con subconjuntos del dominio, y así en particular se puede cuantificar sobre estos conjuntos; por ejemplo, se puede expresar inducción para los números naturales con un solo axioma\[\lforall{R}{((\Atom{R}{\Obj{0}} \land \lforall{x}{(\Atom{R}{x} \lif \Atom{R}{x'})}) \lif \lforall{x}{\Atom{R}{x}})}.\nonumber\] Si se toma el lenguaje de la aritmética para tener símbolos\(\Obj 0, \Obj \prime, +, \times\) y \(<\), se pueden agregar los siguientes axiomas para describir su comportamiento:

    1. \(\lforall{x}{\lnot x' = \Obj 0}\)

    2. \(\lforall{x}{\lforall{y}{(s(x) = s(y) \lif x = y)}}\)

    3. \(\lforall{x}{(x + \Obj 0) = x}\)

    4. \(\lforall{x}{\lforall{y}{(x + y') = (x + y)'}}\)

    5. \(\lforall{x}{(x \times \Obj 0) = \Obj 0}\)

    6. \(\lforall{x}{\lforall{y}{(x \times y') = ((x \times y) + x)}}\)

    7. \(\lforall{x}{\lforall{y}{(x < y \liff \lexists{z}{y = (x + z')})}}\)

    No es difícil demostrar que estos axiomas, junto con el axioma de inducción anterior, proporcionan una descripción categórica de la estructura\(\Struct{N}\), el modelo estándar de aritmética, siempre que estemos utilizando la semántica completa de segundo orden. Dada cualquier estructura\(\Struct{M}\) en la que estos axiomas sean verdaderos, definir una función\(f\) desde\(\Nat\) el dominio de\(\Struct{M}\) usar recursión ordinaria en\(\Nat\), de manera que\(f(0) = \Assign{\Obj 0}{M}\) y\(f(x+1) = \Assign{\prime}{M}(f(x))\). Usando la inducción ordinaria\(\Nat\) y el hecho de que los axiomas (1) y (2) se aferran\(\Struct M\), vemos que\(f\) es inyectivo. Para ver que\(f\) es suryectiva, deja\(P\) ser el conjunto de elementos de los\(\Domain{M}\) que están en el rango de\(f\). Ya que\(\Struct M\) está lleno,\(P\) está en el dominio de segundo orden. Por la construcción de\(f\), sabemos que\(\Assign{\Obj 0}{M}\) está en\(P\), y eso\(P\) está cerrado bajo\(\Assign{\prime}{M}\). El hecho de que el axioma de inducción se mantenga en\(\Struct M\) (en particular, para\(P\)) garantiza que\(P\) es igual a todo el dominio de primer orden de\(\Struct M\). Esto demuestra que\(f\) es una bijección. Demostrar que\(f\) es un homomorfismo no es más difícil, utilizando la inducción ordinaria en\(\Nat\) repetidas ocasiones.

    En términos set-teóricos, una función es solo un tipo especial de relación; por ejemplo, una función unaria\(f\) puede identificarse con una relación binaria\(R\) satisfactoria\(\lforall{x}{\lexists{!y}{R(x,y)}}\). Como resultado, también se pueden cuantificar sobre las funciones. Usando la semántica completa, se puede definir entonces la clase de estructuras infinitas para que sea la clase de estructuras\(\Struct M\) para las que existe una función de inyección desde el dominio de\(\Struct M\) hasta un subconjunto propio de sí mismo:\[\lexists{f}{(\lforall{x}{\lforall{y}{(\eq[f(x)][f(y)] \lif \eq[x][y])}} \land \lexists{y}{\lforall{x}{\eqN[f(x)][y]}})}.\nonumber\] La negación de esta oración entonces define la clase de estructuras finitas.

    Además, se puede definir la clase de ordenamientos de pozos, agregando lo siguiente a la definición de un ordenamiento lineal:\[\lforall{P}{(\lexists{x}{\Atom{P}{x}} \lif \lexists{x}{(\Atom{P}{x} \land \lforall{y}{(y < x \lif \lnot \Atom{P}{y})})})}.\nonumber\] Esto afirma que cada conjunto no vacío tiene un elemento mínimo, módulo la identificación de “conjunto” con “relación de un solo lugar”. Para otro ejemplo, se puede expresar la noción de conectividad para las gráficas, diciendo que no hay una separación no trivial de los vértices en partes desconectadas:\[\lnot \lexists{A}{(\lexists{x}{A(x)} \land \lexists{y}{\lnot A(y)} \land \lforall{w}{\lforall{z}{((\Atom{A}{w} \land \lnot \Atom{A}{z}) \lif \lnot \Atom{R}{w,z})}})}.\nonumber\] Para otro ejemplo más, podrías intentar como ejercicio definir la clase de estructuras finitas cuyo dominio tenga un tamaño par. De manera más sorprendente, se puede proporcionar una descripción categórica de los números reales como un campo ordenado completo que contiene los racionales.

    En definitiva, la lógica de segundo orden es mucho más expresiva que la lógica de primer orden. Esa es la buena noticia; ahora para la mala. Ya hemos mencionado que no existe un sistema de prueba efectivo que esté completo para la semántica completa de segundo orden. Para bien o para mal, muchas de las propiedades de la lógica de primer orden están ausentes, entre ellas la compacidad y los teoremas de Löwenheim-Skolem.

    Por otro lado, si uno está dispuesto a renunciar a la semántica completa de segundo orden en términos de la más débil, entonces el sistema mínimo de prueba de segundo orden está completo para esta semántica. Es decir, si leemos\(\Proves\) como “prueba en el sistema mínimo” y\(\Entails\) como “implica lógicamente en la semántica más débil”, podemos demostrarlo siempre que\(\Gamma \Entails A\) entonces\(\Gamma \Proves A\). Si se quiere incluir axiomas específicos de comprensión en el sistema de prueba, hay que restringir la semántica a estructuras de segundo orden que satisfagan estos axiomas: por ejemplo, si\(\Delta\) consiste en un conjunto de axiomas de comprensión (posiblemente todos ellos), tenemos que si\(\Gamma \cup \Delta \Entails A\), entonces\(\Gamma \cup \Delta \Proves A\). En particular, si no\(A\) es demostrable utilizando los axiomas de comprensión que estamos considerando, entonces existe un modelo\(\lnot A\) en el que se mantienen estos axiomas de comprensión, sin embargo.

    La manera más fácil de ver que el teorema de integridad sostiene para la semántica más débil es pensar en la lógica de segundo orden como una lógica de muchos ordenamientos, de la siguiente manera. Una especie se interpreta como el dominio ordinario de “primer orden”, y luego para cada uno\(k\) tenemos un dominio de “relaciones de aridad\(k\). Tomamos el lenguaje para tener incorporados símbolos de relación “\(\Atom{\Obj{true}_k}{R,x_1,\dots,x_k}\)” que pretende afirmar que\(R\) sostiene de\(x_1\),...\(x_k\), donde\(R\) es una variable del tipo “relación\(k\) -aria” y \(x_1\),...,\(x_k\) son objetos de primer orden.

    Con esta identificación, la débil semántica de segundo orden es esencialmente la semántica habitual para la lógica de muchos ordenados; y ya hemos observado que la lógica de muchos ordenados puede integrarse en la lógica de primer orden. Modulo las traducciones de ida y vuelta, entonces, la concepción más débil de la lógica de segundo orden es realmente una forma de lógica de primer orden disfrazada, donde el dominio contiene tanto “objetos” como “relaciones” gobernadas por los axiomas apropiados.


    This page titled 11.3: Lógica de segundo orden is shared under a CC BY license and was authored, remixed, and/or curated by Richard Zach et al. (Open Logic Project) .