Oi Valéria, Obrigado pelas referências. O Chico respondeu sim. Pelas suas referencias ficou mais claro: são só (bi)hiperdoutrinas de categorias bicartesianas fechadas e cocartesianamente cofechadas (nome muito grande!). Nem sabia que isso tinha utilidade. O caso monoidal parece ser mais interessante, mas mesmo o caso (co)cartesiano parece que não implica ser uma algebra Booleana nessas referencias. Portanto algum axioma da diferença simétrica que o Chico usa não deve valer nessas categorias.
Abs. Em 25 de outubro de 2017 20:51, Valeria de Paiva <valeria.depa...@gmail.com> escreveu: > oi Fernando, > provavelmente o Chico ja respondeu, mas se nao, de uma olhada em > https://arxiv.org/abs/1708.05896 > A Cointuitionistic Adjoint Logic > > ou Crolard's papers: > > > - > > “A formulae-as-types interpretation of Subtractive Logic > <http://cedric.cnam.fr/cpr/crolard/publications/jlc.pdf>”. T. Crolard. > *Journal > of Logic and Computation. Special issue on Intuitionistic Modal Logic and > Application.* Volume 14, Issue 4, August 2004. pp 529-570. > > *Abstract.* We present a formulae-as-types interpretation of > Subtractive Logic (*i.e.* bi-intuitionistic logic). This presentation > is two-fold: we first define a very natural restriction of the λμ-calculus > which is closed under reduction and whose type system is a constructive > restriction of the Classical Natural Deduction. Then we extend this > deduction system conservatively to Subtractive Logic. From a computational > standpoint, the resulting calculus provides a type system for first-class > coroutines (a restricted form of first-class continuations). > - > > “Subtractive logic > <http://cedric.cnam.fr/cpr/crolard/publications/tcs.pdf>”. T. Crolard. > *Theoretical > Computer Science* 254:1–2(2001):151-185.*Abstract.* This paper is the > first part of a work whose purpose is to investigate duality in some > related frameworks (cartesian closed categories, lambda-calculi, > intuitionistic and classical logics) from syntactic, semantical and > computational viewpoints. We start with category theory and we show that > any bicartesian closed category with coexponents is degenerated (i.e. there > is at most one arrow between two objects). The remainder of the paper is > devoted to logical issues. We examine the propositional calculus underlying > the type system of bicartesian closed categories with coexponents and we > show that this calculus corresponds to subtractive logic: a conservative > extension of intuitionistic logic with a new connector (subtraction) dual > to implication. Eventually, we consider first order subtractive logic and > we present an embedding of classical logic into subtractive logic. > > abs > Valeria > > 2017-10-25 3:21 GMT-07:00 Fernando Yamauti <fgyama...@gmail.com>: > >> Oi Chico, >> >> Só uma pergunta idiota. Que adjunção entre a diferença simétrica e a >> disjunção (que voce havia citado) é essa? Suponho que deva ser algo que >> vale em qualquer topos Booleano, mas mesmo em Set algo do tipo (-) \vee A >> -| (-) \Delta A (ou o contrario), onde ambos endofuntores são entre o >> reticulado dos subobjetos, não parece ser verdade. Portanto acho que voce >> esta pensando em algo menos obvio que isso, mas não consegui descobrir o >> que é... >> >> Abs. >> >> >> Em 24 de outubro de 2017 04:08, Francisco Miraglia <mirag...@ime.usp.br> >> escreveu: >> >>> Cara Valéria, >>> >>> Observações que talvez possam ser úteis: >>> >>> 1) O esquema (A --> B) --> (Ng A --> Ng B) é válido no Intucionismo, >>> (versão Heyting); as álgebras de Heyting fornecem uma semântica completa >>> para a versão do Intuicionismo do Arend; >>> >>> 2) Adicionar o esquema recíproco à axiomatização de Heyting da Lógica >>> Intucionista imediatamente fornece a Lógica Clássica; é semelhante ao >>> que acontece com a equivalência no sistema Intuicionista: se for >>> distributiva, a Lógica é clássica. >>> >>> 3) Estou insistindo em incluir o nome do Arend pois afinal nem sempre >>> nos lembramos que o Brower tinha a firme opinião que a sua visão da >>> Lógica era impossível (por definição, já que envolvia a "prática >>> quotidiana dos matemáticos") de ser axiomatizada. >>> >>> 4) Interessante observar que posições filosóficas não se materializam >>> na "prática quotidiana dos matemáticos": um dos resultados mais conhecidos >>> de Brower (toda função contínua do disco de dimensão n em sí mesmo possui >>> ponto fixo) é estabelecido pelo próprio por contradição! >>> O primeiro passo da contradição já é de ordem grande: não há retração >>> contínua do disco em sua borda (em qualquer dimensão n maior ou igual a >>> 1), o que exige métodos homológicos ou homotópicos); exibir o ponto fixo: >>> "para com isso".... >>> >>> 5) Quanto à nomenclatura, tanto Heyting, quanto Kleene (e Vesley) dão o >>> nome de contraposição ao esquema em (1), sempre chamando a atenção de que , >>> no Intuicionismo segundo Arend, difere da regra de contraposição clássica, >>> que, em geral, é enunciada como o esquema "contrapositivo", mencionado em >>> (2). >>> >>> (6) Não me lembro de ler acerca dessas coisas no livro do Dummet (mas >>> também não foi lá que aprendi a lidar com o intuicionismo do Arend), porém >>> sabes como é: a memória não é mais o que era, sendo substituída pela >>> "prática quotidiana" de utilizar metateoria intuicionista para fazer >>> Matemática. Exemplo: anéis de Gelfand (aqueles comutativos com unidade tais >>> que que por cima de todo ideal há apenas um maximal) são, >>> intuicionisticamente, fielmente quadráticos (possuem uma teoria de formas >>> quadráticas "bem comportada" e satisfazem a conjectura de Milnor). Isto já >>> é meio complicado; o caso clássico (que penso também ser verdadeiro) parece >>> ser ainda mais complicado. Interessante que os meus colegas de formas >>> quadráticas e K-teoria não dão a menor importância para a informação >>> intuicionista... >>> >>> (7) A relação intucionista da disjunção com a implicação resume-se ao >>> óbvio; qualquer outra relação é FALSA (experimente nos abertos da reta >>> real). Ou seja, na minha opinião, "barking up the wrong tree". >>> >>> Como voce sabe muito bem, o modo mais adequado de tratar estes conceitos >>> é via adjunções: a implicação é adjunta da conjunção, enquanto que a >>> disjunção é, classicamente, adjunta da diferença simétrica (o complementar >>> clássico da equivalência); porém esta última adjunção está longe de ser >>> intuicionisticamente válida. Aliás, se um reticulado distribitivo possui >>> uma operação parecida com a diferença simétrica, tem que ser uma álgebra de >>> Boole. Aqui começam a aparecer diferenças conceituais importantes e a >>> necessidade de empregar >>> outras noções, mais gerais (e.g., functores adjuntos), para construir >>> Lógicas. Já escrevi demais.... >>> >>> >>> Um grande abraço, >>> >>> Chico Miraglia >>> >>> >>> >>> >>> >>> >>>> On Oct 23, 2017 9:00 PM, "Valeria de Paiva" <valeria.depa...@gmail.com> >>>> wrote: >>>> >>>> prezados colegas, >>>>> >>>>> estou com um probleminha na wikipedia e em vez de gastar o tempo que >>>>> precisaria pra achar minha copia do Dummett em casa, resolvi apelar >>>>> pros >>>>> amigos. >>>>> >>>>> Acho que tem um "erro" em https://en.wikipedia.org/ >>>>> wiki/Intuitionistic_logic >>>>> onde na secao 9 alguem diz que: >>>>> >>>>> Relation to classical logic[edit >>>>> <https://en.wikipedia.org/w/index.php?title=Intuitionistic_l >>>>> ogic&action=edit§ion=9> >>>>> ] >>>>> >>>>> The system of classical logic is obtained by adding any one of the >>>>> following axioms: >>>>> >>>>> - {\displaystyle \phi \lor \lnot \phi }[image: \phi \lor \lnot >>>>> \phi] (Law >>>>> of the excluded middle. May also be formulated as {\displaystyle >>>>> (\phi >>>>> \to \chi )\to ((\lnot \phi \to \chi )\to \chi )}[image: (\phi \to >>>>> \chi >>>>> ) \to ((\lnot \phi \to \chi ) \to \chi )].) >>>>> - {\displaystyle \lnot \lnot \phi \to \phi }[image: \lnot \lnot \phi >>>>> \to \phi] (Double negation elimination) >>>>> - {\displaystyle ((\phi \to \chi )\to \phi )\to \phi }[image: ((\phi >>>>> \to \chi ) \to \phi ) \to \phi] (Peirce's law) >>>>> - {\displaystyle (\lnot \phi \to \lnot \chi )\to (\chi \to \phi >>>>> )}[image: >>>>> {\displaystyle (\lnot \phi \to \lnot \chi )\to (\chi \to \phi )}] >>>>> (Law >>>>> of contraposition) >>>>> >>>>> >>>>> mas essa ultima assercao nao 'e o que eu chamaria de contraposicao. >>>>> Contraposicao usual 'e valida em logical intuicionista. >>>>> >>>>> o que acontece e' que essa assercao combina contraposicao com >>>>> eliminacao >>>>> da negacao dupla, ou seja: >>>>> >>>>> contraposicao devia ser >>>>> >>>>> (A--> B) --> (\neg B --> neg A) >>>>> >>>>> mas quem escreveu o artigo em vez de dizer >>>>> >>>>> (\neg A-->\neg B) --> (\neg\neg B --> \neg\neg A), >>>>> removeu a dupla negacao, ficando com >>>>> (\neg A-->\neg B) --> ( B --> A) >>>>> >>>>> dai que isso 'e mesmo nao-derivavel em IL, pois inclui double >>>>> negation >>>>> elimination, junto com a contraposicao. >>>>> >>>>> voces concordam? ou eu estou "esquecendo" alguma coisa importante? >>>>> tem mais alguma coisa errada no artigo? >>>>> eu estou querendo me lembrar da relacao entre implicacao e disjuncao. >>>>> essas estao certas? >>>>> >>>>> Disjunction versus implication: >>>>> >>>>> - {\displaystyle (\phi \vee \psi )\to (\neg \phi \to \psi )}[image: >>>>> (\phi \vee \psi) \to (\neg \phi \to \psi)] >>>>> - {\displaystyle (\neg \phi \vee \psi )\to (\phi \to \psi )}[image: >>>>> (\neg \phi \vee \psi) \to (\phi \to \psi)] >>>>> >>>>> >>>>> obrigada pela ajuda, >>>>> Valeria >>>>> -- >>>>> Valeria de Paiva >>>>> http://vcvpaiva.github.io/ >>>>> http://research.nuance.com/author/valeria-de-paiva/ >>>>> 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 logica-l+unsubscr...@dimap.ufrn.br. >>>>> Para postar nesse grupo, envie um e-mail para logica-l@dimap.ufrn.br. >>>>> Acesse esse grupo em https://groups.google.com/a/ >>>>> dimap.ufrn.br/group/logica-l/. >>>>> Para ver essa discussão na Web, acesse https://groups.google.com/a/ >>>>> dimap.ufrn.br/d/msgid/logica-l/CAESt%3DXtQF5fvc8xt% >>>>> 2BaKJ2A5d6bw33taeFkFv0j_PCGJQ6UCSGg%40mail.gmail.com >>>>> <https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/ >>>>> CAESt%3DXtQF5fvc8xt%2BaKJ2A5d6bw33taeFkFv0j_PCGJQ6UCSGg%40ma >>>>> il.gmail.com?utm_medium=email&utm_source=footer> >>>>> . >>>>> >>>>> >>>> -- >>>> 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 logica-l+unsubscr...@dimap.ufrn.br. >>>> Para postar neste grupo, envie um e-mail para logica-l@dimap.ufrn.br. >>>> Visite este grupo em https://groups.google.com/a/di >>>> map.ufrn.br/group/logica-l/. >>>> Para ver esta discussão na web, acesse https://groups.google.com/a/di >>>> map.ufrn.br/d/msgid/logica-l/CAAPnweACzeBQqKjVR5jth2Y%3DzmqG >>>> mA_Pm4ssOPg5D6vGp%2B3AOA%40mail.gmail.com. >>>> >>> >>> >>> >>> -- >>> 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 logica-l+unsubscr...@dimap.ufrn.br. >>> Para postar neste grupo, envie um e-mail para logica-l@dimap.ufrn.br. >>> Visite este grupo em https://groups.google.com/a/di >>> map.ufrn.br/group/logica-l/. >>> Para ver esta discussão na web, acesse https://groups.google.com/a/di >>> map.ufrn.br/d/msgid/logica-l/20171024040835.Horde.FIpwwQ6QoR >>> zTHzQgYuI6dQ3%40webmail.ime.usp.br. >>> >> >> -- >> 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 logica-l+unsubscr...@dimap.ufrn.br. >> Para postar nesse grupo, envie um e-mail para logica-l@dimap.ufrn.br. >> Acesse esse grupo em https://groups.google.com/a/di >> map.ufrn.br/group/logica-l/. >> Para ver essa discussão na Web, acesse https://groups.google.com/a/di >> map.ufrn.br/d/msgid/logica-l/CAJGvw-3rtaS6%2B45LRrLi9J-eefu >> pmA9LRJO95ZHcxHFaZ7Mi6g%40mail.gmail.com >> <https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAJGvw-3rtaS6%2B45LRrLi9J-eefupmA9LRJO95ZHcxHFaZ7Mi6g%40mail.gmail.com?utm_medium=email&utm_source=footer> >> . >> > > > > -- > Valeria de Paiva > http://vcvpaiva.github.io/ > http://research.nuance.com/author/valeria-de-paiva/ > 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 logica-l+unsubscr...@dimap.ufrn.br. > Para postar nesse grupo, envie um e-mail para logica-l@dimap.ufrn.br. > Acesse esse grupo em https://groups.google.com/a/ > dimap.ufrn.br/group/logica-l/. > Para ver essa discussão na Web, acesse https://groups.google.com/a/ > dimap.ufrn.br/d/msgid/logica-l/CAESt%3DXuqsrVGenCd0Mq2P7xmUzosbx% > 2BTXweGo69xfb6vp%3D8F7A%40mail.gmail.com > <https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAESt%3DXuqsrVGenCd0Mq2P7xmUzosbx%2BTXweGo69xfb6vp%3D8F7A%40mail.gmail.com?utm_medium=email&utm_source=footer> > . > -- 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 logica-l+unsubscr...@dimap.ufrn.br. Para postar neste grupo, envie um e-mail para logica-l@dimap.ufrn.br. Visite este grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/. Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAJGvw-1ZuPQSRBREyfi39du1TbBt1kVTTiMtNidLgg50j2Cuqw%40mail.gmail.com.
