Caros Eliane, Eduardo, e demais colegas, Uma teoria da prova para a igualdade pode ser formulada de forma mais "natural" quando termos e símbolos de função são "cidadãos de primeira classe", o que não ocorre com a Dedução Natural de Prawitz, tampouco com o Cálculo de Seqüentes de Gentzen. A interpretação funcional de Curry-Howard (e suas extensões, como, por exemplo, a "Dedução Natural Rotulada") se apresenta como um arcabouço mais apropriado.
Temos trabalhado nisso há algum tempo, e no final desta mensagem incluo algumas referências bibliográficas. Um abraço, Ruy ---- 1. de Queiroz, R. & de Oliveira, A.: 200?, `Natural Deduction for Equality: The Missing Entity'. In *Advances in Natural Deduction*, E. H. Haeusler, L. C. Pereira & V. de Paiva (eds.), Kluwer, to appear. 2. de Queiroz, R. & Gabbay, D.: 1999, `Labelled Natural Deduction'. In *Logic, Language and Reasoning. Essays in Honor of Dov Gabbay*<http://www.springer.com/dal/home/philosophy/logic?SGWID=1-40392-22-33743914-0>, H.J. Ohlbach and U. Reyle (eds.), volume 5 of *Trends in Logic*<http://www.springer.com/dal/home/philosophy/logic?SGWID=1-40392-69-173624612-0> series, Kluwer Academic Publishers, Dordrecht, June 1999, pp. 173-250. 3. de Oliveira, A. & de Queiroz, R.: 1999, `A Normalization Procedure for the Equational Fragment of Labelled Natural Deduction<http://www.oup.co.uk/igpl/Volume_07/Issue_02/#oliviera> '. *Logic Journal of the Interest Group in Pure and Applied Logics*<http://www.oup.co.uk/igpl> , *7*(2):173-215 <http://www.oup.co.uk/igpl/Volume_07/Issue_02/>, 1999, Oxford Univ. Press. Full version of a paper presented at *2nd WoLLIC'95*<http://wollic.org/wollic95/welcome.txt>, Recife, Brazil, July 1995. Abstract appeared in*Journal of the Interest Group in Pure and Applied Logics* <http://www.oup.co.uk/igpl> *4*(2):330-332, 1996. 4. de Queiroz, R. & Gabbay, D.: 1994, `Equality in Labelled Deductive Systems and the Functional Interpretation of Propositional Equality'. In *Proceedings of the Ninth Amsterdam Colloquium*, Paul Dekker & Martin Stokhof (eds.), ILLC/Department of Philosophy, University of Amsterdam, 1994, pp. 547-565. Em 18 de junho de 2010 04:54, Elaine Pimentel <elaine.pimen...@gmail.com>escreveu: > Oi, Eduardo, > > Eu nao sou expert em deducao natural, mas me parece que a prova e' essa: > > Pabb'|-Qabb' b=b' > ------------------------- > Pabb'|-Qabb |-Pabb b=b' > ----------------- --------------- > |-Pabb' => Qabb |-Pabb' > ------------------------------------- > |-Qabb > > Abraco, > > Elaine. > > 2010/6/18 Eduardo Ochs <eduardoo...@gmail.com>: > > Oi pessoas, > > > > acabei de descobrir, pela n-ésima vez, que eu sei menos de Dedução > > Natural do que deveria... 8-\ > > > > Eu imaginava que as regras para igualdade fossem: > > > > ---=I > > b=b > > > > b=b' Pabb > > ----------=E > > Pabb' > > > > e a partir delas todas as outras propriedades "naturais" da igualdade > > pudessem ser obtidas como regras derivadas... eu consigo > > reflexividade, simetria, transitividade e um monte de outras, mas não > > estou conseguindo substituição (b':=b): > > > > [Pabb'] > > : > > Qabb' Pabb > > ===========subst > > Qabb > > > > Alguém sabe como derivá-la? > > > > Pra piorar: descobri (mas tomara que eu esteja errado) que o Prawitz > > fala bem pouco sobre igualdade no "Natural Deduction"... Num artigo > > que eu estou tentando ler com todos os detalhes, > > > > http://www.math.mcgill.ca/rags/ZML/ZML.PDF > > > > as regras "=I" e "=E" aparecem, mas nem sei de onde é que o autor as > > tirou... Dicas?... 8-/ > > > > Obrigado, > > Eduardo Ochs > > eduardoo...@gmail.com > > http://angg.twu.net/ > > _______________________________________________ > > Logica-l mailing list > > Logica-l@dimap.ufrn.br > > http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l > > > -- > Elaine. > ------------------------------------------------- > Elaine Pimentel - DMat/UFMG > > Address: Departamento de Matematica > Universidade Federal de Minas Gerais > Av Antonio Carlos, 6627 - C.P. 702 > Pampulha - CEP 30.161-970 > Belo Horizonte - Minas Gerais - Brazil > Phone: 55 31 3409-5970/3409-5994 > Fax: 55 31 3409-5692 > http://www.mat.ufmg.br/~elaine > ------------------------------------------------- > _______________________________________________ > Logica-l mailing list > Logica-l@dimap.ufrn.br > http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l >
_______________________________________________ Logica-l mailing list Logica-l@dimap.ufrn.br http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
