Categoria ilustrada: lógica (2021)

 (abuseofnotation.github.io)
2 pontos por GN⁺ 2024-10-27 | 1 comentários | Compartilhar no WhatsApp
  • A lógica parte de proposições atômicas aceitas como verdadeiras e constrói proposições maiores com operadores como and, or e implies, e assim como na teoria das categorias, a composição é central
  • A lógica clássica interpreta proposições como valores Booleanos verdadeiro/falso, e os operadores lógicos como funções booleanas, tratando negação, conjunção, disjunção, implicação e equivalência por meio de tabelas-verdade
  • A interpretação BHK da lógica intuicionista vê proposições como objetos que possuem provas, interpretando A ∧ B como um par de provas e A → B como uma função que transforma uma prova de A em uma prova de B
  • Em algumas categorias, objetos correspondem a proposições e morfismos a provas; em ordens, A ≤ B representa A → B como uma preorder ou partial order
  • A lógica intuicionista corresponde, em termos de teoria da ordem, a uma álgebra de Heyting e, em termos gerais de teoria das categorias, a uma categoria bicartesiana fechada; conjunção, disjunção, verdadeiro, falso e implicação correspondem respectivamente a meet/join, terminal/inicial e objeto exponencial

Lógica começando por proposições

  • A lógica trata de regras formais consistentes consigo mesmas, independentemente da observação, e é um sistema para concluir ou provar que algo é verdadeiro quando se sabe outra coisa
  • Uma teoria matemática pode ser vista como lógica com definições adicionais
    • A teoria dos conjuntos pode ser definida adicionando à lógica padrão o conceito primitivo de relação de pertinência a conjunto
  • Para começar a lógica, é necessário um conjunto inicial de proposições aceitas como verdadeiras ou falsas
    • Isso é chamado de premissas, proposições atômicas ou primary proposition
  • Duas ou mais proposições tornam-se uma única proposição composta por meio de operadores lógicos como and, or e implies/entails
    • ∧ é and
    • ∨ é or
    • → significa follows ou implicação
  • Uma proposição composta também pode, como uma proposição atômica, ser composta novamente com outras proposições

Modus ponens e tautologias

  • Modus ponens é um padrão lógico antigo segundo o qual, se A é verdadeiro e A → B é verdadeiro, então B também é verdadeiro
    • A forma é (A ∧ (A ⇒ B)) → B
    • Pode ser expresso com exemplos como “Sócrates é humano, e se humano então mortal, logo Sócrates é mortal”
  • A lógica não trata apenas de operações isoladas, mas também de combinações e relações entre vários operadores lógicos
    • A relação entre and e implies aparece no modus ponens
    • A lei distributiva entre and e or também é um tema importante
  • Uma tautologia é uma proposição sempre verdadeira, independentemente dos valores de verdade das proposições que a compõem
    • No modus ponens, quer A e B sejam verdadeiros ou falsos, a fórmula inteira é sempre verdadeira
    • Uma proposição sempre falsa é chamada de contradição
    • Colocar not em uma tautologia a transforma em contradição, e colocar not em uma contradição a transforma em tautologia
  • Proposições cujo valor varia entre verdadeiro e falso conforme o caso são chamadas de contingent statement e ficam fora do interesse principal da lógica
  • A tautologia mais simples é a lei da identidade, segundo a qual toda proposição implica a si mesma

Esquemas de axiomas e sistemas lógicos

  • Tautologias formam a base de esquemas de axiomas e regras de inferência
  • Um esquema de axioma é uma fórmula com marcadores de posição, que podem ser substituídos por proposições para gerar proposições concretas
    • Se removermos as cores ou proposições concretas do modus ponens, resta a estrutura geral
    • Inserindo proposições atômicas ou compostas nessa estrutura, é possível construir enunciados específicos de modus ponens
  • Regras de inferência podem ser escritas quase da mesma forma que esquemas de axiomas, e esquemas de axiomas também podem ser aplicados como regras de inferência
  • Toda tautologia pode ser usada como esquema de axioma
  • Um sistema lógico ou sistema formal é uma coleção de esquemas de axiomas e regras de inferência, usada para gerar todas as proposições possíveis
    • Como exemplo, é apresentado um sistema composto por cinco esquemas de axiomas e a regra de inferência do modus ponens
    • O fato de esse sistema lógico ser completo se conecta ao teorema da completude de Gödel

Interpretação por funções de verdade da lógica clássica

  • A lógica clássica baseia-se na dicotomia de que toda proposição é verdadeira ou falsa
  • Na interpretação clássica, proposições e operadores são definidos assim
    • Proposições são coisas que, como valores Booleanos, são verdadeiras ou falsas
    • Operadores lógicos são funções que recebem um ou mais valores Booleanos e retornam um valor Booleano
  • A negação ¬p é uma operação unária que transforma verdadeiro em falso e falso em verdadeiro
    • O mesmo conteúdo pode ser expresso por uma tabela-verdade
    • A eliminação da dupla negação é provada mostrando que aplicar a negação duas vezes retorna ao valor inicial
  • and recebe dois valores Booleanos e retorna verdadeiro apenas quando ambos são verdadeiros
    • p ∧ q → p
    • p ∧ q → q
  • or retorna verdadeiro se pelo menos um dos dois valores Booleanos for verdadeiro
    • p → p ∨ q
    • q → p ∨ q
  • implies, ou condição material, é escrito como p → q e só é falso quando p é verdadeiro e q é falso
    • Na lógica clássica, p → q equivale ao caso em que ¬p ∨ q é verdadeiro
  • if and only if, ou iff, é verdadeiro quando duas proposições têm o mesmo valor
    • P ↔ Q é equivalente a P → Q ∧ Q → P
  • Além de tabelas-verdade, também é possível provar a equivalência entre p → q e ¬p ∨ q com axiomas e regras de inferência
    • Uma prova completa de equivalência requer demonstrações nos dois sentidos

Lógica intuicionista e interpretação BHK

  • A lógica intuicionista vê a prova não como descoberta de uma verdade universal, mas como construção
  • Nessa perspectiva, não se pode usar a dicotomia de que toda proposição é necessariamente verdadeira ou falsa
    • Uma proposição pode não ser demonstrável não por ser falsa, mas por estar fora do escopo do sistema lógico dado
    • A conjectura dos primos gêmeos é frequentemente apresentada como exemplo
  • Na interpretação Brouwer–Heyting–Kolmogorov (BHK), o foco está nas provas, não nas proposições
    • Uma proposição é algo que possui uma prova
    • Operadores lógicos são construções que produzem provas a partir de outras provas
  • Uma prova de A ∧ B é um par composto por uma prova de A e uma prova de B, ou seja, um product
  • A → B significa que existe uma função que transforma uma prova de A em uma prova de B
    • O conjunto de provas de A → B pode ser representado como o conjunto de funções de A para B, isto é, um hom-set
    • Se esse conjunto estiver vazio, não há como transformar uma prova de A em uma prova de B
  • A interpretação BHK não tem um operador iff separado, mas tem setas
    • Quando há funções de A para B e de B para A, as duas proposições são tratadas como equivalentes
    • Do ponto de vista de conjuntos, isso é uma situação em que os conjuntos de provas das duas proposições são isomorfos
  • Negação não significa apenas ausência de prova; é preciso mostrar que, assumindo A como verdadeiro, chega-se a uma contradição
    • ⊥ desempenha o papel de False ou bottom value, isto é, a prova de uma fórmula sem prova
    • Em BHK, ¬A é lido como A → ⊥
    • Na teoria dos conjuntos, ⊥ é representado pelo conjunto vazio

Ver a lógica como categoria

  • A interpretação BHK oferece uma perspectiva de alto nível para interpretar a lógica por teoria das categorias
  • Algumas categorias podem ser vistas como sistemas lógicos
    • Objetos são proposições
    • Morfismos são provas
  • Nem toda categoria se torna um sistema lógico; são necessárias condições para que existam objetos correspondentes a proposições lógicas válidas e não existam objetos correspondentes a proposições inválidas
  • Categorias que satisfazem essas condições são chamadas de categorias bicartesianas fechadas
  • Como caso simples, podemos olhar primeiro para uma ordem; um sistema lógico e um conjunto de proposições atômicas formam uma categoria
    • Se há apenas uma forma de ir de A para B, ou se a diferença é ignorada, isso se torna uma preorder
    • Se proposições que se implicam mutuamente forem tratadas como equivalentes, obtém-se uma partial order
    • A ≤ B significa A → B
  • Em um diagrama de Hasse, quando A está abaixo de B, vale A → B

Correspondência ordenada das operações lógicas

  • and e or da lógica aparecem como product e sum na interpretação BHK e correspondem a meet e join na teoria da ordem
  • Para que seja um sistema lógico, uma ordem deve permitir combinar quaisquer duas proposições com and ou or, então precisa ter meet e join para todos os elementos
    • Uma ordem assim é chamada de lattice
  • Uma lei importante entre and e or é a distributividade
    • Se para todos A, B, C vale A ∧ (B ∨ C) ≅ (A ∧ B) ∨ (A ∧ C), então temos um distributive lattice
  • Para expressar lógica intuicionista, o lattice também precisa ter elementos correspondentes a True e False
    • False é escrito como ⊥ e se conecta ao princípio da explosão, segundo o qual, se há uma prova de False, qualquer proposição pode ser provada
    • True é escrito como ⊤ e decorre de toda proposição, mas não produz conteúdo significativo por si só
  • Em ordens, True e False são respectivamente o greatest object e o least object
    • Em termos da teoria das categorias, correspondem a objeto terminal e objeto inicial
    • Um lattice com least e greatest é um bounded lattice

Objeto de implicação e objeto exponencial

  • Um lattice que representa um sistema lógico precisa, para cada par A, B, de um objeto de implicação que represente a proposição de que A implica B
  • Esse objeto é definido pela estrutura do modus ponens
    • Deve valer A ∧ (A ⇒ B) → B
  • Só essa condição não basta
    • Outros objetos como A ⇒ B ∧ C ou A ⇒ B ∧ C ∧ D também poderiam ocupar o mesmo lugar
    • O verdadeiro A ⇒ B é o maior objeto entre os X que satisfazem A ∧ X → B
  • Na teoria da ordem, A ⇒ B é chamado de elemento exponencial ou pseudo-complemento relativo
    • É o maior X que satisfaz A ∧ X ≤ B
  • Em termos lógicos, a proposição mais trivial X que satisfaz A ∧ X → B é a proposição de implicação A ⇒ B
  • Em teoria das categorias, isso é definido como objeto exponencial ou objeto de homomorfismo interno
    • Deve existir um morfismo A × X → B
    • E, para qualquer outro objeto candidato com a mesma propriedade, deve existir um único morfismo dele para o verdadeiro objeto exponencial
  • Essa definição de objeto de implicação corresponde à lógica intuicionista
    • Na lógica clássica, devido ao terceiro excluído, A ⇒ B se simplifica para ¬A ∨ B
  • Assim como meet, join e o objeto de implicação, A ⇒ B também é definido de maneira única a menos de isomorfismo

Álgebra de Heyting e categoria bicartesiana fechada

  • A lógica intuicionista é composta por True, False, and, or e implies
  • Quando isso é expresso como uma ordem, obtém-se uma álgebra de Heyting
    • Possui join e meet
    • Possui greatest e least object
    • Possui objeto de implicação
  • Um sistema de lógica intuicionista pode ser visto como uma álgebra de Heyting
    • and e or são meet e join
    • True e False são greatest e least object
    • implies é o objeto exponencial
  • Adaptando a mesma definição para categorias gerais, obtém-se uma categoria bicartesiana fechada
    • Possui product e coproduct
    • Possui objeto inicial e objeto terminal
    • Possui objeto exponencial
  • Um sistema de lógica intuicionista também pode ser visto como uma categoria bicartesiana fechada
    • and e or são product e coproduct
    • True e False são objeto terminal e objeto inicial
    • implies é o objeto exponencial
  • Um lattice que segue a lógica clássica deve, além de bounded e distributive, ser complemented
    • Para cada proposição A, existe uma ¬A única tal que A ∨ ¬A = 1 e A ∧ ¬A = 0
    • Um lattice assim é chamado de álgebra Booleana

Uma prova simples vista pela lógica categórica

  • A ∨ ⊤ ≅ ⊤ segue diretamente da definição de join
    • Join é o menor majorante que é maior ou igual aos dois objetos
    • Como não existe objeto maior ou igual a ⊤ além do próprio ⊤, o join de qualquer A com ⊤ é ⊤
    • Em termos lógicos, isso é a tautologia “qualquer A ou True é True”
  • Se existe A → B, então A ∨ B = B
    • Quando um dos dois objetos está acima do outro, o join é o objeto mais alto
    • Isso pode ser visto como uma generalização de A ∨ ⊤ = ⊤
    • Porque para todo objeto A, sempre vale A → ⊤
  • A lei da identidade também é provada com o objeto de implicação
    • A ⇒ A é o maior X que satisfaz A ∧ X → A
    • Como essa condição vale para todo X, ele se torna o maior objeto ⊤
    • Portanto, A → A é sempre verdadeiro
  • Se A é consequência semântica de B em todos os modelos, A ⊨ B, então A ⇒ B também corresponde a ⊤
    • Como o próprio A já implica B, A ∧ X → B vale para todo X
    • Isso também é chamado de teorema da dedução

Construindo lógica com a free Heyting algebra

  • Para fazer lógica, primeiro escolhe-se quais proposições atômicas serão usadas de acordo com o domínio do problema
  • Se o tipo de lógica escolhido for a lógica intuicionista, é preciso desenhar no grafo proposições compostas como A ∧ B e A ∨ B para todos A, B
  • Como as composições de proposições compostas também precisam ser incluídas novamente, a lista inteira torna-se infinita
  • Se uma proposição implica outra pode ser verificado seguindo os caminhos das setas que saem da proposição de partida
  • Fazer lógica é o processo de encontrar um caminho do que já se sabe até o que se quer provar, ou de manipular provas já existentes para construir uma nova prova
  • Na lógica intuicionista, em geral é difícil provar que um fato é inalcançável a partir dos axiomas, isto é, que não pode ser demonstrado

Leituras relacionadas

1 comentários

 
GN⁺ 2024-10-27
Comentários no Hacker News

  • Esta página é realmente excelente, e já esbarrei nela várias vezes ao estudar assuntos relacionados.
    Ainda assim, eu votaria por aprender com Milewski. Aprender isso é uma jornada, e o autor de ct-illustrated parece ainda estar no meio dela.
    Milewski já percorreu esse caminho várias vezes, então o livro e o blog são bons pontos de partida.
    https://github.com/hmemcpy/milewski-ctfp-pdf Livro
    https://bartoszmilewski.com/2014/10/28/category-theory-for-p... Blog

    • Li as primeiras dezenas de capítulos de Milewski; os primeiros capítulos foram muito bons, mas o estilo de não dar definições e notações precisas fica cada vez mais irritante.
      Ele parece achar que tudo fica mais fácil de entender quando escrito em prosa leve e imprecisa, mas isso torna o material quase inútil como referência.
      Não é nada disso¹
      ¹) https://news.ycombinator.com/item?id=41756286
    • Como não entendo o que bartoszmilewski está dizendo, esse livro parece inútil para mim.
      Mas no trabalho usamos teoria das categorias em todo o meu modelo de domínio.

  • Isso já foi discutido antes em outra URL.
    https://news.ycombinator.com/item?id=28660131 (2 comentários)
    https://news.ycombinator.com/item?id=28660157 (112 comentários)

  • No começo do livro encontrei esta ótima frase, comparando matemática com ciência ou engenharia:
    “Por causa disso, os matemáticos se veem numa posição estranha, talvez até única, de ter que defender constantemente o que fazem em termos de seu valor para outras áreas do conhecimento. Reforçando: em qualquer outra área do conhecimento, isso seria considerado absurdo.”
    É uma ideia com que qualquer pessoa que tenha estudado uma área que não leve diretamente a resultados monetizáveis pode se identificar, e é bom ouvir que até pessoas com talento para números precisam lutar contra a navalha de Milton Friedman.

    • Então é uma sorte que muitos projetos de “estudos culturais” sejam, na prática, financiados diretamente pelo Departamento de Defesa e pelo Departamento de Estado dos EUA.
      Hoje, todo o campo de estudos de “pós-colonialismo” não passa do backend do soft power americano e, se houver guerra, provavelmente também será o backend do hard power.

  • Se os círculos internos estiverem sempre centralizados verticalmente, o diagrama de círculos dentro de círculos não escala muito bem.

  • Há alguma história de sucesso em que se tenha usado teoria das categorias para resolver de forma útil um problema de CS/SWE que não poderia ter sido resolvido sem teoria das categorias? Mônadas não contam, porque são algo que você acaba inventando naturalmente se a situação exigir.
    Estudei isso por um ano na pós-graduação, mas acabei desistindo.

    • Não há problema que não possa ser modelado sem teoria das categorias.
      Um dos teoremas mais básicos da teoria das categorias, o lema de Yoneda, diz diretamente que qualquer problema expresso na linguagem das categorias pode ser traduzido para a linguagem de conjuntos e funções. O mesmo vale para qualquer objeto matemático definido em termos de conjuntos, de modo que sempre se pode substituir o nome pela definição.
      A contribuição da linguagem categórica para o arcabouço implícito de uma teoria não pode ser maior que a definição de “categoria”, e essa definição é muito pequena. É parecido com perguntar por que usar grupos quando “uma operação sobre um conjunto com associatividade, fechamento, identidade e inversos” parece mais acessível.
      A álgebra abstrata se baseia em uma biblioteca de definições que apontam para tipos de operações sobre conjuntos simples o bastante para serem comuns. Ferramentas ou técnicas não são o tipo de coisa que se encontra dentro de uma definição.
      Anéis, espaços vetoriais e módulos costumam ser aceitos de imediato por si só, mas categorias dividem crentes e descrentes. Fico curioso por que isso acontece.
    • O exemplo mais próximo que conheço é o trabalho do UMAP.
      Quando entrevistei Leland McInnes, ele explicou em detalhes que, mesmo que a teoria das categorias não fosse estritamente necessária no código real do resultado final, ela teve um papel importante em conectar vários pontos.
      Considerando a melhoria relativa em relação ao t-SNE, que era o estado da arte anterior, esse é o único exemplo que me fez repensar minhas críticas à forma como se fala de teoria das categorias em software.
      https://arxiv.org/abs/1802.03426
    • É parecido com perguntar: “há alguma história de sucesso de usar um carro para ir a algum lugar aonde não se podia chegar a pé?”
      Teoria das categorias é uma linguagem e uma ferramenta, então o que pode ser dito na linguagem da teoria das categorias também pode ser dito em outras linguagens.
      Como com um carro, quando você aprende a dirigir — e aqui a curva de aprendizado é bem íngreme —, consegue chegar mais rápido. Em princípio, não há nada a que você não possa chegar a pé sem mencionar explicitamente conceitos de teoria das categorias.
    • Quando você reformula algo que já entende em um arcabouço mais geral, enxerga melhor o que aquilo realmente significa e consegue separar a essência dos detalhes bagunçados.
      Pelo meu entendimento bastante limitado, caracterizar objetos por propriedades universais é uma parte importante da teoria das categorias.
      Outra utilidade prática da teoria das categorias é fornecer uma linguagem comum para cientistas da computação, matemáticos e físicos conversarem. Quando todos chamam o mesmo padrão por nomes diferentes e usam definições ligeiramente incompatíveis, a colaboração não fica fácil.
    • O Topos Institute está criando um novo software que esperamos que pareça muito mais transparente para pessoas que ainda não beberam o Kool-Aid da teoria das categorias.
      A pré-alfa atual é voltada principalmente para modelagem de dinâmica de sistemas, mas acho que uma base categórica é essencial para o escopo de trabalho que temos como objetivo. Ficaria feliz em ouvir a opinião de qualquer pessoa.
      https://topos.site/blog/2024-10-02-introducing-catcolab/

  • Acho que teoria das categorias é útil, mas ainda não em computação.
    Se você não tiver uma necessidade real dela, é inevitável que pareça difícil. Será que você realmente precisa entender propriedades universais, funtores adjuntos e o lema de Yoneda? Se não precisa, vai sofrer para aprender o que eles são.
    Curiosamente, experiência com programação funcional ajuda a entender teoria das categorias, mas o contrário não ajuda tanto. Por exemplo, polimorfismo paramétrico dá uma intuição para transformações naturais, e transformações naturais são centrais em todas as aplicações da teoria das categorias.
    As aplicações convincentes da teoria das categorias são muito matemáticas. Dá para encontrá-las em topologia algébrica, teoria de representações, geometria algébrica e lógicas não clássicas.

  • Há um erro.
    “O modus ponens é uma proposição composta por duas outras proposições, aqui indicadas por A e B, e diz que, se a proposição A é verdadeira e A --> B também é verdadeira, isto é, se A implica B, então B também é verdadeira. Por exemplo, se sabemos que ‘Sócrates é humano’ e que ‘humanos morrem’, então também sabemos que ‘Sócrates morre’.”
    Esse exemplo não é um caso de modus ponens, que é uma regra da lógica proposicional, mas sim um silogismo categórico, que exige lógica de predicados.

  • Aqui se diz que “a lógica é a ciência do possível”, mas a lógica não deveria ser a ciência do determinado?
    Acho que o ponto central é permitir dizer de forma definitiva o que é válido ou não.

  • A notação diagramática é interessante.
    O autor também apresenta regras de inferência para transformações preservadoras de verdade dos diagramas?