Propagación (intuicionismo)

Tipo particular de especies: secuencias infinitas definidas mediante propiedades decidibles finitas

En matemáticas intuicionistas , una dispersión es un tipo particular de especie de secuencias infinitas definidas mediante propiedades decidibles finitas . Aquí, una especie es una colección, una noción similar a un conjunto clásico en el sentido de que una especie está determinada por sus miembros.

Historia

La noción de dispersión fue propuesta por primera vez por LEJ Brouwer (1918B) y se utilizó para definir el continuo . A medida que se desarrollaron sus ideas, el uso de dispersiones se volvió común en las matemáticas intuicionistas , especialmente cuando se trata de secuencias de elección y análisis intuicionista (ver Dummett 77, Troelstra 77). En este último, los números reales se representan mediante las dispersiones de números naturales o enteros.

Los llamados abanicos, más restringidos, son de particular interés en los fundamentos intuicionistas de las matemáticas . Allí, su principal uso es en la discusión del teorema del abanico (que trata sobre barras , no se analiza aquí), un resultado que se utiliza en la derivación del teorema de continuidad uniforme.

Definiciones

Descripción general

En la terminología moderna, un spread es un conjunto cerrado habitado de secuencias. Los spreads se definen a través de una función de spread , que realiza una "verificación" ( decidible ) en secuencias finitas. Si todas las partes iniciales finitas de una secuencia infinita satisfacen la "verificación" de una función de spread, entonces decimos que la secuencia infinita es admisible para el spread . La noción de un spread y su función de spread son intercambiables en la literatura. Teóricamente , se puede pensar en un spread en términos de un árbol dirigido con raíces y etiquetas numéricas en los vértices . Un abanico , también conocido como spread finitario , es un tipo especial de spread. En términos de grafos, tiene ramificaciones finitas. Finalmente, un spread arreglado es un spread junto con alguna función que actúa sobre secuencias finitas.

Notación preliminar y terminología

En este artículo se utilizan " " y " " para indicar el comienzo o el final de una secuencia. La secuencia sin elementos, denominada secuencia vacía, se denota con . ${\displaystyle \langle }$ ${\displaystyle \rangle }$ ${\displaystyle \langle \rangle }$

Dada una secuencia infinita , decimos que la secuencia finita es un segmento inicial de si y sólo si y y ... y . ${\displaystyle \langle x_{1},x_{2},\ldots \rangle }$ ${\displaystyle \langle y_{1},y_{2},\ldots ,y_{i}\rangle }$ ${\displaystyle \langle x_{1},x_{2},\ldots \rangle }$ ${\displaystyle x_{1}=y_{1}}$ ${\displaystyle x_{2}=y_{2}}$ ${\displaystyle x_{i}=y_{i}}$

Función de propagación

Una función de dispersión es una función en secuencias finitas que satisface las siguientes propiedades: ${\displaystyle s}$

• Dada cualquier secuencia finita, ya sea o . En otras palabras, la propiedad que se está probando debe ser decidible mediante . ${\displaystyle \langle x_{1},x_{2},\ldots ,x_{i}\rangle }$ ${\displaystyle s(\langle x_{1},x_{2},\ldots ,x_{i}\rangle )=0}$ ${\displaystyle s(\langle x_{1},x_{2},\ldots ,x_{i}\rangle )=1}$ ${\displaystyle s}$
• ${\displaystyle s(\langle \rangle )=0}$.
• Dada cualquier secuencia finita tal que , existen algunas tales que . ${\displaystyle \langle x_{1},x_{2},\ldots ,x_{i}\rangle }$ ${\displaystyle s(\langle x_{1},x_{2},\ldots ,x_{i}\rangle )=0}$ ${\displaystyle k}$ ${\displaystyle s(\langle x_{1},x_{2},\ldots ,x_{i},k\rangle )=0}$

Dada una secuencia finita, si devuelve 0, la secuencia es admisible en la extensión dada hasta , y de lo contrario es inadmisible . La secuencia vacía es admisible y, por lo tanto, parte de cada extensión. Cada secuencia finita en la extensión se puede extender a otra secuencia finita en la extensión agregando un elemento adicional al final de la secuencia. De esa manera, la función de extensión actúa como una función característica que acepta muchas secuencias finitas largas. ${\displaystyle s}$ ${\displaystyle s}$

También decimos que una secuencia infinita es admisible para una extensión definida por una función de extensión si y solo si cada segmento inicial de es admisible para . Por ejemplo, para un predicado que caracteriza una secuencia de números interminable similar a una ley, se puede validar que es admisible con respecto a alguna función de extensión. ${\displaystyle \langle x_{1},x_{2},\ldots \rangle }$ ${\displaystyle s}$ ${\displaystyle \langle x_{1},x_{2},\ldots \rangle }$ ${\displaystyle s}$

Admirador

De manera informal, una función de dispersión define un abanico si, dada una secuencia finita admisible en la dispersión, solo hay un número finito de valores posibles que podemos agregar al final de esta secuencia de manera que nuestra nueva secuencia finita extendida sea admisible en la dispersión. Alternativamente, podemos decir que existe un límite superior para el valor de cada elemento de cualquier secuencia admisible en la dispersión. Formalmente: ${\displaystyle s}$

• Una función de propagación define un abanico si y solo si, dada cualquier secuencia admisible para la propagación , entonces existe alguna tal que, dado cualquier entonces ${\displaystyle s}$ ${\displaystyle \langle x_{1},x_{2},\ldots ,x_{i}\rangle }$ ${\displaystyle k}$ ${\displaystyle j>k}$ ${\displaystyle s(\langle x_{1},x_{2},\ldots ,x_{i},j\rangle )=1}$

Entonces, dada una secuencia admisible para el ventilador, solo tenemos un número finito de extensiones posibles que también son admisibles para el ventilador, y conocemos el elemento máximo que podemos agregar a nuestra secuencia admisible de modo que la extensión siga siendo admisible.

Ejemplos

Spreads

Algunos ejemplos sencillos de spreads incluyen:

• El conjunto de secuencias de números pares
• El conjunto de sucesiones de los números enteros 1–6
• El conjunto de secuencias de comandos de terminal válidos. ^{[ aclaración necesaria ]}

Aficionados

• El conjunto de secuencias de movimientos legales del ajedrez.
• El conjunto de secuencias binarias infinitas
• El conjunto de secuencias de letras

A continuación se presentan dos spreads comúnmente utilizados en la literatura.

La difusión universal (lacontinuo)

Dada cualquier secuencia finita , tenemos . En otras palabras, esta es la distribución que contiene todas las secuencias posibles. Esta distribución se utiliza a menudo para representar la colección de todas las secuencias de elección . ${\displaystyle \langle x_{1},x_{2},\ldots ,x_{i}\rangle }$ ${\displaystyle s(\langle x_{1},x_{2},\ldots ,x_{i}\rangle )=0}$

El spread binario

Dada cualquier secuencia finita , si todos nuestros elementos ( ) son 0 o 1 entonces , en caso contrario . En otras palabras, esta es la dispersión que contiene todas las secuencias binarias . ${\displaystyle \langle x_{1},x_{2},\ldots ,x_{i}\rangle }$ ${\displaystyle x_{1},x_{2},\ldots ,x_{i}}$ ${\displaystyle s(\langle x_{1},x_{2},\ldots ,x_{i}\rangle )=0}$ ${\displaystyle s(\langle x_{1},x_{2},\ldots ,x_{i}\rangle )=1}$

Vestidos de noche

Un ejemplo de una dispersión vestida es la dispersión de números enteros tal que si y solo si ${\displaystyle s(\langle x_{1},x_{2},\ldots ,x_{i}\rangle )=0}$

${\displaystyle \forall y.(0<y\leq i)\to {\big (}(x_{i}=0)\lor (x_{i}=2\cdot x_{y-1}\pm 1){\big )}}$,

Junto con la función . Esto representa los números reales . ${\displaystyle f(\langle x_{1},x_{2},\ldots ,x_{i}\rangle )=x_{i}\cdot 2^{2-i}}$

Véase también

• Barra de inducción
• Secuencia de elección
• Análisis constructivo

Referencias

• LEJ Brouwer Begründung der Mengenlehre unabhängig vom logischen Satz vom ausgeschlossenen Dritten. Erster Teil, Allgemeine Mengenlehre , KNAW Verhandelingen, 5: 1–43 (1918A)
• Michael Dummett Elementos del intuicionismo , Oxford University Press (1977)
• AS Troelstra Secuencias de elección: un capítulo de matemáticas intuicionistas , Clarendon Press (1977)