En matemáticas , un setoide ( X , ~) es un conjunto (o tipo ) X equipado con una relación de equivalencia ~. Un setoide también puede denominarse conjunto E , conjunto de obispo o conjunto extensional . [1]
Los setoides se estudian especialmente en la teoría de la prueba y en los fundamentos matemáticos de la teoría de tipos . A menudo, en matemáticas, cuando se define una relación de equivalencia en un conjunto, se forma inmediatamente el conjunto cociente (convirtiendo la equivalencia en igualdad ). Por el contrario, los setoides se pueden utilizar cuando se debe mantener una diferencia entre identidad y equivalencia, a menudo con una interpretación de igualdad intensional (la igualdad en el conjunto original) e igualdad extensional (la relación de equivalencia o la igualdad en el conjunto cociente).
En la teoría de la prueba, particularmente en la teoría de la prueba de las matemáticas constructivas basada en la correspondencia Curry-Howard , a menudo se identifica una proposición matemática con su conjunto de pruebas (si las hay). Por supuesto, una proposición dada puede tener muchas pruebas; Según el principio de irrelevancia de la prueba, normalmente sólo importa la verdad de la proposición, no qué prueba se utilizó. Sin embargo, la correspondencia Curry-Howard puede convertir las pruebas en algoritmos , y las diferencias entre algoritmos suelen ser importantes. Por lo tanto, los teóricos de la prueba pueden preferir identificar una proposición con un conjunto de pruebas, considerando las pruebas equivalentes si pueden convertirse unas en otras mediante conversión beta o algo similar.
En los fundamentos matemáticos de la teoría de tipos, los setoides se pueden utilizar en una teoría de tipos que carece de tipos de cocientes para modelar conjuntos matemáticos generales. Por ejemplo, en la teoría de tipos intuicionista de Per Martin-Löf , no existe ningún tipo de números reales , sólo un tipo de secuencias regulares de Cauchy de números racionales . Por lo tanto, para hacer un análisis real en el marco de Martin-Löf, uno debe trabajar con un setoide de números reales, el tipo de secuencias regulares de Cauchy equipadas con la noción habitual de equivalencia. Es necesario definir predicados y funciones de números reales para secuencias regulares de Cauchy y demostrar que son compatibles con la relación de equivalencia. Normalmente (aunque depende de la teoría de tipos utilizada), el axioma de elección se aplicará a funciones entre tipos (funciones intensionales), pero no a funciones entre setoides (funciones extensionales). [ se necesita aclaración ] El término "conjunto" se utiliza de diversas formas como sinónimo de "tipo" o como sinónimo de "setoide". [2]
En matemáticas constructivas , a menudo se toma un setoide con una relación de separación en lugar de una relación de equivalencia, llamado setoide constructivo . A veces también se considera un setoide parcial utilizando una relación de equivalencia parcial o separación parcial (ver, por ejemplo, Barthe et al. , sección 1).
{{cite journal}}: Citar diario requiere |journal=( ayuda )