¿Es decidible la teoría de las categorías?

Question

Hay muchos teoremas del álgebra homológica básica, como el lema de los cinco o el lema de la serpiente, que parecen más fáciles de demostrar por ordenador que a mano. Esto me llevó a plantearme la siguiente cuestión: ¿es decidible la teoría de las categorías?

Más concretamente, me preguntaba si las declaraciones sobre abeliano Las categorías pueden determinarse como verdaderas o falsas en un tiempo finito. Además, si se puede determinar que son falsas, ¿es posible describir explícitamente un contraejemplo? Si se sabe que es decidible, ¿se sabe algo sobre la complejidad? (Otras teorías decidibles suelen tener complejidades de tiempo multiexponencial). Si se sabe que es indecidible, digamos que al incrustar el problema de detención, ¿puedo cambiar un poco mis suposiciones y hacerlo decidible? (Por ejemplo, tal vez no debería buscar categorías abelianas después de todo).

Gracias de antemano.

Editar : Parece que se necesita una aclaración. Mi objetivo era considerar la teoría mínima que podría estado cosas como el lema de los cinco, pero no necesariamente demostrarlas. Por ejemplo, quiero decir:

Si en una categoría abeliana, tienes un montón de mapas $0\to A \to B \to C\to 0$ y $0\to A' \to B' \to C'\to 0$ que componen dos cortas secuencias exactas y algunos mapas más $a:A\to A'$ , $b:B\to B'$ , $c:C\to C'$ que conmutan con los mapas anteriores, y $a$ y $c$ son isomorfismos, entonces $b$ también es un isomorfismo.

Las frases de esta forma serían entradas para un programa, que decide si esta afirmación es de hecho verdadera en ZFC (o su otra axiomatización favorita de la teoría de categorías). La cuestión aquí es que estoy restringiendo la frases uno puede introducir en el programa, pero manteniendo ZFC o lo que sea como marco.

Esperaba (quizás ingenuamente) que si restringía la clase de oraciones, podría ser decidible si estas afirmaciones eran verdaderas o no. Por ejemplo, imaginé que cada uno de estos teoremas se demuestra mediante la búsqueda de diagramas, o bien es posible encontrar un ejemplo concreto de mapas entre, digamos, módulos R que contradigan el resultado.

Answer 1

Gracias por aclarar su pregunta. La formulación que usted y Dorais dan parece perfectamente razonable. Usted tiene un lenguaje de primer orden para la teoría de la categoría, donde se puede cuantificar sobre objetos y morfismos, puedes componer morfismos de forma adecuada y se puede expresar que un objeto objeto es el objeto inicial o terminal de un morfismo morfismo. En este lenguaje, se pueden describir varios diagramas finitos finitos, expresar si son o no conmutativos, etc. etc. En particular, se puede expresar que la composición es asociativa, etc. y describir lo que significa ser una categoría de esta manera.

La pregunta ahora es: ¿es esta teoría decidible? En otras palabras, ¿existe un procedimiento computable para determinar dada una afirmación en este lenguaje, si es válida en todas las categorías?

La respuesta es No .

Una forma de ver esto es mostrar aún más: uno no puede ni siquiera decidir si una afirmación dada es verdadera es verdadera en todas categorías que tienen un solo objeto. La razón es que la teoría de grupos no es una teoría decidible. No hay un procedimiento computable computable para determinar si un enunciado dado en el lenguaje de primer orden de la teoría de grupos es verdadera en todos los grupos. Pero las categorías de un punto incluyen naturalmente todos los grupos (y podemos definir en un solo enunciado en el lenguaje lenguaje teórico de la categoría exactamente lo que se necesita para la colección de morfismos sobre ese objeto sea un grupo). Así, si pudiéramos decidir la teoría de categorías, entonces podríamos decidir las traducciones de las preguntas de la teoría de grupos a la teoría de la categoría, y seríamos capaces de decidir la teoría de que no podemos. Contradicción.

El obstáculo fundamental para la decidibilidad aquí, como mencioné en mi respuesta anterior (ver historial de ediciones), es la capacidad de codificar la aritmética. La noción de fuertemente indecidible estructura es clave para demostrar que varias teorías son indecidibles. A teoría fuertemente indecidible es una teoría finitamente axiomatizable axiomatizable de forma finita, tal que cualquier teoría consistente con ella es indecidible. Robinson demostró que existe una teoría fuertemente indecidible de la aritmética, conocida como la Q de Robinson. estructura fuertemente indecidible es una estructura que modela un teoría fuertemente indecidible. Estas estructuras son sorprendentes, porque cualquier teoría verdadera en una estructura fuertemente indecidible es indecidible. Por ejemplo, el modelo estándar de la aritmética, que satisface Q, es fuertemente indecidible. Si A es fuertemente indecidible y se interpreta en B, entonces se deduce que B también es fuertemente indecidible. Así, podemos demostrar que la teoría de grafos es indecidible, que la teoría de anillos es es indecidible y que la teoría de grupos es indecidible, simplemente encontrar un grafo, un anillo o un grupo en el que el número natural números naturales. Tarski encontró un grupo fuertemente indecidible grupo, a saber, el grupo G de permutaciones de los números enteros Z. Es fuertemente indecidible porque los números naturales pueden ser interpretados en este grupo. Básicamente, el número n está representado por la traslación por n. Se puede identificar la colección de traslaciones, como exactamente aquellas que conmutan con s = traslación-por-1. Entonces, se puede definir la suma como composición (es decir, adición de exponentes) y la relación es definible como: i divide a j si todo lo que conmuta con s i también conmuta con s j . Y así sucesivamente.

Afirmo de manera similar que hay una fuerte indecidible categoría. Esto es casi inmediato, ya que todo grupo puede como los morfismos de una categoría de un objeto, y el grupo se interpreta como los morfismos de esta categoría. Así, la categoría interpreta el grupo fuertemente indecidible y, por tanto, la categoría es también fuertemente indecidible. En En particular, cualquier teoría verdadera en la categoría es también indecidible. Así que la propia teoría de la categoría es indecidible.

Answer 2

Esta respuesta se basa en las de F. G. Dorais y Joel David Hamkins para responder a su "pregunta específica", la pregunta que ellos dejaron abierta, a saber, si la teoría de abeliano categorías es decidible.

La respuesta sigue siendo no .

Incluso la siguiente familia más limitada de problemas es indecidible:

Palabras dadas $r, r_1,\ldots,r_m$ en $x_1,\ldots,x_n$ (es decir, cada $r_i$ es un producto finito del $x_i$ y sus inversos), decida si es cierto que siempre que el $x_i$ se interpretan como automorfismos de un objeto $M$ en una categoría abeliana, $r_1=\cdots=r_m=1_M$ implica $r=1_M$ .

Si la respuesta a la instancia correspondiente del problema de palabras para grupos finitamente presentados es afirmativa, entonces la respuesta a esta pregunta de la categoría abeliana es afirmativa. A la inversa, si la respuesta a la instancia del problema de palabras es no, entonces podemos construir el grupo finitamente presentado $G = \langle x_1,\ldots,x_n | r_1,\ldots,r_m \rangle$ forman el anillo de grupo $\mathbb{Z}G$ y que $M$ sea $\mathbb{Z}G$ como un módulo sobre sí mismo, lo que demuestra que la respuesta a la pregunta sobre la categoría abeliana también es negativa.

Así que si hubiera un algoritmo para decidir esta familia de problemas de categorías abelianas, también habría un algoritmo para decidir el problema de la palabra para grupos finitamente presentados. Pero P. S. Novikov demostró en 1955 que este último algoritmo no existe.

Answer 3

La teoría de las categorías es indecidible. Por teoría de categorías entiendo la teoría con dos tipos Ob (objetos) y Ar (flechas) junto con las operaciones dom:Ar → Ob, cod:Ar → Ob, 1:Ob → Ar, y o:Ar×Ar→Ar (posiblemente composición parcial), y los axiomas obvios.

Una forma de ver esto es interpretar la teoría de los grupos -que es indecidible por un hermoso teorema de Trakhtenbrot- dentro de la teoría de las categorías punteadas, es decir, las categorías con un objeto distinguido * (que es una extensión no esencial). En efecto, la definible El conjunto de flechas invertibles de * a * forman un grupo, y todo grupo puede interpretarse como el conjunto de flechas de una categoría con * como único objeto. Sospecho que la teoría de las categorías abelianas tampoco es decidible, pero no he intentado demostrarlo (todavía).