oi Elaine e Eduardo, eu tinha comecado a escrever pra dizer que a pessoa indicada pra responder era o Ruy, quando notei que ele ja tinha escrito..oba, e' bom quando listas funcionam..
mas tb fiquei pensando que a pergunta do Eduardo leva pra dois lados meio diferentes que nao sei se os papers que o Ruy citou resolvem. Um 'e o lado da modelagem categorica, que 'e o paper do Seely que o Eduardo estava lendo. Outro aspecto que acho que o Ruy pode clarificar um tanto 'e a generalizacao de igualdade pra teoria de tipos do Martin-Loeuf. assisti a uma palestra recente e parece que a estoria do UIP (uniqueness of identity proofs) parece que da' panos pra manga...Se tiver um resuminho de um paragrafo que possa ser feito sobre o assunto, eu agradeceria bastante.. abracos, Valeria 2010/6/18 Elaine Pimentel <[email protected]>: > 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 <[email protected]>: >> 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 >> [email protected] >> http://angg.twu.net/ >> _______________________________________________ >> Logica-l mailing list >> [email protected] >> 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 > [email protected] > http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l > -- Valeria de Paiva http://www.cs.bham.ac.uk/~vdp/ http://valeriadepaiva.org/www/ _______________________________________________ Logica-l mailing list [email protected] http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
