> Considero a existência de duas operações sintáticas: instanciação e > substituição. > > A instanciação diz respeito à troca de ocorrências livres de variáveis por > termos, sendo que o ideal é renomear as variáveis ligadas nas quais a > variável instanciada esteja em sua faixa. É usada na formulação de pelo > menos três das quatro leis de introdução e eliminação dos quantificadores > universal e existencial, sendo que, em uma lógica como a intuicionista, por > exemplo, é necessário usar a instanciação na formulação das quatro leis.
Você estaria falando das "leis" de dedução natural? Neste caso, por que "três" e não "duas" ou "quatro"? (em dedução automática, ambas a introdução do universal e a eliminação do existencial tratam as variáveis envolvidas como *parâmetros*, enquanto que as outras regras tratam as variáveis como *incógnitas*) > A substituição diz respeito à troca das ocorrências "reais" (segundo a minha > formulação) de termos por termos ou de fórmulas por fórmulas. É usada na > formulação das leis de substituição de termos por termos (onde igualdades > geram novas igualdades) e de fórmulas por fórmulas (onde equivalências geram > novas equivalências). Você estaria tratando aqui daquilo que a literatura de computação chama de *reescrita*? > Acontece porém, que os livros de Lógica confundem, em geral, estas duas > operações, no caso da troca de variáveis por termos. Você poderia dar exemplo de livros que dizem coisas equivocadas graças a esta "confusão". > Dou abaixo um exemplo mostrando a diferença. > > Notação: > P(x|t) - denota a instanciação de uma variável x por um termo t em uma > fórmula P > P(x||t) - denota a substituição de uma variável x por um termo t em uma > fórmula P > > Considere P a fórmula Ay p(x,y) e q(x,y,z), onde "A" representa o > quantificador universal, e "e" representa o conectivo da conjunção. > > P(x|y + z) = (Aw p(x,w) e q(x,y,z)) (x|y + z) = Aw p(y + z,w) e q(y + > z,y,z) (observe aqui a necessidade de renomear a variável ligada y para uma > nova variável w antes de trocar as ocorrências livres de x por y + z em P, a > fim de que ocorrências livres de variáveis em "y + z" não passem a ser > ligadas no resultado) (diversos livros de Lógica não apresentam este > cuidado, mas isto dá diversos problemas posteriores). Isto não poderia ser resolvido com mais facilidade simplesmente se você usasse dois alfabetos diferentes, um para variáveis livres e outro para variáveis ligadas, reconhecendo assim de uma vez por todas que se tratam de dois animais de espécies muito diferentes? > P(x||y + z) = Ayp(y + z,y) e q(y + z,y,z) (aqui não há o cuidado de > renomeação que é considerado na instanciação, porque esta operação tem em > Lógica outras aplicações, distintas das aplicações da instanciação). Quais aplicações? * * * Nem toda "instância de substituição" parece envolver a troca de "variáveis" por "termos"... Outra questão que você talvez queira levar em consideração, no seu artigo e no seu curso, é o fato de que algumas lógicas não validam regras (globais) de *substituição uniforme* irrestritas, segundo as quais uma inferência já estabelecida como correta permaneceria correta ao trocarmos uniformemente variáveis atômicas por fórmulas quaisquer. Lógicas não-monotônicas, em geral, só admitem, sem abrir mão da correção, a substituição uniforme de átomos por outros átomos. * * * JM _______________________________________________ Logica-l mailing list [email protected] http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
