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/ > 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/CAJGvw-3rtaS6%2B45LRrLi9J- > eefupmA9LRJO95ZHcxHFaZ7Mi6g%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ê 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/CAESt%3DXuqsrVGenCd0Mq2P7xmUzosbx%2BTXweGo69xfb6vp%3D8F7A%40mail.gmail.com.
