oi Marcio, sim, que o lambda-calculus sem tipos precisa de ser modelado em categorias (pra nao ter problemas parecidos com os do paradoxo de Russell) 'e bem conhecido. o paper mais famoso do John Reynolds e' Polymorphism is not set-theoretic - HAL-Inri <https://hal.inria.fr/inria-00076261/document>e a resposta do Andy Pitts 'e: Polymorphism is set theoretic, constructively <https://link.springer.com/content/pdf/10.1007%2F3-540-18508-9_18.pdf> e sim 'e otimo ilustrar outros possiveis usos pro framework. mas esse uso eu nao acho muito convincente nao, pois a gente sabe modelar o lambda-calculus com ou sem tipos. a minha impressao sobre foundational frameworks 'e que eles todos funcionam -mais ou menos- igualmente. umas coisas sao melhores em um, outras em outro, mas no final da' tudo mais ou menos no mesmo na media. abs Valeria
On Fri, Oct 9, 2020 at 4:59 PM Márcio Palmares <[email protected]> wrote: > No livro "Introduction to higher order categorical logic", Lambek e P.J. > Scott dizem o seguinte: > > "An obvious question to ask about the untyped λ-calculus, as originally > defined or as extended by us, is what its models, that is, Curry algebras > or C-monoids, look like. In particular, are there any models other than the > trivial one with only one element? This is the old question: can one > consistently posit a universe of functions which apply to all functions, > including themselves as arguments?" [pp. 118-119] > > O livro é de 1986, mas teve reimpressão em 1994... > > Em um artigo, creio que de 1982, "What is a model of the lambda calculus", > Albert R. Meyer, por sua vez, escrevia: > > > "Applying a function to itself violates the rules of ordinary set theory > which forbid a function from being in its own domain. The violation can > quickly lead to contradiction. For example, let P be the "paradoxical" > functional such that P(f) is zero if f(f) is not the integer zero, and P(f) > is the integer one otherwise. So by definition P(f) != f(f) for all f; > substituting P for f immediately yields the > contradiction P(P) != P(P)." > > Em publicações mais recentes sobre modelos para o cálculo lambda, > encontramos sempre a mesma objeção a um possível universo de funções > auto-aplicáveis, como se obter um tal sistema não fosse possível. > > Bem, a menos que tenhamos feito tudo errado (não creio que seja o caso, > haha), encontramos um tal sistema. > > Aqui entra uma possível interessante conexão com a teoria de categorias > (entre outras). > > Sabe-se que Dana Scott construiu um modelo para o "untyped lambda > calculus" usando a ideia de um "objeto reflexivo" U em uma categoria > cartesianamente fechada (detalhes em > https://ncatlab.org/nlab/show/lambda-calculus). > > Esse modelo de Dana Scott, de algum modo, é similar à visão intuitiva que > temos do universo primitivo U (não é um termo da teoria) onde "estariam" > todos os termos da teoria Flow... > > Então, um problema interessante é o seguinte: será que alguma porção do > universo de Flow pode ser modelada usando essa ideia de Dana Scott? Se sim, > por uma espécie de transitividade, saberíamos qual é a porção do universo > de Flow que corresponde a um modelo para o cálculo lambda. > > [Não pretendo tirar o foco da discussão sobre o Princípio da Partição, > estou apenas ilustrando possíveis "usos" para o framework.] :-) > > []'s > > M. > > > > Em sexta-feira, 9 de outubro de 2020, Valeria de Paiva < > [email protected]> escreveu: > >> muito obrigada pela resposta direta Samuel! >> valeu! >> Valeria >> >> On Fri, Oct 9, 2020 at 4:04 PM Samuel Gomes da Silva <[email protected]> >> wrote: >> >>> Olá Valeria, >>> >>> Eu confesso que a minha desconfiança no quanto a PP ser equivalente a AC >>> ou não, que eu realmente achava que poderia ser, >>> era mais pelo tempo que o problema ficou aberto. >>> >>> Recentemente, quando Malliaris e Shelah provaram que p = t, eu também >>> estava no grupo dos 99 por cento dos teoristas de conjuntos >>> que pensavam que a solução do problema não seria essa, e sim p < t >>> consistente. >>> >>> Então a gente cria expectativas quando um problema de muito tempo fica >>> aberto, no meu caso não era muito mais do que >>> isso o "chute" de que PP poderia ser equivalente a AC. >>> >>> Quanto a grandes cardinais: ora, categoristas mais ou menos pressupõem >>> que existam grandes cardinais, não é ? É com grandes >>> cardinais que normalmente se justificam a existência (no sentido de se >>> imaginar modelos conjuntistas) de conglomerados e outros que tais. >>> >>> Por exemplo, eu estava lendo recentemente alguma reportagem na qual se >>> dizia que Grothendieck não tinha absolutamente >>> nenhuma preocupação quanto ao fato de que a existência de Universos de >>> Grothendieck era equivalente à existência de >>> cardinais fortemente inacessíveis. Para ele, aquilo seria apenas um meio >>> para se chegar em algo. >>> >>> Se existe a intenção de que a teoria Flow se meta em Categorias, >>> inacessíveis são até bem vindos, acho. >>> >>> Atés >>> >>> []s Samuel >>> >>> ------------------------------ >>> *De: *"Valeria de Paiva" <[email protected]> >>> *Para: *"samuel" <[email protected]> >>> *Cc: *"LOGICA-L" <[email protected]>, "marciopalmares" < >>> [email protected]>, "Adonai S. Sant'Anna" < >>> [email protected]> >>> *Enviadas: *Sexta-feira, 9 de outubro de 2020 18:54:13 >>> *Assunto: *Re: [Logica-l] Re: Teoria Flow: o princípio da partição não >>> implica o axioma de escolha >>> >>> Sim, Samuel! >>> e' por isso que eu perguntei, ne? >>> >>> vc tb publicou ha' algum tempo atras (2017) com o Andreas e o Hugo >>> >>> https://www.researchgate.net/publication/319331534_Categorial_forms_of_the_Axiom_of_Choice >>> e a continuacao (que eu ainda nao li). >>> >>> por isso minha pergunta inicial: >>> o que nos levava a pensar que PP e AC seriam equivalentes? >>> nao eram as formas categoricas do AC, me parece. >>> >>> uma segunda pergunta, mais geral e', por que introduzir mais um >>> "foundational framework"-- >>> se nao for pra resolver o problema de PP equivalente ou nao a AC? ('e >>> muito lindo mesmo, se resolver esse problema, tb acho!) >>> >>> mas a terceira pergunta 'e se isso nao 'e "caro" demais: Flow insiste >>> que tenhamos a "existence of strongly inaccessible cardinals". >>> vale o preco? na verdade eu nao sei os "precos" em teoria de conjuntos, >>> nao sei o que 'e caro ou o que e' barato. >>> mas eu acho que 'essa a discussao q o Adonai, o Marcio e o Renato >>> estavam querendo suscitar, nao e'? >>> >>> abracos conjuntistas (mas ignorantes) a todxs! >>> Valeria >>> >>> >>> On Fri, Oct 9, 2020 at 3:25 PM samuel <[email protected]> wrote: >>> >>>> ... Bom, só pra dar um pitaco de Princípio da Partição em categorias, >>>> recentemente eu publiquei este paper aqui, relacionando tanto o Axioma da >>>> Escolha quanto o Princípio da Partição com as categorias Dialecticas da >>>> Valeria. >>>> >>>> >>>> https://academic.oup.com/jigpal/advance-article-abstract/doi/10.1093/jigpal/jzaa023/5875437?redirectedFrom=fulltext >>>> >>>> Atés >>>> >>>> []s Samuel >>>> >>>> >>>> Em sexta-feira, 9 de outubro de 2020 às 18:19:17 UTC-4, samuel escreveu: >>>> >>>>> ... Foi pelo blog do Karagila que há alguns anos atrás eu fiquei >>>>> sabendo do Princípio da Partição, >>>>> >>>>> Se ele está acompanhando a coisa, trata-se de um especialista no >>>>> assunto, muito bem ! >>>>> >>>>> Atés >>>>> >>>>> []s Samuel >>>>> >>>>> Em sexta-feira, 9 de outubro de 2020 às 17:43:11 UTC-4, marciopalmares >>>>> escreveu: >>>>> >>>>>> Oi, Valeria! >>>>>> >>>>>> Que bom que Adonai respondeu à sua pergunta... Eu sempre pensei >>>>>> assim: todo epimorfismo pode ser cindido em Set, temos portanto uma >>>>>> versão >>>>>> categorial do axioma da escolha, sabemos que o axioma da escolha implica >>>>>> a >>>>>> lei do terceiro escolhido, então saberemos como é a álgebra dos >>>>>> subobjetos >>>>>> nas categorias em que vale o AE, e pronto! É tudo o que precisamos saber >>>>>> sobre axioma de escolha! (Eu nem sabia que esse problema do Princípio da >>>>>> Partição existia...). >>>>>> >>>>>> Como Adonai mencionou, o artigo chamou a atenção de Asaf Karagila. >>>>>> Ele fez uma postagem em seu blog e está comentando passo a passo, à >>>>>> medida >>>>>> em que progride na leitura pelo twitter: >>>>>> http://karagila.org/2020/going-with-the-flow/ (São muito divertidos >>>>>> os comentários.) >>>>>> >>>>>> Esse primeiro artigo está completamente focado em demonstrar o >>>>>> resultado principal, e também em provar que os axiomas de ZF são teoremas >>>>>> quando traduzidos em Flow. Mas estamos trabalhando também em outra >>>>>> frente: >>>>>> mostrar que o sistema que William Lawvere sugeriu em 1966 (category of >>>>>> categories as a foundation) também pode ser imerso em Flow, isto é, os >>>>>> axiomas da teoria de primeira ordem sugeridos por Lawvere são teoremas em >>>>>> Flow, quando devidamente traduzidos. >>>>>> >>>>>> Seria muito legal se o artigo despertasse também atenção dos >>>>>> categoristas, apesar de, por restrições de tamanho e pelo resultado >>>>>> obtido, >>>>>> ter ficado restrito a teoria de conjuntos, teoria de modelos. >>>>>> >>>>>> Abraços! >>>>>> >>>>>> M. >>>>>> >>>>>> >>>>>> >>>>>> >>>>>> Em sex., 9 de out. de 2020 às 18:34, Adonai S. Sant'Anna < >>>>>> [email protected]> escreveu: >>>>>> >>>>>>> Valeria >>>>>>> >>>>>>> Longa história para responder à sua pergunta. Se o trabalho estiver >>>>>>> certo, nossa teoria geral de funções Flow permite exibir modelo de ZF >>>>>>> onde >>>>>>> vale PP mas não AE. Isso é conseguido graças a um axioma de F-Escolha >>>>>>> que >>>>>>> sugerimos em nosso trabalho. Esse axioma de F-Escolha permite PP como >>>>>>> teorema. No entanto, existe ZF-conjunto (ZF-conjuntos são termos de Flow >>>>>>> que correspondem a conjuntos de ZF num sentido preciso) que não pode ser >>>>>>> bem ordenado. Logo, não vale AE. Não somos os únicos que desconfiaram >>>>>>> que >>>>>>> AE independe de PP. Asaf Karagila admitiu por e-mail ter a mesma >>>>>>> impressão. >>>>>>> Estamos conversando com ele sobre isso. Em breve teremos mais novidades >>>>>>> (boas ou ruins, só Deus sabe). >>>>>>> >>>>>>> Abraço >>>>>>> >>>>>>> Adonai >>>>>>> >>>>>> Em sex, 9 de out de 2020 às 5:42 PM, Valeria de Paiva < >>>>>>> [email protected]> escreveu: >>>>>>> >>>>>> Marcio, Samuel, >>>>>>>> e voces conseguem dizer *por que* o principio da particao 'vale em >>>>>>>> ZF, mas o axioma da escolha nao? >>>>>>>> porque tinha uma razao pra pensar que eles seriam equivalentes, ne? >>>>>>>> qual era essa razao? >>>>>>>> obrigada, >>>>>>>> Valeria >>>>>>>> >>>>>>>> On Fri, Oct 9, 2020 at 1:32 PM samuel <[email protected]> wrote: >>>>>>>> >>>>>>>>> Caros, >>>>>>>>> >>>>>>>>> Renato Brodzinski (outro dos autores) tinha me avisado mais cedo >>>>>>>>> desse trabalho. Por acaso, o seminário que eu vou apresentar em >>>>>>>>> novembro >>>>>>>>> fala, precisamente, do Princípio da Partição ! >>>>>>>>> >>>>>>>>> Se tudo der certo, eles resolveram só o problema mais antigo da >>>>>>>>> Teoria dos Conjuntos (com mais de 100 anos em aberto). >>>>>>>>> >>>>>>>>> Atés e parabéns pelo trabalho, >>>>>>>>> >>>>>>>>> []s Samuel >>>>>>>>> >>>>>>>>> Em sexta-feira, 9 de outubro de 2020 às 08:29:14 UTC-4, >>>>>>>>> marciopalmares escreveu: >>>>>>>>> >>>>>>>>>> Olá, pessoal! >>>>>>>>>> >>>>>>>>>> Estamos divulgando nosso trabalho sobre a teoria Flow, uma teoria >>>>>>>>>> geral sobre funções, cujo propósito inicial era fornecer um >>>>>>>>>> framework tanto >>>>>>>>>> para a teoria de categorias quanto para ZF. No meio do caminho, >>>>>>>>>> Adonai >>>>>>>>>> resolveu o problema em aberto do princípio da partição, isto é, >>>>>>>>>> construiu >>>>>>>>>> um modelo para ZF em Flow em que vale o princípio da partição mas >>>>>>>>>> não o >>>>>>>>>> axioma de escolha, e agora a Teoria Flow conta com um cartão de >>>>>>>>>> visitas >>>>>>>>>> muito legal! >>>>>>>>>> >>>>>>>>>> Uma prévia do trabalho está disponível no arXiv: >>>>>>>>>> https://arxiv.org/abs/2010.03664 >>>>>>>>>> >>>>>>>>>> O objetivo de divulgar o preprint é recolher críticas, sugestões, >>>>>>>>>> antes da submissão para um periódico. Então, todas as críticas são >>>>>>>>>> bem-vindas! >>>>>>>>>> >>>>>>>>>> Obrigado! >>>>>>>>>> >>>>>>>>>> Abraços! >>>>>>>>>> >>>>>>>>>> M. >>>>>>>>>> >>>>>>>>>> >>>>>>>>>> >>>>>>>>>> >>>>>>>>>> >>>>>>>>> >>>>>>>>> >>>>>>>>> >>>>>>>>> >>>>>>>>> >>>>>>>>> >>>>>>>>> >>>>>>>>> >>>>>>>>> -- >>>>>>>>> >>>>>>>>> >>>>>>>>> Você recebeu essa mensagem porque está inscrito 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 essa discussão na Web, acesse >>>>>>>>> https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/8335ff82-f056-426b-b53c-95cef9dbacban%40dimap.ufrn.br >>>>>>>>> <https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/8335ff82-f056-426b-b53c-95cef9dbacban%40dimap.ufrn.br?utm_medium=email&utm_source=footer> >>>>>>>>> . >>>>>>>>> >>>>>>>>> >>>>>>>>> >>>>>>>> >>>>>>>> -- >>>>>>>> Valeria de Paiva >>>>>>>> http://vcvpaiva.github.io/ >>>>>>>> http://www.cs.bham.ac.uk/~vdp/ >>>>>>>> >>>>>>>> >>>>>>>> >>>>>>>> >>>>>>>> >>>>>>>> >>>>>>>> >>>>>>>> >>>>>>>> >>>>>>>> >>>>>>>> -- >>>>>>>> >>>>>>>> >>>>>>>> Você recebeu essa mensagem porque está inscrito 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 essa discussão na Web, acesse >>>>>>>> https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAESt%3DXuUF49LXeNoStYW9wR20FtxcYi6sXu8HftR-SJ-WXSjow%40mail.gmail.com >>>>>>>> <https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAESt%3DXuUF49LXeNoStYW9wR20FtxcYi6sXu8HftR-SJ-WXSjow%40mail.gmail.com?utm_medium=email&utm_source=footer> >>>>>>>> . >>>>>>>> >>>>>>>> >>>>>>>> -- >>>>>>> Adonai S. Sant'Anna >>>>>>> DMAT/UFPR >>>>>>> >>>>>>> 6accdæ13eff7i319n4o4qrr4s8t12vz >>>>>>> >>>>>> >>> >>> -- >>> Valeria de Paiva >>> http://vcvpaiva.github.io/ >>> http://www.cs.bham.ac.uk/~vdp/ >>> >>> >>> -- >>> Você recebeu essa mensagem porque está inscrito 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 essa discussão na Web, acesse >>> https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/1621402665.2982199.1602284649723.JavaMail.zimbra%40ufba.br >>> <https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/1621402665.2982199.1602284649723.JavaMail.zimbra%40ufba.br?utm_medium=email&utm_source=footer> >>> . >>> >> >> >> -- >> Valeria de Paiva >> http://vcvpaiva.github.io/ >> http://www.cs.bham.ac.uk/~vdp/ >> >> -- Valeria de Paiva http://vcvpaiva.github.io/ http://www.cs.bham.ac.uk/~vdp/ -- 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/CAESt%3DXtWv05vD_jqt24EK8jfG9Fmd7rn9vO5n9yixpp_7fr4jA%40mail.gmail.com.
