Secuencia de elección

En matemáticas intuicionistas , una secuencia de elección es una formulación constructiva de una secuencia . Dado que la escuela intuicionista de matemáticas, formulada por LEJ Brouwer , rechaza la idea de un infinito completo , para utilizar una secuencia (que, en matemáticas clásicas, es un objeto infinito), debemos tener una formulación de un objeto finito y constructible que pueda cumplir la misma función que una secuencia. Así, Brouwer formuló la secuencia de elección, que se presenta como una construcción, en lugar de un objeto abstracto e infinito. ^{[ 1 ]}

Se distingue entre secuencias sin ley y secuencias con ley . ^{[ 2 ]} Una secuencia con ley es aquella que puede describirse completamente ; es una construcción completa que puede describirse totalmente. Por ejemplo, los números naturales.${\displaystyle \mathbb {N} }$puede pensarse como una secuencia de tipo ley: la secuencia puede describirse completamente de forma constructiva mediante el único elemento 0 y una función sucesora . Dada esta formulación, sabemos que la${\displaystyle i}$El enésimo elemento de la secuencia de números naturales será el número${\displaystyle i-1}$. De manera similar, una función${\displaystyle f:\mathbb {N} \mapsto \mathbb {N} }$El mapeo de los números naturales a los números naturales determina efectivamente el valor de cualquier argumento que tome y, por lo tanto, describe una secuencia que sigue una ley.

Por otro lado, una secuencia sin ley (o libre ) es aquella que no está predeterminada. Debe entenderse como un procedimiento para generar valores para los argumentos 0, 1, 2, .... Es decir, una secuencia sin ley.${\displaystyle \alpha }$es un procedimiento para generar${\displaystyle \alpha _{0}}$,${\displaystyle \alpha _{1}}$, ... (los elementos de la secuencia)${\displaystyle \alpha }$) de tal manera que:

• En cualquier momento dado de la construcción de la secuencia${\displaystyle \alpha }$, solo se conoce un segmento inicial de la secuencia y no se imponen restricciones a los valores futuros de${\displaystyle \alpha }$; y
• Se puede especificar, de antemano, un segmento inicial.${\displaystyle \langle \alpha _ {0},\alpha _ {1},\ldots,\alpha _ {k}\rangle}$de${\displaystyle \alpha }$.

Tenga en cuenta que el primer punto anterior es un poco engañoso, ya que podemos especificar, por ejemplo, que los valores de una secuencia se extraigan exclusivamente del conjunto de los números naturales; podemos especificar, a priori , el rango de la secuencia.

El ejemplo canónico de una secuencia sin ley es la serie de lanzamientos de un dado . Especificamos qué dado usar y, opcionalmente, especificamos de antemano los valores del primero.${\displaystyle k}$rollos (para${\displaystyle k\in \mathbb {N} }$). Además, restringimos los valores de la secuencia para que estén en el conjunto${\displaystyle \{1,2,3,4,5,6\}}$Esta especificación comprende el procedimiento para generar la secuencia sin ley en cuestión. Por lo tanto, en ningún momento se conoce ningún valor futuro particular de la secuencia.

Hay dos axiomas en particular que esperamos que se cumplan para las secuencias de elección descritas anteriormente. Sea${\displaystyle \alpha \in n}$denotan la relación "la secuencia${\displaystyle \alpha }$comienza con la secuencia inicial${\displaystyle n}$" para secuencia de elección${\displaystyle \alpha }$y segmento finito${\displaystyle n}$(más específicamente,${\displaystyle n}$probablemente será un número entero que codifica una secuencia inicial finita).

Esperamos que se cumpla lo siguiente, denominado axioma de datos abiertos , para todas las secuencias sin ley: $${\displaystyle A(\alpha )\rightarrow \exists n[\alpha \in n\,\land \,\forall \beta \in n[A(\beta )]]}$$ dónde${\displaystyle A}$es un predicado de un solo lugar . La justificación intuitiva de este axioma es la siguiente: en matemáticas intuicionistas, la verificación de que${\displaystyle A}$sostiene la secuencia${\displaystyle \alpha }$se da como un procedimiento ; en cualquier punto de ejecución de este procedimiento, habremos examinado solo un segmento inicial finito de la secuencia. Intuitivamente, entonces, este axioma establece que puesto que, en cualquier punto de verificación que${\displaystyle A}$posee de${\displaystyle \alpha }$, solo habremos verificado que${\displaystyle A}$se cumple para una secuencia inicial finita de${\displaystyle \alpha }$; por lo tanto, debe ser cierto que${\displaystyle A}$Esto también se aplica a cualquier secuencia sin ley.${\displaystyle \beta }$compartiendo esta secuencia inicial. Esto se debe a que, en cualquier punto del procedimiento de verificación${\displaystyle A(\alpha )}$, para cualquier tal${\displaystyle \beta }$compartiendo el prefijo inicial de${\displaystyle \alpha }$codificado por${\displaystyle n}$que ya hemos examinado, si ejecutamos el mismo procedimiento en${\displaystyle \beta }$Obtendremos el mismo resultado. El axioma puede generalizarse para cualquier predicado que tome un número arbitrario de argumentos.

Se requiere otro axioma para las secuencias sin ley. El axioma de densidad , dado por: $${\displaystyle \forall n\,\exists \alpha [\alpha \in n]}$$ establece que, para cualquier prefijo finito (codificado por)${\displaystyle n}$, hay alguna secuencia${\displaystyle \alpha }$Comenzando con ese prefijo. Requerimos este axioma para evitar "huecos" en el conjunto de secuencias de elección. Este axioma es la razón por la que exigimos que se puedan especificar de antemano secuencias iniciales finitas arbitrariamente largas de secuencias de elección no lineales; sin este requisito, el axioma de densidad no está necesariamente garantizado.

• Constructivismo (filosofía de las matemáticas) : postura filosófica que sostiene que las pruebas de existencia deben ser constructivas.