Autor Tema: Preguntas y referencias sobre distintos temas de lógica

0 Usuarios y 1 Visitante están viendo este tema.

12 Diciembre, 2020, 06:20 pm
Leído 1066 veces

alexpglez

  • $$\Large \color{#5e8d56}\pi\,\pi\,\pi$$
  • Mensajes: 162
  • País: es
  • Karma: +0/-0
  • Sexo: Masculino
Hola a todos!

Quería estudiar formalmente lógica, lógica de orden superior, teoría de tipos, teoría de categorías y teoría de conjuntos.

Hace tiempo empecé a leer un libro de teoría de categorías (lo dejé y no recuerdo el nombre) y se me hace duro que las categorías puedan ser clases propias, pues por experiencia, si uno no tiene cuidado puede llegar a contradicciones lógicas, y la mayoría de referencias que he visto no tienen mucho cuidado. Otra forma de explicar las categorías es como una teoría estructural y metamatemática, análogo a la teoría de conjuntos de Cantor que no terminó muy bien...

Por otra parte, la teoría de espacios vectoriales no tiene una formalización muy satisfactoria en la lógica de primer orden. Pues no hay manera de introducir los números reales y el producto en la propia teoría, a no ser que uno juegue con infinitas funciones [texx] \mu_{\lambda}v:=\lambda v [/texx] pero ésto es muy artificial y con poco poder expresivo. Pensé, "uno podría hacer una teoría variables tipo [texx] \mathbb R [/texx] y tipo [texx] V [/texx] y funciones mixtas". Entonces, ¿es ésta construcción una teoría de tipos?

También me interesan las teorías lógicas de orden superior. De hecho, ¿no se podrían embeber en una teoría de tipos considerando variables tipo funciones y la operación natural [texx] f\cdot a:=f(a) [/texx]?

Por último me gustaría ver la relación de la lógica con la teoría de categorías y los conjuntos. En concreto, ¿existe una teoría lógica (basada en tipos seguramente) que formalice la teoría de categorías y permita construir la categoría de los conjuntos (cumpliendo la axiomática de ZFC o NBG)?

Imagino que la última pregunta no está actualmente resuelta. (De estar resuelta sería fácil de googlear)

Muchas gracias


12 Diciembre, 2020, 11:57 pm
Respuesta #1

geómetracat

  • Moderador Global
  • Mensajes: 2,303
  • País: es
  • Karma: +0/-0
  • Sexo: Masculino
Antes de nada un "disclaimer": mis conocimientos sobre estas cosas son limitados, pero son temas que me han interesado y me interesan, así que algo puedo decir. Pero puede que meta la pata o diga algo falso.

Hace tiempo empecé a leer un libro de teoría de categorías (lo dejé y no recuerdo el nombre) y se me hace duro que las categorías puedan ser clases propias, pues por experiencia, si uno no tiene cuidado puede llegar a contradicciones lógicas, y la mayoría de referencias que he visto no tienen mucho cuidado.

Mi consejo es que no te preocupes demasiado sobre eso. No creo que ningún libro elemental (y pocos libros avanzados) preste mucha atención a temas de tamaño o conjuntista, pero puedes estar bien tranquilo que todos los resultados que salgan en esos libros son ciertos y han sido comprobados muchas veces. De todas formas, las únicas sutilezas conjuntistas en teoría de categorías es con el tema de los tamaños, y cuando sabes de qué va es muy fácil ver cómo podrías formalizar los resultados o cuando necesitas restringirte a conjuntos o puedes trabajar con clases propias.

Para la gran mayoría de cosas en teoría de categorías básica, lo único que necesitas es la distinción entre categorías pequeñas (los objetos son un conjunto) y grandes (los objetos son una clase propia). En contadas ocasiones se necesitan más de dos niveles. Esro se formaliza con los llamados universos de Grothendieck, pero viene a ser equivalente a considerar ZFC+existen \( \omega \) cardinales fuertemente inaccesibles \( \kappa_1<\kappa_2<\kappa_3<\dots \). Entonces las categorías "pequeñas" serían aquellas en que la clase de objetos tiene cardinalidad menor que \[ \kappa_1 \], las "grandes" las que tienen cardinalidad entre \( \kappa_1 \) y \( \kappa_2 \), las "muy grandes" las que tienen cardinalidad entre \( \kappa_2 \) y \( \kappa_3 \), etc.

Si te interesan los asuntos conjuntistas en categorías, lo mejor que he visto es este paper de Miie Shulman. Pero si sabes poco de teoría de categorías puede que sea ilegible.

Citar
Otra forma de explicar las categorías es como una teoría estructural y metamatemática, análogo a la teoría de conjuntos de Cantor que no terminó muy bien...
Bueno, terminó bastante bien diría yo, teniendo en cuenta que una axiomatización (ZFC) es la teoría que se suele considerar como fundamentación de las matemáticas. De igual manera, puedes formalizar la teoría de categorías en lógica de primer orden sin muchos problemas.

Citar
Por otra parte, la teoría de espacios vectoriales no tiene una formalización muy satisfactoria en la lógica de primer orden. Pues no hay manera de introducir los números reales y el producto en la propia teoría, a no ser que uno juegue con infinitas funciones [texx] \mu_{\lambda}v:=\lambda v [/texx] pero ésto es muy artificial y con poco poder expresivo. Pensé, "uno podría hacer una teoría variables tipo [texx] \mathbb R [/texx] y tipo [texx] V [/texx] y funciones mixtas". Entonces, ¿es ésta construcción una teoría de tipos?

Lo que describes se suele llamar "many-sorted logic" (no sé cómo se suele traducir al castellano). Es una extensión sencilla de la lógica de primer orden. También se puede ver como una teoría de tipos (al igual que la lógica usual de primer orden se puede ver como una teoría de tipos).

Citar
También me interesan las teorías lógicas de orden superior. De hecho, ¿no se podrían embeber en una teoría de tipos considerando variables tipo funciones y la operación natural [texx] f\cdot a:=f(a) [/texx]?
Así tal como lo dices parece algo naïf. La lógica de orden superior está muy relacionada con las teorías de conjuntos y con las teorías de tipos dependientes. Y ambas están relacionadas con los topos elementales (un tipo especial de categoría que se puede ver como un "universo" para hacer matemáticas). Básicamente la idea es que si tienes un tipo \( A \), variables de segundo orden son las de tipo \( PA \), donde \( PA \) es análogo al conjunto potencia de \( A \), hace el papel de subconjuntos de \( A \). Pero los detalles no son tan sencillos como añadir para cada tipo otro que corresponda con sus subconjuntos, hay que hacerlo con cuidado.

Citar
Por último me gustaría ver la relación de la lógica con la teoría de categorías y los conjuntos.
Buf, muchísimas. Hay todo un campo que se llama "lógica categorial" que se dedica a mirar la lógica desde el punto de vista categorial. Esto puede significar muchas cosas. Por ejemplo, puedes ver la lógica de primer orden desde el punto de vista categorial, de manera que las teorías lógicas acaban siendo un tipo de categoría (la llamada categoría sintáctica de la teoría) y los modelos acaban siendo funtores contravariantes de la categoría sintáctica a Set. Visto así, puedes extender el alcance de la teoría de modelos considerando "modelos en C", donde C es una categoría arbitraria.

Otro tema es la relación entre teorías de tipos, categorías y computación. A la visión de qie estas tres cosas son esencialmente lo mismo se le llama "trinitarianismo computacional". Las teorías de tipos se pueden ver como el lenguaje interno de ciertas clases de categorías. De manera que en estas clases de categorías puedes razonar de dos formas equivalentes: externamente, con diagramas, o internamente, con las reglas de una teoría de tipos. Esto ha llevado a desarrollos muy interesantes últimamente, como la teoría homotópica de tipos (homotopy type theory), que es un tipo de teoría de tipos dependiente donde los tipos se puedeb interpretar como "tipos de homotopía" (o más precisamente, \[ \infty \]-grupoides), y resulta ser el lenguaje interno de los \[ \infty \]-topos (si no has oido hablar de nada de esto, puedes olvidarlo).

Otra relación entre categorías y teoróas de conjuntos son las llamadas teorías de conjuntos estructurales, que son formas de recuperar la categoría Set a partir de categorías. Lo más famoso de esto es la ETCS (elementary theory of the category of sets), que se basa en dar una formulación axiomática de Set como un topos elemental que cumple unas ciertas condiciones adicionales.

Citar
En concreto, ¿existe una teoría lógica (basada en tipos seguramente) que formalice la teoría de categorías y permita construir la categoría de los conjuntos (cumpliendo la axiomática de ZFC o NBG)?

Esta pregunta no sé muy bien cómo interpretarla. En cualquier caso yo diría que sí. Puedes formalizar la teoría de categorías en lógica de primer orden si quieres (o en una teoría de tipos dependientes), y luego construir Set usando el enfoque de ETCS del que hablaba antes.

En fin, no sé si este mensaje te aclarará algo o te liará aún más. Espero que te sirva.
La ecuación más bonita de las matemáticas: \( d^2=0 \)

13 Diciembre, 2020, 03:57 pm
Respuesta #2

alexpglez

  • $$\Large \color{#5e8d56}\pi\,\pi\,\pi$$
  • Mensajes: 162
  • País: es
  • Karma: +0/-0
  • Sexo: Masculino
Hola geómetracat!
Gracias por tu respuesta. Me puse a googlear y me ha servido bastante en cuanto a lógica (aunque en teoría de categorías he encontrado poco).
Mi consejo es que no te preocupes demasiado sobre eso. No creo que ningún libro elemental (y pocos libros avanzados) preste mucha atención a temas de tamaño o conjuntista, pero puedes estar bien tranquilo que todos los resultados que salgan en esos libros son ciertos y han sido comprobados muchas veces. De todas formas, las únicas sutilezas conjuntistas en teoría de categorías es con el tema de los tamaños, y cuando sabes de qué va es muy fácil ver cómo podrías formalizar los resultados o cuando necesitas restringirte a conjuntos o puedes trabajar con clases propias.
La sensación que me da es muy similar a cuándo en 1º de carrera te introducen la teoría de conjuntos de forma intuitiva, en dónde parece que la construcción de la clase de Russel es un conjunto. Pero peor, porque en su momento leí a Carlos Ivorra y sabía qué era lo que fallaba de lo que me estaban contando y cómo se axiomatiza bien. Y sin embargo con teoría de categorías no sé cómo ponerme formal.
Es equivalente a que en análisis te digan "la integral es un concepto fundamental y las propiedades de la integral son éstas", pero no te definan "¿qué es una integral?" o "¿qué funciones son integrables?". Yo no puedo trabajar con cosas que no están muy bien definidas, sin reglas de inferencia formales que permitan entender qué es una demostración en teoría de categorías.

Para la gran mayoría de cosas en teoría de categorías básica, lo único que necesitas es la distinción entre categorías pequeñas (los objetos son un conjunto) y grandes (los objetos son una clase propia). En contadas ocasiones se necesitan más de dos niveles. Esro se formaliza con los llamados universos de Grothendieck, pero viene a ser equivalente a considerar ZFC+existen \( \omega \) cardinales fuertemente inaccesibles \( \kappa_1<\kappa_2<\kappa_3<\dots \). Entonces las categorías "pequeñas" serían aquellas en que la clase de objetos tiene cardinalidad menor que \[ \kappa_1 \], las "grandes" las que tienen cardinalidad entre \( \kappa_1 \) y \( \kappa_2 \), las "muy grandes" las que tienen cardinalidad entre \( \kappa_2 \) y \( \kappa_3 \), etc.

Si te interesan los asuntos conjuntistas en categorías, lo mejor que he visto es este paper de Miie Shulman. Pero si sabes poco de teoría de categorías puede que sea ilegible.
Gracias! Aunque me parece muy artificial esta distinción. En la teoría NBG, la clase de funciones entre clases propias es vacía (pues ninguna función entre clases puede ser un conjunto), son de las cosas por las que entiendo que hay que tener mucho cuidado.
Yo estaba pensando en considerar la teoría de categorías como algo superior a los conjuntos y las clases. Algunas categorías podrían ser conjuntos o clases propias, pero no necesariamente. Así eliminar estas construcciones artificiales que aparecen porque la teoría de conjuntos no se pensó para formalizar estas ideas.

Citar
Otra forma de explicar las categorías es como una teoría estructural y metamatemática, análogo a la teoría de conjuntos de Cantor que no terminó muy bien...
Bueno, terminó bastante bien diría yo, teniendo en cuenta que una axiomatización (ZFC) es la teoría que se suele considerar como fundamentación de las matemáticas. De igual manera, puedes formalizar la teoría de categorías en lógica de primer orden sin muchos problemas.
Bueno, a posteriori se eliminaron las paradojas y culminó en las teorías ZFC y NBG. Pero la teoría de Cantor estaba plagada de paradojas, que es a lo que me refería: si uno no tiene cuidado podría plagar la teoría de categorías de paradojas.

Lo que describes se suele llamar "many-sorted logic" (no sé cómo se suele traducir al castellano). Es una extensión sencilla de la lógica de primer orden. También se puede ver como una teoría de tipos (al igual que la lógica usual de primer orden se puede ver como una teoría de tipos).
Pues he redescubierto sin querer un tipo de lógica que no conocía  ;D, aunque pensé que eso era teoría de tipos, ¿qué es un teoría de tipos entonces?
He estado googleando y he encontrado un hilo de math stackexchange titulado "Is many sorted logic really a unifying logic?". Parece que en cierto sentido esta teoría unifica las demás, aunque no en todo su potencial. Menciona un libro donde explica teorías lógicas de orden superior y tipos, para después intentar unificarlos en many sorted logic. Creo que cuando tenga tiempo lo empezaré a leer.

Buf, muchísimas. Hay todo un campo que se llama "lógica categorial" que se dedica a mirar la lógica desde el punto de vista categorial. Esto puede significar muchas cosas. Por ejemplo, puedes ver la lógica de primer orden desde el punto de vista categorial, de manera que las teorías lógicas acaban siendo un tipo de categoría (la llamada categoría sintáctica de la teoría) y los modelos acaban siendo funtores contravariantes de la categoría sintáctica a Set. Visto así, puedes extender el alcance de la teoría de modelos considerando "modelos en C", donde C es una categoría arbitraria.

Otro tema es la relación entre teorías de tipos, categorías y computación. A la visión de qie estas tres cosas son esencialmente lo mismo se le llama "trinitarianismo computacional". Las teorías de tipos se pueden ver como el lenguaje interno de ciertas clases de categorías. De manera que en estas clases de categorías puedes razonar de dos formas equivalentes: externamente, con diagramas, o internamente, con las reglas de una teoría de tipos. Esto ha llevado a desarrollos muy interesantes últimamente, como la teoría homotópica de tipos (homotopy type theory), que es un tipo de teoría de tipos dependiente donde los tipos se puedeb interpretar como "tipos de homotopía" (o más precisamente, \[ \infty \]-grupoides), y resulta ser el lenguaje interno de los \[ \infty \]-topos (si no has oido hablar de nada de esto, puedes olvidarlo).

Otra relación entre categorías y teoróas de conjuntos son las llamadas teorías de conjuntos estructurales, que son formas de recuperar la categoría Set a partir de categorías. Lo más famoso de esto es la ETCS (elementary theory of the category of sets), que se basa en dar una formulación axiomática de Set como un topos elemental que cumple unas ciertas condiciones adicionales.

Citar
En concreto, ¿existe una teoría lógica (basada en tipos seguramente) que formalice la teoría de categorías y permita construir la categoría de los conjuntos (cumpliendo la axiomática de ZFC o NBG)?

Esta pregunta no sé muy bien cómo interpretarla. En cualquier caso yo diría que sí. Puedes formalizar la teoría de categorías en lógica de primer orden si quieres (o en una teoría de tipos dependientes), y luego construir Set usando el enfoque de ETCS del que hablaba antes.
¿Sabes de algún buen libro dónde se expliquen los ECTS y la lógica categorial? Yo lo que preguntaba era sobre la ECTS, la lógica categorial me recuerda a considerar un grupo en una categoría general (grupo en la categoría de Set es el grupo usual, en topología serían los grupos topológicos, en variedades los grupos de Lie, etc, aunque no conozco más ejemplos), parece muy interesante y potente.

En fin, no sé si este mensaje te aclarará algo o te liará aún más. Espero que te sirva.
¡Sí!, me ha servido mucho, sobretodo conocer la many sorted logic. Me interesa el libro que encontré que te mencionaba antes.

¡Muchas gracias!

Ps: el libro de categorías que empecé a leer si no recuerdo mal era de McLane Categories for the working mathematician.

Ps2: Estaba pensando que también se puede pensar una categoría como un grafo dirigido. Mmm

13 Diciembre, 2020, 05:21 pm
Respuesta #3

geómetracat

  • Moderador Global
  • Mensajes: 2,303
  • País: es
  • Karma: +0/-0
  • Sexo: Masculino
La sensación que me da es muy similar a cuándo en 1º de carrera te introducen la teoría de conjuntos de forma intuitiva, en dónde parece que la construcción de la clase de Russel es un conjunto. Pero peor, porque en su momento leí a Carlos Ivorra y sabía qué era lo que fallaba de lo que me estaban contando y cómo se axiomatiza bien. Y sin embargo con teoría de categorías no sé cómo ponerme formal.
Es equivalente a que en análisis te digan "la integral es un concepto fundamental y las propiedades de la integral son éstas", pero no te definan "¿qué es una integral?" o "¿qué funciones son integrables?". Yo no puedo trabajar con cosas que no están muy bien definidas, sin reglas de inferencia formales que permitan entender qué es una demostración en teoría de categorías.
No sé, me da la sensación de que no enfocas el estudio de la teoría de categorías correctamente. La teoría de categorías no es distinta de la teoría de grupos o cualquier otra teoría matemática estándar. Quiero decir, el planteamiento estándar es que trabajas en NBG o en ZFC y das unos axiomas para las categorías (una clase propia de objetos y otra de flechas, con una operación de composición, que cumplen una serie de condiciones, como la existencia de identidades y la asociatividad de la composición). Esto es análogo a cuando defines un grupo vía los axiomas. En particular no sé a qué te refieres con qué es una demostración en teoría de categorías. Una demostración en teoría de categorías es lo mismo que una demostración en teoría de conjuntos o en lógica formal. Se siguen las mismas reglas de la lógica de primer orden y de la teoría de conjuntos. No hay ninguna diferencia esencial con una demostración en teoría de conjuntos.

Otra cosa es si quieres considerar la teoría de conjuntos como una teoría fundacional. Entonces, puedes dar directamente los axiomas en lógica de primer orden (o en una teoría de tipos) y trabajar directamente con ellos, al igual que trabajarías con cualquier teoría de primer orden. En principio no debería dar ningún problema.

Citar
Gracias! Aunque me parece muy artificial esta distinción. En la teoría NBG, la clase de funciones entre clases propias es vacía (pues ninguna función entre clases puede ser un conjunto), son de las cosas por las que entiendo que hay que tener mucho cuidado.
Yo estaba pensando en considerar la teoría de categorías como algo superior a los conjuntos y las clases. Algunas categorías podrían ser conjuntos o clases propias, pero no necesariamente. Así eliminar estas construcciones artificiales que aparecen porque la teoría de conjuntos no se pensó para formalizar estas ideas.
En la versión que dí de ZFC + cardinales inaccesibles no hay problemas de clases propias porque todo son conjuntos. En NBG hay que ir con más cuidado pero puedes hacerlo todo igual. Te puedo asegurar que no encontrarás contradicciones lógicas en los libros de categorías. Por ejemplo, la clase de funciones entre clases propias es vacía en NBG, pero puedes definir clases propias que sean funciones entre clases propias en NBG sin problemas. Lo único que no puedes hacer es agruparlas todas en una clase. Este tipo de cosas hace que tratar con clases propias sea algo pesado, pero todo se puede traducir si es necesario de manera más o menos rutinaria.

Citar
Bueno, a posteriori se eliminaron las paradojas y culminó en las teorías ZFC y NBG. Pero la teoría de Cantor estaba plagada de paradojas, que es a lo que me refería: si uno no tiene cuidado podría plagar la teoría de categorías de paradojas.
Sí, pero es que la teoría de categorías no es para nada análoga a la teoría de conjuntos de Cantor. Es una teoría igual que la de grupos, tienes unos axiomas y es fácil producir modelos de categorías en ZFC o en NBG (que es en lo que uno piensa normalmente). Así que no hay problemas lógicos de consistencia.

Citar
Pues he redescubierto sin querer un tipo de lógica que no conocía  ;D, aunque pensé que eso era teoría de tipos, ¿qué es un teoría de tipos entonces?
Bueno, teorías de tipos hay muchísimas de muchos estilos distintos. No sé si hay una definición general que cubra todos los casos. Al menos yo nunca la he visto. En teoría de tipos tienes variables "tipos": \( A,B,C, \dots \), variables "términos" (donde cada término es de algún tipo) \( a:A \) (\( a \) es un término del tipo \( A \)) y tienes una serie de operaciones para construir tipos a partir de otros tipos y términos del nuevo tipo a partir de otros términos de los tipos. El esquema que sigue esto siempre es el mismo. Por poner un ejemplo, podemos considerar tipos producto. Dados dos tipos \( A,B \) se postula la existencia de un tipo producto \( A \times B \). Además se da una regla de introducción: dados \( a:A, b:B \) existe un término \( \langle a, b \rangle : A \times B \), y reglas de eliminación: dado \( z: A \times B \) hay términos \( \pi_1(z):A \) y \( \pi_2(z):B \). Finalmente, hay una regla de computación que dice lo que pasa cuando introduces y después eliminas: si \( a:A, b:B \) entonces \( \pi_1(\langle a,b \rangle)=a \) y \( \pi_2(\langle a,b \rangle)=b \).
Si lo miras bien, esto es exactamente la propiedad universal del producto de dos objetos en una categoría, lo que da una idea de por qué las teorías de tipos y la teoría de categorías están tan relacionadas.

Según las operaciones (como el producto en el ejemplo anterior) que consideres tendrás una teoría de tipos u otra. En este sentido es muy modular, puedes ir poniendo las operaciones que quieras. Además, esta es la teoría de tipos simple, hay cosas más complicadas como teorías de tipos dependiente donde puedes tener tipos que dependen de términos de otro tipo, o teorías de tipos polimórficas donde tienes tipos que dependen de otros tipos.

Visto así, en realidad la teoría de tipos es parecido a un híbrido entre lógica y teoría de conjuntos. Puedes pensar en cierta manera un tipo \( A \) como un conjunto y un término \( a:A \) como un elemento de un conjunto. Pero también puedes ver los tipos como proposiciones lógicas y los términos como demostraciones, y así la teoría de tipos se puede ver como "proof-relevant logic", una versión de la lógica donde se tiene en cuenta no solamente las proposiciones lógicas sino también el hecho de que pueden tener distintas demostraciones.

Así pues hay una diferencia fundamental con el enfoque clásico donde hay dos niveles bien separados: una base de lógica de primer orden y encima de ella una teoría de conjuntos como ZFC. En las teorías de tipos todo está más mezclado: son la base lógica pero a la vez ellas mismas funcionan como si fueran teorías de conjuntos.

Citar
He estado googleando y he encontrado un hilo de math stackexchange titulado "Is many sorted logic really a unifying logic?". Parece que en cierto sentido esta teoría unifica las demás, aunque no en todo su potencial. Menciona un libro donde explica teorías lógicas de orden superior y tipos, para después intentar unificarlos en many sorted logic. Creo que cuando tenga tiempo lo empezaré a leer.
La verdad es que no tengo ni idea de esto pero se ve interesante. Yo solo he encontrado many-sorted logics como una extensión un tanto intrascendente de la lógica de primer orden.

Citar
¿Sabes de algún buen libro dónde se expliquen los ECTS y la lógica categorial? Yo lo que preguntaba era sobre la ECTS, la lógica categorial me recuerda a considerar un grupo en una categoría general (grupo en la categoría de Set es el grupo usual, en topología serían los grupos topológicos, en variedades los grupos de Lie, etc, aunque no conozco más ejemplos), parece muy interesante y potente.
No conozco muchas referencias sobre ETCS, aunque aquí tienes una cuantas. Es recomendable por eso saber unas cuantas cosas sobre categorías en general antes de meterse con esto, creo. También estaría bien aprender algo de teoría de topos, que es una de las partes que más entroncan con lógica de la teoría de categorías. Sobre lógica categorial en general, como ya dije es muy amplia y se usa el término para referirse a cosas muy distintas. Para la historia de teorías de primer orden como categorías y modelos como funtores, están muy bien los primeros temas del curso de Jacob Lurie sobre lógica categorial, que puedes encontrar aquí.

Citar
Ps: el libro de categorías que empecé a leer si no recuerdo mal era de McLane Categories for the working mathematician.
Pues este diría que es de los que hace más comentarios fundacionales, así que imagínate los demás.  ;D

Citar
Ps2: Estaba pensando que también se puede pensar una categoría como un grafo dirigido. Mmm

Sí, claro. Una categoría es básicamente un multigrafo dirigido junto con la información de la composición (qué arista es la composición de dos dadas). Creo recordar que en el libro de MacLane está bien explicada la relación. Pero no sé muy bien a dónde quieres ir a parar con esto.
La ecuación más bonita de las matemáticas: \( d^2=0 \)

13 Diciembre, 2020, 08:02 pm
Respuesta #4

alexpglez

  • $$\Large \color{#5e8d56}\pi\,\pi\,\pi$$
  • Mensajes: 162
  • País: es
  • Karma: +0/-0
  • Sexo: Masculino
Hola!
No sé, me da la sensación de que no enfocas el estudio de la teoría de categorías correctamente. La teoría de categorías no es distinta de la teoría de grupos o cualquier otra teoría matemática estándar.
No le he prestado la atención que se merece a la teoría, más que en contadas aplicaciones que he necesitado. Cuando me ponga a estudiarla en serio ya preguntaré más en concreto, y seré muy tiquismiquis con las posibles contradicciones lógicas que encuentre.

Otra cosa es si quieres considerar la teoría de conjuntos como una teoría fundacional. Entonces, puedes dar directamente los axiomas en lógica de primer orden (o en una teoría de tipos) y trabajar directamente con ellos, al igual que trabajarías con cualquier teoría de primer orden. En principio no debería dar ningún problema.
Es un buen punto a observar. La pregunta en concreto sería, ¿tanto en ZFC+cardinales innaccesibles como en una teoría de categorías se puede demostrar la consistencia de la otra teoría?
Entiendo que me afirmas que sí, y que con NBG+algo también aunque hay que tener más cuidado.

En la versión que dí de ZFC + cardinales inaccesibles no hay problemas de clases propias porque todo son conjuntos. En NBG hay que ir con más cuidado pero puedes hacerlo todo igual. Te puedo asegurar que no encontrarás contradicciones lógicas en los libros de categorías. Por ejemplo, la clase de funciones entre clases propias es vacía en NBG, pero puedes definir clases propias que sean funciones entre clases propias en NBG sin problemas. Lo único que no puedes hacer es agruparlas todas en una clase. Este tipo de cosas hace que tratar con clases propias sea algo pesado, pero todo se puede traducir si es necesario de manera más o menos rutinaria.
Creo que ya entiendo intuitivamente lo de los cardinales innaccesibles. Si tienes una teoría de un cardinal inaccesible te aseguras que las posibles operaciones de categorías como producto, potencia, pullback, etc. estén dentro de la categoría. No puedes considerar la categoría de todos los conjuntos, pero sí la de conjuntos arbitrariamente grandes (y probablemente con muchas otras categorías). Y al ser todas las categorías conjuntos no hay problema en hablar de conjuntos de funtores o cosas así (como si habría problema si fuesen clases propias). Esto me recuerda a los universos de Grothendieck. (Edito: no me fijé que me habías hablado de ellos en tu primer mensaje).
No me gusta éste approach (pues no permite hablar de la categoría de todos los conjuntos), pero he de reconocer que es muy ingenioso. Y seguro que como afirmas, permite modelizar la teoría de categorías en la teoría de conjuntos.
Tampoco me gustan los modelos numerables de la teoría de conjuntos, pero es obvio que existen y no es bueno ignorarlos ;D.

Edito: Según wikipedia ciertos conjuntos de cardinales inaccesibles son modelos de ZFC. Por paradójico que sea ésto, la teoría de categorías se podría formalizar en ZFC+cardinales inaccesibles, y dentro de ésta se podría formalizar ZFC como una categoría de cardinal inaccesible... según entiendo. Resumiendo: no parece anecdótica la construcción de categorías basada en cardinales inaccesibles.

Bueno, teorías de tipos hay muchísimas de muchos estilos distintos. No sé si hay una definición general que cubra todos los casos. Al menos yo nunca la he visto. En teoría de tipos tienes variables "tipos": \( A,B,C, \dots \), variables "términos" (donde cada término es de algún tipo) \( a:A \) (\( a \) es un término del tipo \( A \)) y tienes una serie de operaciones para construir tipos a partir de otros tipos y términos del nuevo tipo a partir de otros términos de los tipos. El esquema que sigue esto siempre es el mismo. Por poner un ejemplo, podemos considerar tipos producto. Dados dos tipos \( A,B \) se postula la existencia de un tipo producto \( A \times B \). Además se da una regla de introducción: dados \( a:A, b:B \) existe un término \( \langle a, b \rangle : A \times B \), y reglas de eliminación: dado \( z: A \times B \) hay términos \( \pi_1(z):A \) y \( \pi_2(z):B \). Finalmente, hay una regla de computación que dice lo que pasa cuando introduces y después eliminas: si \( a:A, b:B \) entonces \( \pi_1(\langle a,b \rangle)=a \) y \( \pi_2(\langle a,b \rangle)=b \).
Si lo miras bien, esto es exactamente la propiedad universal del producto de dos objetos en una categoría, lo que da una idea de por qué las teorías de tipos y la teoría de categorías están tan relacionadas.

Según las operaciones (como el producto en el ejemplo anterior) que consideres tendrás una teoría de tipos u otra. En este sentido es muy modular, puedes ir poniendo las operaciones que quieras. Además, esta es la teoría de tipos simple, hay cosas más complicadas como teorías de tipos dependiente donde puedes tener tipos que dependen de términos de otro tipo, o teorías de tipos polimórficas donde tienes tipos que dependen de otros tipos.

Visto así, en realidad la teoría de tipos es parecido a un híbrido entre lógica y teoría de conjuntos. Puedes pensar en cierta manera un tipo \( A \) como un conjunto y un término \( a:A \) como un elemento de un conjunto. Pero también puedes ver los tipos como proposiciones lógicas y los términos como demostraciones, y así la teoría de tipos se puede ver como "proof-relevant logic", una versión de la lógica donde se tiene en cuenta no solamente las proposiciones lógicas sino también el hecho de que pueden tener distintas demostraciones.

Así pues hay una diferencia fundamental con el enfoque clásico donde hay dos niveles bien separados: una base de lógica de primer orden y encima de ella una teoría de conjuntos como ZFC. En las teorías de tipos todo está más mezclado: son la base lógica pero a la vez ellas mismas funcionan como si fueran teorías de conjuntos.
Mmm, es una generalización bastante grande de la lógica de primer orden. No sé como puede casar en una many sorted logic como creo que se afirmaba en el enlace que te he pasado (sino más bien parece una generalización, pudiendo crear tipos nuevos de unos básicos). Cuando lo estudie preguntaré, no puedo hacer muchas preguntas   :laugh:.

Sí, claro. Una categoría es básicamente un multigrafo dirigido junto con la información de la composición (qué arista es la composición de dos dadas). Creo recordar que en el libro de MacLane está bien explicada la relación. Pero no sé muy bien a dónde quieres ir a parar con esto.
Lo observaba por dos motivos: pedagógicamente igual está bien entender las categorías como grafos, y quizá entendiendo grafos se pueden entender mejor categorías (hasta utilizarse en teoremas) y viceversa.

Y muchas gracias por las referencias, me las apunto para leerlas cuando saque tiempo.

13 Diciembre, 2020, 10:12 pm
Respuesta #5

geómetracat

  • Moderador Global
  • Mensajes: 2,303
  • País: es
  • Karma: +0/-0
  • Sexo: Masculino
No le he prestado la atención que se merece a la teoría, más que en contadas aplicaciones que he necesitado. Cuando me ponga a estudiarla en serio ya preguntaré más en concreto, y seré muy tiquismiquis con las posibles contradicciones lógicas que encuentre.
Pues ya dirás. Pero me juego lo que quieras a que no encontrarás ninguna contradicción lógica en la teoría. Y si la encuentras, te harás muy muy famoso.  ;)

Citar
Es un buen punto a observar. La pregunta en concreto sería, ¿tanto en ZFC+cardinales innaccesibles como en una teoría de categorías se puede demostrar la consistencia de la otra teoría?
Entiendo que me afirmas que sí, y que con NBG+algo también aunque hay que tener más cuidado.
A ver, aquí hay dos cosas. La teoría de categorías, entendiendo los axiomas básicos de una categoría es obviamente una teoría consistente pero muchísimo más débil que ZFC. Por ejemplo, un modelo es un único objeto con la aplicación identidad.

Otra cosa son axiomas para una categoría de conjuntos, como lo del ETCS. Eso es más interesante, y hay muchos resultados de equiconsistencia entre teorías de conjuntos usuales y estas categorías de conjuntos. Sobre esto, puedes mirar el artículo "Comparing material and structural set theories" de Mike Shulman.

De todas maneras, lo de usar clases propias o inaccesibles es básicamente para poder hablar de la categoría de todos los conjuntos (o todos los grupos, o todos los anillos, etc.). En principio podrías hacer teoría de categorías básica sin inaccesibles ni clases propias, si te restringes a trabajar con categorías pequeñas. Dicho de otra manera, los puntos peligrosos lógicamente hablando en teoría de categorías son debido a los peligros de la teoría de conjuntos, y no a nada intrínseco de las categorías.


Citar
Creo que ya entiendo intuitivamente lo de los cardinales innaccesibles. Si tienes una teoría de un cardinal inaccesible te aseguras que las posibles operaciones de categorías como producto, potencia, pullback, etc. estén dentro de la categoría. No puedes considerar la categoría de todos los conjuntos, pero sí la de conjuntos arbitrariamente grandes (y probablemente con muchas otras categorías). Y al ser todas las categorías conjuntos no hay problema en hablar de conjuntos de funtores o cosas así (como si habría problema si fuesen clases propias). Esto me recuerda a los universos de Grothendieck. (Edito: no me fijé que me habías hablado de ellos en tu primer mensaje).
No me gusta éste approach (pues no permite hablar de la categoría de todos los conjuntos), pero he de reconocer que es muy ingenioso. Y seguro que como afirmas, permite modelizar la teoría de categorías en la teoría de conjuntos.
Tampoco me gustan los modelos numerables de la teoría de conjuntos, pero es obvio que existen y no es bueno ignorarlos ;D.
Sí, los universos de Grothendieck es el formalismo más usado para tratar estas cosas, pero es equivalente a lo de los inaccesibles.

Sobre gustar o no gustar, es lo que hay. Es el precio a pagar para hablar de la categoría de todos los conjuntos y demás. No hay otra salida.
Los modelos numerables de la teoría de conjuntos puede que no te gusten, pero son una herramienta importantísima en teoría de conjuntos.

Citar
Edito: Según wikipedia ciertos conjuntos de cardinales inaccesibles son modelos de ZFC. Por paradójico que sea ésto, la teoría de categorías se podría formalizar en ZFC+cardinales inaccesibles, y dentro de ésta se podría formalizar ZFC como una categoría de cardinal inaccesible... según entiendo. Resumiendo: no parece anecdótica la construcción de categorías basada en cardinales inaccesibles.
Es un ejercicio típico en teoría de conjuntos demostrar que si \( \kappa \) es inaccesible, entonces \( V_\kappa \) es un modelo de ZFC. Se trata de ir comprobando que todos los axiomas se cumplen ahí (por ejemplo, si tienes un conjunto \( x \in V_\kappa \) entonces \( Px \in V_\kappa \) y cosas así. La definición de cardinal inaccesible te asegurs que nunca te vas a salir de \( V_\kappa \) haciendo las operaciones típicas a conjuntos de \( V_\kappa \).

Como ZFC + existe un inaccesible prueba la consistencia de ZFC, es una teoría estrictamente más fuerte que ZFC. Pero no conozco a nadie que crea que ZFC es consistente pero ZFC + un inaccesible (o una cantidad numerable de ellos) es inconsistente.

Citar
Mmm, es una generalización bastante grande de la lógica de primer orden. No sé como puede casar en una many sorted logic como creo que se afirmaba en el enlace que te he pasado (sino más bien parece una generalización, pudiendo crear tipos nuevos de unos básicos). Cuando lo estudie preguntaré, no puedo hacer muchas preguntas   :laugh:.
Sí, yo tampoco lo veo muy claro.

Citar
Lo observaba por dos motivos: pedagógicamente igual está bien entender las categorías como grafos, y quizá entendiendo grafos se pueden entender mejor categorías (hasta utilizarse en teoremas) y viceversa.

Y muchas gracias por las referencias, me las apunto para leerlas cuando saque tiempo.

Es interesante pero de alcance más bien limitado. El problema es que los enfoques son muy muy distintos. Por un lado, la teoría de grafos viene de la combinatoria y casi todo lo que se hace es para grafos finitos, mientras que la mayoría de categorías interesantes son infinitas. Por otro lado en teoría de categorías no interesa tanto el estudio de una categoría concreta sino relaciones entre varias (funtores y transformaciones naturales). Y el tipo de cosas por las que se preocupa la teoría de conjuntos es muy distinta del de la teoría de grafos.
La ecuación más bonita de las matemáticas: \( d^2=0 \)