Oi Ruy,
obrigado pelas dicas, eu nunca tinha ouvido falar de "labelled
deductive systems" antes (ô, ignorânça! 8-\)... ainda não consegui
cópias dos artigos que você recomendou - por acaso seria fácil você me
enviar um preprint de algum deles por internet? Só vou ter tempo de ir
a uma biblioteca grande daqui a umas três semanas - estou trabalhando
num campus da UFF no interior do estado do Rio de Janeiro, aqui a
conexão de internet é muito, muito, MUITO ruim, e é dificílimo fazer o
Periódicos Capes funcionar (mas existem boatos de que dá pra baixar
arquivos por ele).
Mas bom, voltando ao que interessa: encontrei bem pouca coisa online
sobre LDS, mas a partir destes dois artigos
Broda/Finger/Russo: "Labelled Natural Deduction for Substructural
Logics" (1997):
http://pubs.doc.ic.ac.uk/LDSSubstructuralLogic/LDSSubstructuralLogic.pdf
Broda/D'Agostino/Russo: "Transformation Methods in LDS" (1999)
http://pubs.doc.ic.ac.uk/TransformationMethods1999/TransformationMethods1999.ps
e do livro "Labelled Deductive Systems, vol. 1", do Gabbay, já deu pra
ter uma boa noção das técnicas básicas...
(Vou tentar escrever o resto da mensagem de um modo que seja mais ou
menos útil para outras pessoas - tomara que funcione.)
Na mensagem que eu acabei de mandar pra Elaine aparecia esta derivação
daqui:
a,b,b';Pabb'|-Qabb'
----------------------
a,b,b';T|-Pabb'->Qabb'
------------------------------
a,b|-b a,b;T|-\forall b'.Pabb'->Qabb'
----------------------------------------
a,b;T|-Pabb->Qabb
-----------------
a,b;Pabb|-Qabb
na qual cada "sequente com as variáveis livres listadas antes do
ponto-e-vírgula" (i.e., todos os da derivação, exceto o a,b|-b) pode
ser interpretado como uma inclusão de subconjuntos. Por exemplo,
a,b,b';Pabb'|-Qabb'
"é" a inclusão:
{(a,b,b')|Pabb'} \subseteq {(a,b,b')|Qabb}
mas esta interpretação de "sequentes" como "inclusões" é meio restrita
- ela nos força a ver o "a,b|-b" como algo de uma natureza
completamente diferente... como você apontou, o "b" na regra de
eliminação do "forall",
b \forall b'.Pabb'->Qabb'
---------------------------\forall E
Pabb'->Qabb'
é um cidadão de segunda classe... mas se a gente passa pra
interpretação mais geral, na qual tudo são "judgments", então o
"a,b|-b" é
a:A.b:B|-b:B
ou seja, "se eu sei o valor da variável a (e esse valor mora em A) e
eu sei o valor da variável b (e ele mora em B) então sei o valor do
termo b à direita do `|-' (e esse valor mora em B)"... e aí o
isomorfismo de Curry-Howard entra para podermos interpretar "Qabb'",
"Pabb'->Qabb'", etc, como "termos".
Acho que já entendi como usar um LDS para inferir as variáveis antes
do ";" em cada nó da derivação acima - ou seja, como começar com uma
derivação em Dedução Natural para lógica de 1ª ordem e transformá-la
numa derivação em "cálculo de sequentes com as variáveis livres
listadas antes do ponto-e-vírgula" (isto exige certos cuidados - vejam
o comentário de um leitor em
http://www.amazon.com/Introduction-Higher-Order-Categorical-Cambridge-Mathematics/dp/0521356539/
e a p.131 do livro), e, melhor ainda, agora estou começando a ter a
impressão de que usando LDSs deve dar pra estender esses sistemas de
Dedução Natural para sistemas de tipos com "dependent types"... Todas
as tentativas que eu já tinha visto de Dedução Natural para DTT eram
de arrancar os cabelos, mas elas eram anteriores à invenção dos
LDSs...
Alguém quer me recomendar algum artigo sobre dedução natural com
"dependent types"? 8-)
Obrigado, [[]]s,
Eduardo Ochs
[email protected]
http://angg.twu.net/
2010/6/18 Ruy de Queiroz <[email protected]>:
> 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
> ----
>
> 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.
> de Queiroz, R. & Gabbay, D.: 1999, `Labelled Natural Deduction'. In Logic,
> Language and Reasoning. Essays in Honor of Dov Gabbay, H.J. Ohlbach and U.
> Reyle (eds.), volume 5 of Trends in Logic series, Kluwer Academic
> Publishers, Dordrecht, June 1999, pp. 173-250.
> de Oliveira, A. & de Queiroz, R.: 1999, `A Normalization Procedure for the
> Equational Fragment of Labelled Natural Deduction'. Logic Journal of the
> Interest Group in Pure and Applied Logics, 7(2):173-215, 1999, Oxford Univ.
> Press. Full version of a paper presented at 2nd WoLLIC'95, Recife, Brazil,
> July 1995. Abstract appeared inJournal of the Interest Group in Pure and
> Applied Logics 4(2):330-332, 1996.
> 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 <[email protected]>
> 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 <[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
>
>
> _______________________________________________
> Logica-l mailing list
> [email protected]
> http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
>
>
_______________________________________________
Logica-l mailing list
[email protected]
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
