11.5: Lógica Intuicionista

Última actualización
Guardar como PDF

Page ID: 103585

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

Template:MathJaxZach

Contraste a la lógica de segundo orden y de orden superior, la lógica intuicionista de primer orden representa una restricción de la versión clásica, destinada a modelar un tipo de razonamiento más “constructivo”. Los siguientes ejemplos pueden servir para ilustrar algunas de las motivaciones subyacentes.

Supongamos que alguien se le acercó un día y anunció que había determinado un número natural$x$, con la propiedad de que si$x$ es primo, la hipótesis de Riemann es verdadera, y si$x$ es compuesta, la hipótesis de Riemann es falsa. ¡Grandes noticias! Si la hipótesis de Riemann es cierta o no es una de las grandes cuestiones abiertas de las matemáticas, y aquí parecen haber reducido el problema a uno de cálculo, es decir, a la determinación de si un número específico es primo o no.

¿Cuál es el valor mágico de$x$? Lo describen de la siguiente manera:$x$ es el número natural que es igual a$7$ si la hipótesis de Riemann es verdadera, y de$9$ otra manera.

Enfurecida, exiges que te devolvamos tu dinero. Desde un punto de vista clásico, la descripción anterior sí determina de hecho un valor único de$x$; pero lo que realmente quieres es un valor de$x$ eso se da explícitamente.

Para tomar otro ejemplo, quizás menos ideado, considere la siguiente pregunta. Sabemos que es posible elevar un número irracional a un poder racional, y obtener un resultado racional. Por ejemplo,$\sqrt{2}^2 = 2$. Lo que está menos claro es si es posible o no elevar un número irracional a un poder irracional, y obtener un resultado racional. El siguiente teorema responde a esto de manera afirmativa:

Teorema$\PageIndex{1}$

Hay números irracionales$a$ y$b$ tal eso$a^b$ es racional.

Prueba. Considerar$\sqrt{2}^{\sqrt{2}}$. Si esto es racional, ya terminamos: podemos dejar$a = b = \sqrt{2}$. De lo contrario, es irracional. Entonces tenemos\[(\sqrt{2}^{\sqrt{2}})^{\sqrt{2}} = \sqrt{2}^{\sqrt{2} \cdot \sqrt{2}} = \sqrt{2}^2 = 2,\nonumber\] lo que sin duda es racional. Entonces, en este caso,$a$ déjese$\sqrt{2}^{\sqrt{2}}$, y déjelo$b$ ser$\sqrt 2$. ◻

¿Constituye esto una prueba válida? La mayoría de los matemáticos sienten que sí. Pero de nuevo, aquí hay algo un poco insatisfactorio: hemos demostrado la existencia de un par de números reales con cierta propiedad, sin poder decir qué par de números es. Es posible probar el mismo resultado, pero de tal manera que el par$a$,$b$ se da en la prueba: tomar$a = \sqrt{3}$ y$b = \log_3 4$. Entonces\[a^b = \sqrt{3}^{\log_3 4} = 3^{1/2 \cdot \log_3 4} = (3^{\log_3 4})^{1/2} = 4^{1/2}= 2,\nonumber\] desde$3^{\log_3 x} = x$.

La lógica intuicionista está diseñada para modelar una especie de razonamiento donde se deshabilitan movimientos como el de la primera prueba. Demostrar la existencia de un$x$ satisfactorio$A(x)$ significa que hay que dar un específico$x$, y una prueba de que satisface$A$, como en la segunda prueba. Demostrar eso$A$ o$B$ sostiene requiere que puedas probar uno u otro.

Formalmente hablando, la lógica intuicionista de primer orden es lo que se obtiene si se omite restringir un sistema de prueba para la lógica de primer orden de cierta manera. Del mismo modo, existen versiones intuicionistas de lógica de segundo orden o de orden superior. Desde el punto de vista matemático, se trata únicamente de sistemas deductivos formales, pero, como ya se señaló, se pretende modelar una especie de razonamiento matemático. Uno puede tomar esto como el tipo de razonamiento que se justifica en una cierta visión filosófica de las matemáticas (como el intuicionismo de Brouwer); uno puede tomarlo como una especie de razonamiento matemático que es más “concreto” y satisfactorio (en la línea del constructivismo de Bishop); y se puede discutir sobre si la descripción formal capta o no la motivación informal. Pero cualesquiera que sean las posiciones filosóficas que podamos tener, podemos estudiar la lógica intuicionista como una lógica formalmente presentada; y por cualquier razón, a muchos logísticos matemáticos les resulta interesante hacerlo.

Existe una interpretación constructiva informal de los conectivos intuicionistas, generalmente conocidos como la interpretación BHK (que lleva el nombre de Brouwer, Heyting y Kolmogorov). Se ejecuta de la siguiente manera: una prueba de$A \land B$ consiste en una prueba de$A$ emparejado con una prueba de$B$; una prueba de$A \lor B$ consiste en ya sea una prueba de$A$, o una prueba de$B$, donde tenemos explícita información en cuanto a cuál es el caso; una prueba de$A \lif B$ consiste en un procedimiento, que transforma una prueba de$A$ en una prueba de$B$; una prueba de$\lforall{x}{A(x)}$ consiste en un procedimiento que devuelve una prueba de$A(x)$ para cualquier valor de$x$; y una prueba de$\lexists{x}{A(x)}$ consiste en un valor de$x$, junto con una prueba de que este valor satisface$A$. Se puede describir la interpretación en términos computacionales conocidos como el “isomorfismo Curry-Howard” o el “paradigma de fórmulas como tipos”: pensar en una fórmula como especificar un cierto tipo de datos, y pruebas como objetos computacionales de estos tipos de datos que nos permiten ver que la fórmula correspondiente es verdadera .

A menudo se piensa que la lógica intuicionista es lógica clásica “menos” la ley del medio excluido. Este teorema siguiente lo hace más preciso.

Teorema$\PageIndex{2}$

Intuicionísticamente, los siguientes esquemas de axiomas son equivalentes:

$(A \lif \lfalse) \lif \lnot A$.
$A \lor \lnot A$
$\lnot \lnot A \lif A$

Obtener instancias de un esquema de cualquiera de los otros es un buen ejercicio de lógica intuicionista.

Los primeros sistemas deductivos para la lógica proposicional intuicionista, planteados como formalizaciones del intuicionismo de Brouwer, se deben, independientemente, a Kolmogorov, Glivenko y Heyting. La primera formalización de la lógica intuicionista de primer orden (y partes de las matemáticas intuicionistas) se debe a Heyting. Aunque una serie de esquemas clásicamente válidos no son intuitivamente válidos, muchos lo son.

La traducción de doble negación describe una importante relación entre lógica clásica e intuicionista. Se define inductivamente sigue (piense$A^N$ como la traducción “intuicionista” de la fórmula clásica$A$):\[\begin{aligned} A^N & \ident \lnot\lnot A \quad \text{for atomic formulas $A$} \\ (A \land B)^N & \ident (A^N \land B^N) \\ (A \lor B)^N & \ident \lnot\lnot (A^N \lor B^N) \\ (A \lif B)^N & \ident (A^N \lif B^N) \\ (\lforall{x}{A})^N & \ident \lforall{x}{A^N} \\ (\lexists{x}{A})^N & \ident \lnot\lnot\lexists{x}{A^N}\end{aligned}\] Kolmogorov y Glivenko tenían versiones de esta traducción para la lógica proposicional; para la lógica predicada, se debe a Gödel y Gentzen, independientemente. Tenemos

Teorema$\PageIndex{3}$

$A \liff A^N$es demostrable clásicamente
Si$A$ es demostrable clásicamente, entonces$A^N$ es demostrable intuitivamente.

Ahora podemos vislumbrar el siguiente diálogo. Matemático clásico: “¡Lo he probado$A$!” Matemático intuicionista: “Tu prueba no es válida. Lo que realmente has demostrado es”$A^N$. Matemático clásico: “¡Bien por mí!” En lo que respecta al matemático clásico, el intuicionista apenas está partiendo pelos, ya que los dos son equivalentes. Pero el intuicionista insiste en que hay una diferencia.

Obsérvese que la traducción anterior se refiere únicamente a la lógica pura; no aborda la cuestión de cuáles son los axiomas no lógicos apropiados para las matemáticas clásicas e intuicionistas, o cuál es la relación entre ellas. Pero la siguiente ligera extensión del teorema anterior proporciona alguna información útil:

Teorema$\PageIndex{4}$

Si se$\Gamma$ prueba$A$ clásicamente,$\Gamma^N$$A^N$ demuestra intuitivamente.

En otras palabras, si$A$ es demostrable a partir de algunas hipótesis clásicamente, entonces$A^N$ es demostrable a partir de sus traducciones de doble negación.

Para demostrar que una oración o fórmula proposicional es intuitivamente válida, todo lo que tienes que hacer es aportar una prueba. Pero, ¿cómo puedes demostrar que no es válido? Para ello, necesitamos una semántica que sea sólida, y preferentemente completa. Una semántica debida a Kripke encaja muy bien en la factura.

Podemos jugar el mismo juego que hicimos para la lógica clásica: definir la semántica, y demostrar solidez e integridad. Sin embargo, vale la pena señalar la siguiente distinción. En el caso de la lógica clásica, la semántica era la “obvia”, en un sentido implícito en el sentido de los conectivos. Aunque uno puede proporcionar alguna motivación intuitiva para la semántica de Kripke, esta última no ofrece la misma sensación de inevitabilidad. Además, la noción de una estructura clásica es matemática natural, por lo que podemos tomar la noción de estructura como una herramienta para estudiar la lógica clásica de primer orden, o tomar la lógica clásica de primer orden como una herramienta para estudiar estructuras matemáticas. Por el contrario, las estructuras de Kripke solo pueden ser vistas como una construcción lógica; no parecen tener un interés matemático independiente.

Una estructura Kripke$\mModel M = \tuple{W, R, V}$ para un lenguaje proposicional consiste$R$ en un conjunto$W$, orden parcial$W$ con un elemento mínimo, y una asignación “monótona” de variables proposicionales a los elementos de$W$. La intuición es que los elementos de$W$ representan “mundos”, o “estados de conocimiento”; un elemento$v \geq u$ representa un “posible estado futuro” de$u$; y las variables proposicionales asignadas$u$ son las proposiciones que son conocido por ser cierto en estado$u$. La relación forzosa extiende$\mSat[,w]{M}{A}$ entonces esta relación a fórmulas arbitrarias en el lenguaje; leídas$\mSat[,w]{M}{A}$ como “$A$es verdad en el estado”$w$. La relación se define inductivamente, de la siguiente manera:

$\mSat[,w]{M}{\Obj p_i}$iff$\Obj p_i$ es una de las variables proposicionales asignadas a$w$.
$\mSatN[,w]{M}{\lfalse}$.
$\mSat[,w]{M}{(A \land B)}$iff$\mSat[,w]{M}{A}$ y$\mSat[,w]{M}{B}$.
$\mSat[,w]{M}{(A \lor B)}$iff$\mSat[,w]{M}{A}$ o$\mSat[,w]{M}{B}$.
$\mSat[,w]{M}{(A \lif B)}$iff, cuando$w' \geq w$ y$\mSat[,w']{M}{A}$, entonces$\mSat[,w']{M}{B}$.

Es un buen ejercicio para tratar de mostrar que no$\lnot (p \land q) \lif (\lnot p \lor \lnot q)$ es intuitivamente válido, cocinando una estructura Kripke que proporcione un contraejemplo.