En matemáticas, el topos efectivo introducido por Martin Hyland (1982) captura la idea matemática de efectividad dentro del marco teórico de categorías .
El topos se basa en el álgebra combinatoria parcial dada por el primer álgebra de Kleene . En la noción de realizabilidad recursiva de Kleene , a cualquier predicado se le asignan números realizadores, es decir, un subconjunto de . Las proposiciones extremas son y , realizadas por y . Sin embargo, en general, este proceso asigna más datos a una proposición que simplemente un valor de verdad binario.
Una fórmula con variables libres dará lugar a un mapa en cuyos valores se encuentra el subconjunto de realizadores correspondientes.
es un excelente ejemplo de un topos de realizabilidad . Se trata de una clase de topoi elementales con una lógica interna intuicionista y que cumplen una forma de elección dependiente . Generalmente no son topoi de Grothendieck.
En particular, el topos efectivo es . Se puede decir que la construcción de otros topos de realizabilidad abstrae algunos de los aspectos aquí interpretados.
Los objetos son pares de conjuntos juntos con una relación simétrica y transitiva en , representando una forma de predicado de igualdad, pero tomando valores en subconjuntos de . Se escribe con un solo argumento para denotar el llamado predicado de existencia, expresando cómo se relaciona uno consigo mismo. Esto puede estar vacío y por lo tanto la relación generalmente no es reflexiva . Las flechas representan clases de equivalencia de relaciones funcionales que respetan adecuadamente las igualdades definidas.
El clasificador asciende a . El par (o, por abuso de notación, solo ese conjunto de poderes subyacente) puede denotarse como . Una relación de vinculación la convierte en una preálgebra de Heyting . Tal contexto permite definir la estructura lógica similar a una red apropiada, con operaciones lógicas dadas en términos de operaciones de los conjuntos de realizadores, haciendo uso de pares y funciones computables.
El objeto terminal es un singleton con predicado de existencia trivial ( ). El producto finito respeta adecuadamente la igualdad. La igualdad del clasificador viene dada por equivalencias en su red.
Algunos objetos exhiben un predicado de existencia bastante trivial que depende sólo de la validez de la relación de igualdad " " de conjuntos, de modo que la igualdad válida se asigna al conjunto superior y la igualdad rechazada a . Esto da lugar a un functor completo y fiel fuera de la categoría de conjuntos , que tiene límites finitos conservando el functor de secciones globales como su adjunto izquierdo. Esto se factoriza a través de una incrustación fiel, completa y de preservación de límites finitos .
El topos tiene un objeto de números naturales con simplemente . Las oraciones verdaderas sobre son exactamente las oraciones realizadas recursivamente de la aritmética de Heyting .
Ahora las flechas pueden entenderse como las funciones recursivas totales y esto también es válido internamente para . Este último es el par dado por funciones recursivas totales y una relación tal que es el conjunto de códigos para . Este último es un subconjunto de los naturales pero no solo un singleton, ya que hay varios índices que calculan la misma función recursiva. Entonces aquí la segunda entrada de los objetos representa los datos de realización.
Con y funciones desde y hacia él, así como con reglas simples para las relaciones de igualdad en la formación de productos finitos , ahora se pueden definir de manera más amplia las operaciones hereditariamente efectivas. Nuevamente se puede pensar que las funciones en están dadas por índices y su igualdad está determinada por los objetos que calculan la misma función. Esta igualdad claramente impone una restricción a , ya que estas funciones resultan ser solo aquellas funciones computables que también respetan adecuadamente la igualdad mencionada en su dominio. Etcétera. Se debe respetar la situación general de igualdad (en el sentido de la 's) en dominio e imagen.
Con esto, se puede validar el principio de Markov y el principio extendido de la Iglesia (y una variante de segundo orden del mismo), que se reducen a una simple declaración sobre un objeto como o . Estos implican independencia de premisa .
Un principio de elección relacionado con la continuidad débil brouweriana falla. Desde cualquier objeto, solo hay un número contable de flechas hasta . cumple un principio de uniformidad. no es el coproducto contable de copias de . Este topos no es una categoría de gavillas.
El objeto es efectivo en un sentido formal y a partir de él se pueden definir secuencias de Cauchy computables . A través de un cociente, el topos tiene un objeto de números reales que no tiene un subobjeto decidible no trivial . Con elección, la noción de reales de Dedekind coincide con la de Cauchy.
El análisis aquí corresponde a la escuela recursiva del constructivismo. Rechaza la afirmación que sería válida para todos los reales . Las formulaciones del teorema del valor intermedio fallan y todas las funciones de reales a reales son comprobadamente continuas . Existe una secuencia de Specker y luego falla Bolzano-Weierstrass .
