Ilustraciones de teoría de categorías: lógica (2021)

 (abuseofnotation.github.io)
2 puntos por GN⁺ 2024-10-27 | 1 comentarios | Compartir por WhatsApp
  • La lógica parte de proposiciones atómicas aceptadas como verdaderas y construye proposiciones más grandes con operadores como and, or e implies; al igual que en teoría de categorías, la composición es clave.
  • La lógica clásica interpreta las proposiciones como valores Booleanos de verdadero/falso, y los operadores lógicos como funciones Booleanas, tratando negación, conjunción, disyunción, implicación y equivalencia mediante tablas de verdad.
  • La interpretación BHK de la lógica intuicionista ve las proposiciones como objetos que tienen demostraciones; A ∧ B se interpreta como un par de demostraciones y A → B como una función que transforma una demostración de A en una demostración de B.
  • En algunas categorías, los objetos corresponden a proposiciones y los morfismos a demostraciones; en teoría del orden esto aparece como un preorder o partial order donde A ≤ B significa A → B.
  • La lógica intuicionista corresponde, desde el punto de vista del orden, a una álgebra de Heyting, y en teoría de categorías general a una bicartesian closed category; la conjunción, disyunción, verdadero, falso e implicación corresponden respectivamente a meet/join, terminal/initial y exponential object.

Lógica que empieza con proposiciones

  • La lógica trata reglas formales consistentes consigo mismas, independientemente de la observación, y es un sistema para concluir o demostrar que algo es verdadero cuando se sabe otra cosa.
  • Una teoría matemática puede verse como lógica con definiciones adicionales.
    • La teoría de conjuntos puede definirse agregando a los axiomas lógicos estándar el concepto primitivo de relación de pertenencia a conjuntos.
  • Para comenzar con la lógica se necesita un conjunto inicial de proposiciones aceptadas como verdaderas o falsas.
    • A esto se le llama premisa, proposición atómica o primary proposition.
  • Dos o más proposiciones forman una sola proposición compuesta mediante operadores lógicos como and, or e implies/entails.
    • ∧ es and
    • ∨ es or
    • → significa follows o implicación
  • Las proposiciones compuestas también pueden volver a componerse con otras proposiciones, igual que las atómicas.

Modus ponens y tautologías

  • Modus ponens es un patrón lógico antiguo según el cual, si A es verdadera y A → B es verdadera, entonces B también es verdadera.
    • Su forma es (A ∧ (A ⇒ B)) → B
    • Puede expresarse con ejemplos como: “Si Sócrates es humano, y si todo humano muere, entonces Sócrates muere”.
  • La lógica no trata solo operaciones individuales, sino también combinaciones y relaciones entre varias operaciones lógicas.
    • La relación entre and e implies se ve en modus ponens.
    • La ley distributiva entre and y or también es un tema principal.
  • Una tautología es una proposición que siempre es verdadera sin importar los valores de verdad de las proposiciones que la componen.
    • En modus ponens, toda la fórmula es siempre verdadera, ya sea que A y B sean verdaderas o falsas.
    • Una proposición siempre falsa se llama contradicción.
    • Si se aplica not a una tautología se obtiene una contradicción, y si se aplica not a una contradicción se obtiene una tautología.
  • Las proposiciones cuyo valor cambia entre verdadero y falso según el caso se llaman contingent statement, y quedan fuera del interés principal de la lógica.
  • La tautología más simple es la ley de identidad, según la cual cada proposición se implica a sí misma.

Esquemas de axiomas y sistemas lógicos

  • Las tautologías sirven de base para los esquemas de axiomas y las reglas de inferencia.
  • Un esquema de axioma es una fórmula con marcadores de posición, que pueden sustituirse por proposiciones para obtener proposiciones concretas.
    • Si en modus ponens se quitan los colores o las proposiciones concretas, queda la estructura general.
    • Insertando proposiciones atómicas o compuestas en esa estructura se obtiene una instancia particular de modus ponens.
  • Las reglas de inferencia pueden escribirse casi del mismo modo que los esquemas de axiomas, y estos también pueden aplicarse como reglas de inferencia.
  • Toda tautología puede usarse como esquema de axioma.
  • Un sistema lógico o sistema formal es una colección de esquemas de axiomas y reglas de inferencia que, al aplicarse, generan todas las proposiciones posibles.
    • Como ejemplo se presenta un sistema compuesto por cinco esquemas de axiomas y la regla de inferencia modus ponens.
    • El hecho de que este tipo de sistema lógico sea completo se relaciona con el teorema de completitud de Gödel.

Interpretación veritativo-funcional de la lógica clásica

  • La lógica clásica se basa en la dicotomía de que toda proposición es o verdadera o falsa.
  • En la interpretación clásica, las proposiciones y operadores se definen así:
    • Las proposiciones son cosas que, como un valor Booleano, son verdaderas o falsas.
    • Los operadores lógicos son funciones que reciben uno o más valores Booleanos y devuelven un valor Booleano.
  • La negación ¬p es un operador unario que convierte verdadero en falso y falso en verdadero.
    • Lo mismo puede expresarse con una tabla de verdad.
    • La eliminación de la doble negación se demuestra diciendo que aplicar la negación dos veces devuelve el valor inicial.
  • and recibe dos valores Booleanos y devuelve verdadero solo si ambos son verdaderos.
    • p ∧ q → p
    • p ∧ q → q
  • or devuelve verdadero si al menos uno de los dos valores Booleanos es verdadero.
    • p → p ∨ q
    • q → p ∨ q
  • implies, o material condition, se escribe p → q y es falso solo cuando p es verdadero y q es falso.
    • En lógica clásica, p → q equivale al caso en que ¬p ∨ q es verdadero.
  • if and only if, o iff, es verdadero cuando dos proposiciones tienen el mismo valor.
    • P ↔ Q es equivalente a P → Q ∧ Q → P.
  • Además de con tablas de verdad, la equivalencia entre p → q y ¬p ∨ q también puede demostrarse con axiomas y reglas de inferencia.
    • Una demostración completa de equivalencia requiere demostrar ambas direcciones.

Lógica intuicionista e interpretación BHK

  • La lógica intuicionista considera la demostración no como descubrimiento de una verdad universal, sino como construcción.
  • Desde este punto de vista no puede usarse la dicotomía de que toda proposición es necesariamente verdadera o falsa.
    • Puede haber proposiciones que no sean demostrables no porque sean falsas, sino porque quedan fuera del alcance del sistema lógico dado.
    • La conjetura de los primos gemelos suele ponerse como ejemplo.
  • En la interpretación de Brouwer–Heyting–Kolmogorov (BHK), el centro no está en las proposiciones sino en las demostraciones.
    • Una proposición es algo que tiene una demostración.
    • Los operadores lógicos son construcciones que producen demostraciones a partir de otras demostraciones.
  • Una demostración de A ∧ B es un par formado por una demostración de A y una demostración de B, es decir, un product.
  • A → B significa que existe una función que transforma una demostración de A en una demostración de B.
    • El conjunto de demostraciones de A → B puede representarse como el conjunto de funciones de A a B, es decir, un hom-set.
    • Si ese conjunto está vacío, no hay forma de convertir una demostración de A en una de B.
  • La interpretación BHK no tiene un operador iff separado, pero sí tiene flechas.
    • Cuando existe una función de A a B y otra de B a A, las dos proposiciones se tratan como equivalentes.
    • Desde la perspectiva de conjuntos, es la situación en la que los conjuntos de demostraciones de ambas proposiciones son isomorfos.
  • La negación no significa simplemente que no haya demostración, sino que debe mostrarse que al asumir que A es verdadera se llega a una contradicción.
    • ⊥ cumple el papel de False o bottom value: una demostración de una fórmula que no tiene demostración.
    • En BHK, ¬A se lee como A → ⊥.
    • En teoría de conjuntos, ⊥ se representa como el conjunto vacío.

Ver la lógica como categoría

  • La interpretación BHK ofrece una perspectiva de alto nivel para interpretar la lógica con teoría de categorías.
  • Algunas categorías pueden verse como sistemas lógicos.
    • Los objetos son proposiciones.
    • Los morfismos son demostraciones.
  • No toda categoría se convierte en sistema lógico; se necesitan condiciones para que haya objetos que correspondan a proposiciones válidas y no los haya para proposiciones no válidas.
  • Las categorías que satisfacen esas condiciones se llaman bicartesian closed category.
  • Como caso simple, primero puede mirarse un orden, donde el sistema lógico y el conjunto de proposiciones atómicas forman una categoría.
    • Si solo hay una forma de ir de A a B, o si se ignoran las diferencias entre formas, se obtiene un preorder.
    • Si se consideran equivalentes las proposiciones que se derivan mutuamente, se obtiene un partial order.
    • A ≤ B significa A → B.
  • En un diagrama de Hasse, si A está debajo de B, entonces se cumple A → B.

Correspondencia orden-teórica de las operaciones lógicas

  • En la interpretación BHK, and y or de la lógica aparecen como product y sum; en teoría del orden corresponden a meet y join.
  • Para que exista un sistema lógico, cualquier par de proposiciones debe poder combinarse con and u or, así que el orden debe tener meet y join para todos sus elementos.
    • A ese tipo de orden se le llama lattice.
  • Una ley importante entre and y or es la distributividad.
    • Si para todo A, B y C se cumple A ∧ (B ∨ C) ≅ (A ∧ B) ∨ (A ∧ C), entonces es un distributive lattice.
  • Para expresar la lógica intuicionista, el lattice también debe tener elementos que correspondan a True y False.
    • False se escribe ⊥ y se relaciona con el principio de explosión, según el cual, si existe una demostración de False, entonces puede demostrarse cualquier proposición.
    • True se escribe ⊤ y se sigue de toda proposición, pero por sí mismo no aporta contenido significativo.
  • En teoría del orden, True y False son respectivamente el greatest object y el least object.
    • En términos de teoría de categorías, corresponden a terminal object e initial object.
    • Un lattice con least y greatest se llama bounded lattice.

Objetos de implicación y objetos exponenciales

  • El lattice que representa un sistema lógico necesita, para cada par A, B, un objeto de implicación que represente la proposición de que A implica B.
  • Este objeto se define mediante la estructura de modus ponens.
    • Debe cumplirse A ∧ (A ⇒ B) → B.
  • Solo esa condición no basta.
    • Otros objetos como A ⇒ B ∧ C o A ⇒ B ∧ C ∧ D también podrían entrar en ese lugar.
    • El verdadero A ⇒ B es el mayor objeto entre los X que satisfacen A ∧ X → B.
  • En teoría del orden, A ⇒ B se llama exponential element o relative pseudo-complement.
    • Es el mayor X que satisface A ∧ X ≤ B.
  • En términos lógicos, el enunciado de implicación A ⇒ B es la proposición X menos específica que satisface A ∧ X → B.
  • En teoría de categorías, se define como exponential object o internal homomorphism object.
    • Debe existir un morfismo A × X → B.
    • Y para cualquier otro objeto candidato con la misma propiedad, debe existir un único morfismo hacia el verdadero objeto exponencial.
  • Esta definición del objeto de implicación encaja con la lógica intuicionista.
    • En lógica clásica, debido a la ley del tercero excluido, A ⇒ B se simplifica a ¬A ∨ B.
  • Igual que meet, join y el objeto de implicación, A ⇒ B queda definido de manera única salvo isomorfismo.

Álgebra de Heyting y bicartesian closed category

  • La lógica intuicionista se compone de True, False, and, or e implies.
  • Si eso se expresa como un orden, se obtiene una álgebra de Heyting.
    • Tiene join y meet.
    • Tiene greatest y least object.
    • Tiene objeto de implicación.
  • Un sistema lógico intuicionista puede verse como una álgebra de Heyting.
    • and y or son meet y join.
    • True y False son greatest y least object.
    • implies es el exponential object.
  • Si la misma definición se adapta a una categoría general, se obtiene una bicartesian closed category.
    • Tiene product y coproduct.
    • Tiene initial y terminal object.
    • Tiene exponential object.
  • Un sistema lógico intuicionista también puede verse como una bicartesian closed category.
    • and y or son product y coproduct.
    • True y False son terminal e initial object.
    • implies es exponential object.
  • Un lattice que siga lógica clásica debe ser, además de bounded y distributive, complemented.
    • Para cada proposición A existe un ¬A único tal que A ∨ ¬A = 1 y A ∧ ¬A = 0.
    • A ese tipo de lattice se le llama Boolean algebra.

Una demostración simple desde la lógica categórica

  • A ∨ ⊤ ≅ ⊤ se sigue directamente de la definición de join.
    • Join es la mínima cota superior que es mayor o igual que ambos objetos.
    • Como no hay ningún objeto mayor o igual que ⊤ salvo ⊤ mismo, el join de cualquier A con ⊤ es ⊤.
    • Lógicamente, es la tautología “cualquier A o True es True”.
  • Si existe A → B, entonces A ∨ B = B.
    • Si uno de los dos objetos está por encima del otro, el join es el objeto superior.
    • Esto puede verse como una generalización de A ∨ ⊤ = ⊤.
    • Porque para todo objeto A, siempre se cumple A → ⊤.
  • La ley de identidad también se demuestra con el objeto de implicación.
    • A ⇒ A es el mayor X que satisface A ∧ X → A.
    • Como esta condición se cumple para todo X, el mayor objeto es ⊤.
    • Por lo tanto, A → A siempre es verdadero.
  • Si A implica semánticamente a B en todos los modelos, es decir, A ⊨ B, entonces A ⇒ B también corresponde a ⊤.
    • Como A mismo ya implica B, se cumple A ∧ X → B para todo X.
    • A esto también se le llama deduction theorem.

Construir lógica con un Free Heyting algebra

  • Para hacer lógica, primero se eligen las proposiciones atómicas que se usarán según el dominio del problema.
  • Si el tipo de lógica elegido es la lógica intuicionista, hay que dibujar en un grafo todas las proposiciones compuestas como A ∧ B y A ∨ B para todo A, B.
  • Como también hay que incluir las composiciones de proposiciones compuestas, la lista completa se vuelve infinita.
  • Para verificar si una proposición implica otra, se sigue el camino de las flechas que salen de la proposición de origen.
  • Hacer lógica consiste en encontrar un camino desde lo que ya se sabe hasta lo que se quiere demostrar, o en construir una demostración manipulando demostraciones ya existentes.
  • En lógica intuicionista, en general es difícil demostrar que un hecho no es alcanzable desde los axiomas, es decir, que no puede demostrarse.

Lecturas relacionadas

1 comentarios

 
GN⁺ 2024-10-27
Comentarios en Hacker News

  • Esta página es realmente excelente, y me la he topado varias veces al estudiar temas relacionados
    Aun así, le doy mi voto a aprender con Milewski. Aprender esto es un recorrido, y el autor de ct-illustrated parece seguir a mitad de ese camino
    Milewski es alguien que ya ha hecho ese recorrido varias veces, así que su libro y su blog son un buen punto de partida
    https://github.com/hmemcpy/milewski-ctfp-pdf Book
    https://bartoszmilewski.com/2014/10/28/category-theory-for-p... Blog

    • Leí como una docena de capítulos del inicio de Milewski, y aunque los primeros capítulos son muy buenos, con el tiempo me irrita cada vez más su estilo de no dar definiciones y notación precisas
      Parece asumir que, si algo se escribe como una prosa ligera e imprecisa, automáticamente es más fácil de entender, pero por eso mismo como referencia casi no sirve
      No es así en absoluto¹
      ¹) https://news.ycombinator.com/item?id=41756286
    • No logro entender qué quiere decir bartoszmilewski, así que ese libro no me sirve de mucho
      Pero en el trabajo uso teoría de categorías en todo mi modelo de dominio

  • Ya se había discutido antes con otra URL
    https://news.ycombinator.com/item?id=28660131 (2 comentarios)
    https://news.ycombinator.com/item?id=28660157 (112 comentarios)

  • En la parte inicial del libro me encontré con esta gran frase al comparar las matemáticas con la ciencia o la ingeniería
    “Por esto, los matemáticos ocupan una posición extraña, incluso podría decirse única, en la que siempre deben defender lo que hacen en términos de su valor para otros campos del saber. Vale la pena enfatizar otra vez que, para cualquier otra disciplina, esto se consideraría absurdo.”
    Es una idea con la que cualquiera que haya estudiado un campo que no lleve directamente a resultados rentables puede identificarse, y da gusto oír que incluso quienes tienen talento para los números también tienen que pelear contra la navaja de Milton Friedman

    • Entonces es una suerte que muchos proyectos de “estudios culturales” en realidad reciban financiamiento directo del Departamento de Defensa y el Departamento de Estado de EE. UU.
      Hoy en día, todo el campo de los estudios “poscoloniales” no es más que el backend del soft power estadounidense, y si hay guerra probablemente también sea el backend del hard power

  • Si los círculos interiores siempre quedan centrados verticalmente, el diagrama de círculos dentro de círculos no escala bien

  • ¿Hay alguna historia de éxito de usar teoría de categorías para resolver de forma útil un problema de CS/SWE que no se hubiera podido resolver sin ella? Mónadas no cuentan, porque uno las terminaría inventando de manera natural si la situación lo exige
    La estudié un año en posgrado, pero al final la dejé

    • No hay ningún problema que no pueda modelarse sin teoría de categorías
      Uno de los teoremas más básicos de la teoría de categorías, el lema de Yoneda, dice directamente que todo problema expresado en el lenguaje de las categorías puede traducirse al lenguaje de conjuntos y funciones. Lo mismo vale para cualquier objeto matemático definido con conjuntos, así que siempre se puede sustituir el nombre por la definición
      Lo que el lenguaje categórico aporta al marco implícito de una teoría no puede ser mayor que la definición de “categoría”, y esa definición es muy pequeña. Es parecido a preguntar por qué usar grupos si “una operación sobre un conjunto con asociatividad, clausura, elemento identidad e inversos” parece más accesible
      El álgebra abstracta se basa en una biblioteca de definiciones que nombran tipos de operaciones sobre conjuntos lo bastante simples como para aparecer con frecuencia. Las herramientas o técnicas no son del tipo de cosa que se encuentra dentro de una definición
      Anillos, espacios vectoriales y módulos suelen aceptarse de inmediato, pero con las categorías la gente se divide entre creyentes y no creyentes. Me intriga por qué pasa eso
    • El caso más cercano que conozco es el trabajo de UMAP
      Cuando entrevisté a Leland McInnes, me explicó en detalle que la teoría de categorías fue clave para conectar varios puntos, aunque no fuera estrictamente necesaria en el código real del resultado final
      Dado el nivel de mejora relativa frente a t-SNE, que era el estado del arte anterior, es el único ejemplo que me ha hecho replantearme mi crítica sobre cómo se habla de teoría de categorías en software
      https://arxiv.org/abs/1802.03426
    • Es parecido a preguntar: “¿Hay historias de éxito de usar un automóvil para llegar a un lugar al que no se podía llegar caminando?”
      La teoría de categorías es un lenguaje y una herramienta, así que todo lo que puedes decir en el lenguaje de la teoría de categorías también puedes decirlo en otro lenguaje
      Como con un automóvil, si aprendes a manejarlo —y la curva de aprendizaje aquí es muy empinada— puedes llegar más rápido. En principio, no es que no puedas llegar caminando sin mencionar explícitamente conceptos de teoría de categorías
    • Si vuelves a formalizar algo que ya entendías dentro de un marco más general, puedes ver mejor lo que realmente significa y separar la esencia de los detalles sucios
      Por lo poco que yo mismo entiendo, una parte importante de la teoría de categorías es caracterizar objetos mediante propiedades universales
      Otra utilidad práctica de la teoría de categorías es que da un lenguaje común para que hablen informáticos, matemáticos y físicos. Si todos llaman al mismo patrón con nombres distintos y definiciones ligeramente incompatibles, colaborar no es fácil
    • En Topos Institute estamos haciendo software nuevo que esperamos resulte mucho más transparente para quienes aún no se han tomado el Kool-Aid de la teoría de categorías
      Por ahora la prealfa es sobre todo para modelado de dinámica de sistemas, pero creemos que para el rango de trabajo al que apuntamos la base categórica es esencial. Me encantaría escuchar ideas de cualquiera
      https://topos.site/blog/2024-10-02-introducing-catcolab/

  • Creo que la teoría de categorías es útil, pero todavía no en computación
    Si no hay una necesidad real, inevitablemente se siente difícil. ¿De verdad hace falta entender bien las propiedades universales, los adjuntos y el lema de Yoneda? Si no hace falta, cuesta mucho aprender qué son
    Curiosamente, la experiencia en programación funcional sí ayuda a entender la teoría de categorías, pero al revés no tanto. Por ejemplo, el polimorfismo paramétrico da intuición sobre las transformaciones naturales, y las transformaciones naturales son clave en todas las aplicaciones de la teoría de categorías
    Las aplicaciones convincentes de la teoría de categorías son muy matemáticas. Se pueden encontrar en topología algebraica, teoría de representaciones, geometría algebraica y lógica no clásica

  • Hay un error
    “El modus ponens es una proposición compuesta por otras dos proposiciones, aquí marcadas como A y B; si la proposición A es verdadera y la proposición A --> B también es verdadera, es decir, si A implica B, entonces B también es verdadera. Por ejemplo, si sabemos ‘Sócrates es humano’ y ‘los humanos mueren’, entonces también sabemos ‘Sócrates muere’.”
    Este ejemplo no es un caso de modus ponens, que es una regla de la lógica proposicional, sino un silogismo categórico que requiere lógica de predicados

  • Aquí dice que “la lógica es la ciencia de lo posible”, pero ¿no debería ser la lógica la ciencia de lo determinable?
    Me parece que el punto central es poder decir de manera concluyente qué es válido y qué no

  • La notación diagramática es interesante
    ¿El autor también presenta reglas de inferencia para transformaciones que preservan la verdad de los diagramas?