Oi, Walter Sou novo aqui no grupo. Espero estar usando os comandos certos para responder para o grupo todo. Há muitos anos não participo de grupo algum na internet.
De imediato não temos como responder à sua questão, pelo menos por enquanto. O fato é que Flow é uma teoria de primeira ordem. E todas as funções são termos. Se é possível ou não imitar de alguma forma aquilo que lambda faz (pelo menos no untyped lambda calculus) para criar funções, não sabemos (por enquanto). Nosso foco inicial é algo um tanto diferente. A principal motivação para este trabalho reside no fato de que formulações conjuntistas usuais para teorias matemáticas e físicas contam com uma carga excessiva de conceitos primitivos dispensáveis. Para confirmar isso, dar uma olhada nas referências do artigo (especialmente trabalhos que fiz com Newton da Costa sobre eliminabilidade de espaço, tempo e espaço-tempo em teorias físicas). Um bom resumo dessas ideias se encontra em artigo que fiz com Otávio Bueno e que foi publicado cinco anos atrás em Erkenntnis. Em função disso, a motivação para Flow consiste em uma proposta que estenda as concepções de Suppes para axiomatização de teorias (no lugar de predicados conjuntistas, propomos predicados numa linguagem como a de Flow) e que permita redefinir teorias usuais da matemática e da física de forma mais enxuta. Provar que categorias está imersa em Flow foi apenas um bônus. Mas foi um bônus muito bem-vindo, claro. É claro que existe uma relação entre categorias e teoria de tipos. Ou seja, sua pergunta motiva algo importante a ser respondido. Mas temos um problema logístico aqui. Por um lado, o atual texto divulgado por aqui já está bastante extenso (com mais de 40 páginas). E estamos longe ainda de concluirmos aquilo que nos propomos a fazer. Isso significa que se formos tratar de relações entre Flow e teoria de tipos, duvido que tentemos isso já no primeiro artigo sobre o tema. Mas é aquela coisa. Se quiser colaborar neste projeto, sinta-se muitíssimo bem-vindo. Abbracci Adonai Em quarta-feira, 6 de novembro de 2019 09:28:39 UTC-3, Walter Carnielli escreveu: > > > > Oi Márcio, > > Não vi ainda mas parece interessante. > > Você poderia comentar um pouco sobre as relações entre Flow Theor > <http://groups.google.com/a/dimap.ufrn.br/group/logica-l/t/fed74aa17f31ddda?utm_source=digest&utm_medium=email>y > > e teoria de tipos ,em particular sobre o abstrator lambda que forma > funções? > > W. > > Em qua, 6 de nov de 2019 08:10, <[email protected] <javascript:>> > escreveu: > >> [email protected] >> <https://groups.google.com/a/dimap.ufrn.br/forum/?utm_source=digest&utm_medium=email#!forum/logica-l/topics> >> Grupos >> do Google >> <https://groups.google.com/a/dimap.ufrn.br/forum/?utm_source=digest&utm_medium=email/#!overview> >> >> <https://groups.google.com/a/dimap.ufrn.br/forum/?utm_source=digest&utm_medium=email/#!overview> >> >> Resumo por e-mail dos temas >> Ver todos os temas >> <https://groups.google.com/a/dimap.ufrn.br/forum/?utm_source=digest&utm_medium=email#!forum/logica-l/topics> >> >> >> - INSCRIÇÕES ATÉ 12/11/2019: Prof >> >> <#CA+ob58OVxeJAtMR8NjxYNQMse2HHhhUDmCLUaVG9FVy7dqB2QQ@mail.gmail.com_m_2500684615994902327_group_thread_0> >> >> > > >> - Flow Theory: conjuntos, relações e categorias como casos >> particulares do conceito de função >> >> <http://groups.google.com/a/dimap.ufrn.br/group/logica-l/t/fed74aa17f31ddda?utm_source=digest&utm_medium=email> >> >> >> >> "Márcio Palmares" <[email protected] <javascript:>>: Nov 05 10:29AM >> -0200 >> >> Olá, pessoal! >> >> Compartilho a seguir o link para o preprint de um artigo que será em breve >> publicado (assim esperamos): >> >> http://philsci-archive.pitt.edu/16610/ >> >> Trata-se de uma teoria de primeira ordem com igualdade e uma única letra >> funcional, cuja interpretação pretendida é o conceito intuitivo de função, >> mais precisamente a ideia de "valoração", "calcular em", ou "avaliação" >> (evaluation): f_1^2(x, y) = x(y). >> >> O propósito dessa teoria é modificar a máxima "todas as coisas são >> conjuntos", ou "tudo é conjunto", substituindo-a por "todas as coisas são >> funções" ou "tudo é função". >> >> Não é um programa novo, apesar de os resultados que apresentamos no >> preprint, sim, são novos. Entre eles, destacamos: >> >> 1) O paradoxo de Russell é evitado de forma muito simples, sem necessidade >> de algo similar ao Esquema de Separação; >> >> 2) A definição usual de igualdade de funções é um teorema em Flow, que >> decorre de um axioma de extensionalidade associado a "propriedades >> universais" de duas funções especiais; >> >> 3) Par ordenado é teorema; >> >> 4) Potência é teorema; >> >> 5) Não há redução do conceito de avaliação ao de composição, como em >> categorias, tais ideias permanecem distintas, o que nos permite observar >> fenômenos que não aparecem quando usamos apenas "lentes categoriais". >> >> Como é bem sabido, von Newmman introduziu em seu famoso artigo de 1925 uma >> proposta de fundamentação para a matemática inteiramente assentada na >> ideia >> de função, isto é, em que os conjuntos são definidos por meio de funções >> e, >> portanto, figuram numa posição subordinada. >> >> Por outro lado, é também evidente que a teoria de categorias concede >> grande >> centralidade à ideia de função (generalizada no conceito de morfismo), >> subordinando os conjuntos ao papel de meros objetos que, a rigor, são >> dispensáveis: podem ser substituídos por morfismos-identidade >> ("object-free >> definition"). Note-se, a propósito, a antevisão de von Neumman, que >> apresentou sua proposta vinte anos antes do artigo "A general theory of >> natural equivalences" de Eilenberg e Mac Lane. (Não estamos sugerindo >> correlação direta entre tais trabalhos ou entre as duas visões sobre >> matemática que eles representam, apenas tentando enfatizar o papel >> preponderante que funções podem adquirir frente aos conjuntos.) >> >> O trabalho que agora submetemos à critica é um desenvolvimeto de pesquisas >> realizadas há vários anos pelo Prof. Adonai Sant'anna, em parceria com o >> Prof. Otávio Bueno e com o Prof. Newton da Costa, sobre a possibilidade de >> eliminar o máximo número de conceitos primitivos "dispensáveis" >> (definíveis >> por meio de outros) na axiomatização de teorias físicas e também de >> teorias >> matemáticas usuais, como a teoria de conjuntos. >> >> A primeira formulação das ideias que deram origem à Teoria Flow apareceu >> num artigo do Prof. Adonai e do Prof. Otávio Bueno publicado em 2014, >> intitulado "Sets and functions in theoretical physics". Neste trabalho, >> entretanto, a então "Teoria N" mantinha-se ainda muito próxima da ideia >> original de von Neumman e não se fazia uso sistemático de métodos >> categoriais (busca pelos fenômenos de dualidade, adjunção, propriedades >> universais, etc.) para a obtenção de linhas de investigação ou resultados >> novos. Por isso, duas funções especiais, constantes introduzidas por von >> Neumman para fazer o papel análogo ao daquilo que hoje chamamos de >> "classificador de subobjetos" de Set, isto é, ligadas ao conceito de >> função >> característica, permaneciam sem significado na Teoria N, a despeito do >> fato >> de que o próprio artigo já sugerisse a possibilidade de investigar com >> mais >> profundidade o possível significado dessas funções. >> >> Na formulação atual, tais constantes, representadas com 0 e 1, são agora >> funções muito especiais, que possuem "propriedades universais", de certo >> modo "duais" (a notação já sugeria, desde a Teoria N, embora não >> intencionalmente, a dualidade objeto terminal vs. inicial). >> >> Por estar assentada no conceito de avaliação (evaluation) e não no >> conceito >> de composição, como a teoria de categorias, Flow é simultaneamente >> distinta >> da teoria de categorias e parece conter a teoria de categorias, na medida >> em que esta pode ser vista como a descrição de um subuniverso de Flow, em >> que por razões práticas pode ser útil introduzir a ideia de composição >> restrita, domínio e codomínio, etc. (Em Flow, todas as funções são >> "componíveis", não há necessidade, em princípio, dos conceitos de domínio >> e >> codomínio, mas eles podem ser facilmente introduzidos.) >> >> O nome Flow Theory é uma alusão à filosofia de Heráclito, que compreende a >> realidade como um processo de transformação permanente, um fluxo de >> transformações e mudanças. Tal escolha está, portanto, em oposição à >> "filosofia" implícita na ideia de conjuntos abstratos, onde os entes do >> universo matemático são coisas estáticas, com elementos igualmente >> estáticos, que se relacionam com os conjuntos por meio da rígida relação >> de >> pertinência. Em Flow, os entes do universo são funções, processos de >> transformação. As transformações atuam umas sobre as outras produzindo >> novas transformações. Aqui há um notável paralelo, obtido de forma não >> intencional, com a fundamentação filosófica da Topos Theory, em que toda >> ideia de "constância" é vista como um caso limite de processos de variação >> (William Lawvere). De modo análogo, em Flow, conjuntos são funções muito >> especiais, funções que chamamos de "estáticas" (às vezes de "mortas"). >> >> A versão apresentada nesse preprint é uma versão simplificada de Flow, em >> que forçamos a "extensionalidade fraca" de Flow a se comportar como a >> extensionalidade conjuntista: duas funções com o mesmo "comportamento" são >> iguais nessa versão simplificada. Essa escolha tem o propósito de >> facilitar >> a demonstração de que os axiomas de ZFC, quando traduzidos em Flow, são >> teoremas. Na versão não simplificada de Flow, contudo, pode não ser tão >> fácil obter tal demonstração: duas funções com o mesmo comportamento não >> são necessariamente iguais, seriam apenas "equivalentes". Ainda não >> descobrimos, nessa versão não simplificada, leis de cancelamento (como >> monomorfismo e epimorfismo) ou "separadores" (como o objeto terminal em >> Set) que nos permitam separar morfismos, obter a igualdade de funções: >> elas >> continuam sendo seres com individualidade, porém não totalmente >> distinguíveis (até o momento). Acreditamos que Flow possa desempenhar, no >> futuro, papel relevante na formulação de problemas sobre >> "indistinguibilidade" que ocorrem em mecânica quântica. >> >> Um minicurso sobre a Teoria Flow será apresentado em um workshop sobre >> mecânica quântica que ocorrerá em Florianópolis em dezembro. Até lá, >> pretendemos ainda preencher as lacunas do preprint e coletar críticas, >> sugestões e correções. Como a proposta é bastante ousada, pode ser que >> estejamos completamente equivocados! :-) >> >> Por outro lado, a versão que está agora no papel é resultado de seis meses >> de trabalho diário. Nesse percurso, nos deparamos diversas vezes com >> pequenas inconsistências. Ficaremos imensamente agradecidos se os colegas >> interessados puderem analisá-lo com seus alertas de inconsistência >> ligados! >> >> Ainda há muita coisa interessante para ser analisada e certamente diversos >> fatos, teoremas, que não estamos enxergando. Uma das nossas dificuldades >> no >> momento é que o único categorista da nossa equipe é amador (eu), o que tem >> atrasado um pouco a obtenção de resultados que parecem estar diante do >> nosso nariz, mas que não conseguimos formular satisfatoriamente. Temos a >> esperança, contudo, de que categoristas profissionais se interessem pelo >> trabalho e queiram contribuir com o desenvolvimento dessa teoria. >> >> A propósito, os diagraminhas que representam as funções finitas pequenas >> de >> Flow são grafos reflexivos, o que sugere um problema de imersão (fora da >> teoria, é claro) de Flow na categoria dos grafos reflexivos ou um problema >> de imersão de Flow, vista como categoria (monoide sob a composição), na >> categoria dos endomorfismos de conjuntos... Isso tudo está em aberto. >> Outro >> fato curioso é que uma das funções mais importantes de Flow, a função >> sucessor, tem um comportamento "algébrico" muito similar ao de um >> funtor-hom, e parece nos dar de fato uma interpretação "quase-funtorial" >> de >> um subuniverso de Flow em conjuntos (chamamos de "quase-funtorial" porque >> o >> sucessor de uma composição não é igual à composição de sucessores, ela >> contém a composição, mas apenas em casos particulares é igual). >> >> Bom, era isso. Esperamos que os colegas se interessem e que possam >> analisar >> o material (e que não descubramos nenhum erro muito grave, hahaha...) >> >> Abraços! >> >> M. >> Voltar ao início >> <#CA+ob58OVxeJAtMR8NjxYNQMse2HHhhUDmCLUaVG9FVy7dqB2QQ@mail.gmail.com_m_2500684615994902327_digest_top> >> >> Você recebeu esse resumo porque está inscrito para receber atualizações >> deste grupo. Você pode alterar suas configurações na página de >> associação do grupo >> <https://groups.google.com/a/dimap.ufrn.br/forum/?utm_source=digest&utm_medium=email#!forum/logica-l/join> >> . >> Para cancelar sua inscrição neste grupo e deixar de receber e-mails do >> mesmo, envie um e-mail para [email protected] <javascript:>. >> > -- Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos Grupos do Google. Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para [email protected]. Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/6f6d8217-7640-417a-b6fb-cdb6a64ad4e7%40dimap.ufrn.br.
