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 la primera álgebra de Kleene . En la noción de Kleene de realizabilidad recursiva , a cualquier predicado se le asignan números realizables, es decir, un subconjunto de . Las proposiciones extremales son y , realizadas por y . Sin embargo, en general, este proceso asigna más datos a una proposición que solo un valor de verdad binario.
Una fórmula con variables libres dará lugar a un mapa en cuyos valores está el subconjunto de realizadores correspondientes.
es un excelente ejemplo de un topo de realizabilidad . Se trata de una clase de topos elementales con una lógica interna intuicionista y que cumplen una forma de elección dependiente . Por lo general, no son topos de Grothendieck.
En particular, el topos efectivo es . Se puede decir que otras construcciones de topos de realizabilidad abstraen algunos aspectos que se tienen en cuenta aquí.
Los objetos son pares de conjuntos que tienen una relación simétrica y transitiva en , lo que representa una forma de predicado de igualdad, pero que toma valores que son subconjuntos de . Se escribe con un solo argumento para denotar el llamado predicado de existencia, que expresa cómo se relaciona an consigo mismo. Este puede estar vacío, lo que expresa que la relación no es generalmente reflexiva . Las flechas equivalen a clases de equivalencia de relaciones funcionales que respetan adecuadamente las igualdades definidas.
El clasificador equivale a . El par (o, por abuso de notación, simplemente ese conjunto potencia subyacente) puede denotarse como . Una relación de implicación en lo convierte en un preálgebra de Heyting . Un contexto de este tipo permite definir la estructura lógica reticular adecuada, con operaciones lógicas dadas en términos de operaciones de los conjuntos realizadores, haciendo uso de pares y funciones computables.
El objeto terminal es un singleton con predicado de existencia trivial (es decir, igual a ). El producto finito respeta la igualdad de manera apropiada. La igualdad del clasificador se da a través de equivalencias en su red.
Algunos objetos presentan un predicado de existencia bastante trivial que depende únicamente de la validez de la relación de igualdad " " de los conjuntos, de modo que la igualdad válida se asigna al conjunto superior y la igualdad rechazada se asigna a . Esto da lugar a un funtor completo y fiel fuera de la categoría de conjuntos , que tiene el funtor de secciones globales que preservan límites finitos como su adjunto izquierdo. Esto se factoriza a través de una incrustación completa y fiel que preserva límites finitos - .
El topos tiene un objeto de números naturales con simplemente . Las oraciones verdaderas acerca de son exactamente las oraciones realizadas recursivamente de la aritmética de Heyting .
Ahora bien, las flechas pueden entenderse como las funciones recursivas totales y esto también se cumple internamente para . Este último es el par dado por las 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. Así que 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 al formar productos finitos , ahora se pueden definir de manera más amplia las operaciones hereditariamente efectivas. Nuevamente se puede pensar en funciones en como 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. La situación para , la igualdad (en el sentido de la 's) en el dominio y la imagen general debe respetarse.
Con esto, se puede validar el principio de Markov y el principio de Church extendido (y una variante de segundo orden del mismo), que se reducen a simples enunciados sobre objetos como o . Estos implican una independencia de premisa .
Un principio de elección relacionado con la continuidad débil de Brouwer falla. Desde cualquier objeto, solo hay una cantidad 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 haces.
El objeto es efectivo en sentido formal y a partir de él se pueden definir sucesiones de Cauchy computables . Mediante un cociente, el topos tiene un objeto de números reales que no tiene ningún 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 de que se cumpliría para todos los números reales . Las formulaciones del teorema del valor intermedio fallan y todas las funciones de los números reales a los reales son demostrablemente continuas . Existe una secuencia de Specker y luego falla la de Bolzano-Weierstrass .
