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/883c0ec9-edf9-488c-82fd-38d098bbd678%40dimap.ufrn.br.
