Saltar al contenido principal

# 11.4: Lógica de orden superior

$$\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

Pasar de la lógica de primer orden a la lógica de segundo orden nos permitió hablar de conjuntos de objetos en el dominio de primer orden, dentro del lenguaje formal. ¿Por qué parar ahí? Por ejemplo, la lógica de tercer orden debería permitirnos tratar con conjuntos de conjuntos de objetos, o tal vez incluso conjuntos que contienen tanto objetos como conjuntos de objetos. Y la lógica de cuarto orden nos permitirá hablar de conjuntos de objetos de ese tipo. Como habrás adivinado, se puede iterar esta idea arbitrariamente.

En la práctica, la lógica de orden superior a menudo se formula en términos de funciones en lugar de relaciones. (Modulo las identificaciones naturales, esta diferencia no es esencial.) Dados algunos “tipos” básicos$$A$$$$B$$$$C$$,,,... (que ahora llamaremos “tipos”), podemos crear otros nuevos estipulando

Si$$\sigma$$ y$$\tau$$ son tipos finitos entonces así es$$\sigma \to \tau$$.

Piense en los tipos como “etiquetas” sintácticas, que clasifican los objetos que queremos en nuestro dominio;$$\sigma \to \tau$$ describe aquellos objetos que son funciones que llevan objetos de tipo$$\sigma$$ a objetos de tipo$$\tau$$. Por ejemplo, podríamos querer tener un tipo$$\Omega$$ de valores de verdad, “verdaderos” y “falsos”, y un tipo$$\Nat$$ de números naturales. En ese caso, se puede pensar en objetos de tipo$$\Nat \to \Omega$$ como relaciones unarias, o subconjuntos de$$\Nat$$; los objetos de tipo$$\Nat \to \Nat$$ son funciones desde numeros naturales hasta números naturales; y los objetos de tipo$$(\Nat \to \Nat) \to \Nat$$ son “funcionales”, es decir, superiores- escriba funciones que llevan funciones a números.

Como en el caso de la lógica de segundo orden, se puede pensar en la lógica de orden superior como una especie de lógica de muchos ordenamientos, donde hay una especie para cada tipo de objeto que queremos considerar. Pero suele ser más claro solo para definir la sintaxis de la lógica de tipo superior desde cero. Por ejemplo, podemos definir un conjunto de tipos finitos inductivamente, de la siguiente manera:

1. $$\Nat$$es un tipo finito.

2. Si$$\sigma$$ y$$\tau$$ son tipos finitos, entonces también lo es$$\sigma \to \tau$$.

3. Si$$\sigma$$ y$$\tau$$ son tipos finitos, así es$$\sigma \times \tau$$.

Intuitivamente,$$\Nat$$ denota el tipo de los números naturales,$$\sigma \to \tau$$ denota el tipo de funciones de$$\sigma$$ a$$\tau$$, y$$\sigma \times \tau$$ denota el tipo de pares de objetos, uno de$$\sigma$$ y otro de $$\tau$$. Entonces podemos definir un conjunto de términos inductivamente, de la siguiente manera:

1. Para cada tipo$$\sigma$$, hay un stock de variables$$x$$,$$y$$,$$z$$,... de tipo$$\sigma$$

2. $$\Obj 0$$es un término de tipo$$\Nat$$

3. $$\Obj S$$(sucesor) es un término de tipo$$\Nat \to \Nat$$

4. Si$$s$$ es un término de tipo$$\sigma$$, y$$t$$ es un término de tipo$$\Nat \to (\sigma \to \sigma)$$, entonces$$\Obj{R}_{st}$$ es un término de tipo$$\Nat \to \sigma$$

5. Si$$s$$ es un término de tipo$$\tau \to \sigma$$ y$$t$$ es un término de tipo$$\tau$$, entonces$$s(t)$$ es un término de tipo$$\sigma$$

6. Si$$s$$ es un término de tipo$$\sigma$$ y$$x$$ es una variable de tipo$$\tau$$, entonces$$\lambd[x][s]$$ es un término de tipo$$\tau \to \sigma$$.

7. Si$$s$$ es un término de tipo$$\sigma$$ y$$t$$ es un término de tipo$$\tau$$, entonces$$\tuple{s, t}$$ es un término de tipo$$\sigma \times \tau$$.

8. Si$$s$$ es un término de tipo$$\sigma \times \tau$$ entonces$$p_1(s)$$ es un término de tipo$$\sigma$$ y$$p_2(s)$$ es un término de tipo$$\tau$$.

Intuitivamente,$$\Obj{R}_{st}$$ denota la función definida recursivamente por\begin{aligned} \Obj{R}_{st}(0) & = s \\ \Obj{R}_{st}(x+1) & = t(x, R_{st}(x)),\end{aligned}$$\tuple{s, t}$$ denota el par cuyo primer componente es$$s$$ y cuyo segundo componente es$$t$$, y$$p_1(s)$$ y$$p_2(s)$$ denotan el primer y segundo elementos (“proyecciones”) de$$s$$. Finalmente,$$\lambd[x][s]$$ denota la función$$f$$ definida por$f(x) = s\nonumber$ para cualquier$$x$$ tipo$$\sigma$$; así ítem (6) nos da una forma de comprensión, permitiéndonos definir funciones usando términos. Las fórmulas se construyen a partir de declaraciones de predicado de identidad$$\eq[s][t]$$ entre términos del mismo tipo, las conectivas proposicionales habituales y la cuantificación de tipo superior. Entonces se pueden tomar los axiomas del sistema como las ecuaciones básicas que rigen los términos definidos anteriormente, junto con las reglas habituales de lógica con cuantificadores y predicado de identidad.

Si se aumenta el sistema de tipos finitos con un tipo$$\Omega$$ de valores de verdad, hay que incluir axiomas que también gobiernan su uso. De hecho, si uno es inteligente, uno puede deshacerse de fórmulas complejas por completo, ¡reemplazándolas por términos de tipo$$\Omega$$! El sistema de prueba puede entonces ser modificado en consecuencia. El resultado es esencialmente la teoría simple de tipos planteada por la Iglesia Alonzo en la década de 1930.

Como en el caso de la lógica de segundo orden, hay diferentes versiones de semántica de tipo superior que uno podría querer usar. En la versión completa, las variables de tipo$$\sigma \to \tau$$ van sobre el conjunto de todas las funciones desde los objetos de tipo$$\sigma$$ hasta objetos de tipo$$\tau$$. Como cabría esperar, esta semántica es demasiado fuerte para admitir un sistema de pruebas completo y efectivo. Pero se puede considerar una semántica más débil, en la que una estructura consiste en conjuntos de elementos$$T_\tau$$ para cada tipo$$\tau$$, junto con operaciones apropiadas para aplicación, proyección, etc. Si los detalles se llevan a cabo correctamente, se pueden obtener teoremas de integridad para el tipos de sistemas de prueba descritos anteriormente.

La lógica de tipo superior es atractiva porque proporciona un marco en el que podemos incrustar una buena cantidad de matemáticas de una manera natural: comenzando con$$\Nat$$, se pueden definir números reales, funciones continuas, etc. También resulta particularmente atractivo en el contexto de la lógica intuicionista, ya que los tipos tienen claras intepretaciones “constructivas”. De hecho, se pueden desarrollar versiones constructivas de semántica de tipo superior (basadas en lógica intuicionista, más que clásica) que aclaren muy bien estas interpretaciones constructivas, y son, en muchos sentidos, más interesantes que las contrapartes clásicas.

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