Oi Elaine,
do modo (torto? 8-)) como eu entendo cálculo de sequentes a sua
derivação para o subst
Pabb'|-Qabb'
subst
Pabb|-Qabb
acaba envolvendo uma hipótese extra, b=b', que nunca é descartada...
Mas acabei de encontrar uma solução, ó:
[Pabb']^1
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
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,
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
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
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
