> > A sintaxe do sistema é brevemente explicada aqui > <https://github.com/bbentzen/Cubo/tree-save/master/README.md>.
Uma pequena correção: o link acima está quebrado (obrigado por me avisar, Eduardo!), o endereço correto do README é este aqui <https://github.com/bbentzen/Cubo/blob/master/README.md>. On Tuesday, October 24, 2017 at 9:51:51 PM UTC+8, Bruno Bentzen wrote: > > Oi Valéria, > > Acrescentando meus dois centavos: > > Nos últimos anos comecei a brincar um pouco com uma implementação de um > checador de tipos em C, o resultado foi um mini checador de tipos "for fun" > para uma versão extendida do Cálculo lambda simplesmente tipado. Batizei o > pequeno sistema de "Cubo". > > Uma lista razoável com provas de mais de 40 proposições válidas > intuicionisticamente (incluindo grande parte dos teoremas listados na > entrada citada da Wikipedia) pode ser achada nesta mini biblioteca > <https://github.com/bbentzen/Cubo/blob/master/Library> do Cubo. A sintaxe > do sistema é brevemente explicada aqui > <https://github.com/bbentzen/Cubo/tree-save/master/README.md>. Quaisquer > comentários são bem-vindos. :) > > Claro, o Cubo (mal-programado, mas consistente!) é apenas uma criança, mas > no futuro pretendo incluir suporte para tipos dependentes e universos > também. Bem, quem sabe um dia ele não se tornará um adulto que possa servir > como checador de tipos para uma teoria de tipos cúbica? (Daí a origem do > nome) > > Abraços lógicos, > Bruno > > -- > Bruno Bentzen > https://sites.google.com/site/bbentzena/ > > On Tuesday, October 24, 2017 at 7:00:02 AM UTC+8, valeria.depaiva 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_logic&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ê 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/85d1a3e4-24c6-4bfb-b88d-af01c5556bd1%40dimap.ufrn.br.
