Re: [Logica-l] Lançamento do livro "The Functional Interpretation of Logical Deduction" (World Scientific)

[Francisco Antonio Doria]

Aderiste às msgs via iPhone? :))

Me junto a teus parabens!!!

2011/11/12 Valeria De Paiva 

> Parabens Ruy e Ju!
>
> Sent from my iPhone
>
> On Nov 11, 2011, at 3:18 PM, Ruy de Queiroz  wrote:
>
> > Caros(as),
> >
> > Estão todos convidados a comparecer ao lançamento do nosso livro (em
> > parceria com Anjolina e Dov Gabbay):
> >
> > The Functional Interpretation of Logical
> > Deduction(World
> > Scientific, Oct 2011):
> >
> >
> > Onde: *SBS Livraria Internacional* (Av. Conselheiro Rosa e Silva 1519,
> > Recife, em frente à ABA-Aflitos)
> > Quando: 6a. Feira, 02/12/11, às 19hs.
> >
> > *Todos são bem-vindos!*
> >
> > RSVP para r...@cin.ufpe.br
> >
> > Ruy
> > ___
> > 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
>



-- 
fad

ahhata alati, awienta Wilushati
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l

Re: [Logica-l] Lançamento do livro "The Functional Interpretation of Logical Deduction" (World Scientific)

[Walter Carnielli]

Caro Ruy:

meus  sinceros parabéns à Angiolina, a você e ao Dov. Infelizmente,
esta  mensagem não vale como "RSVP"
porque Recife  está um tanto  longe... :-)
Mas  o Dov Gabbay tem tido  tantas  parcerias  por aqui que  já merece
 ser  considerado "um  lógioc  brasileiro", assim como
os australianos consideram o David Lewis  "an Australasian  logician"!

Abraços,

Walter


>> > Estão todos convidados a comparecer ao lançamento do nosso livro (em
>> > parceria com Anjolina e Dov Gabbay):
>> >
>> > The Functional Interpretation of Logical
>> > Deduction(World
>> > Scientific, Oct 2011):
>> >
>> >
>> > Onde: *SBS Livraria Internacional* (Av. Conselheiro Rosa e Silva 1519,
>> > Recife, em frente à ABA-Aflitos)
>> > Quando: 6a. Feira, 02/12/11, às 19hs.
>> >
>> > *Todos são bem-vindos!*
>> >
>> > RSVP para r...@cin.ufpe.br
>> >
>> > Ruy
>> > ___
>> > Logica-l mailing list
>> > Logica-l@dimap.ufrn.br
>> > http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l

---
Prof. Dr. Walter Carnielli
Director
Centre for Logic, Epistemology and the History of Science – CLE
State University of Campinas –UNICAMP
13083-859 Campinas -SP, Brazil
Phone: (+55) (19) 3521-6517
Fax: (+55) (19) 3289-3269
Institutional e-mail: walter.carnie...@cle.unicamp.br
Website: http://www.cle.unicamp.br/prof/carnielli
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l

[Logica-l] Nicolelis

[Francisco Antonio Doria]

http://www.cartacapital.com.br/sociedade/miguel-nicolelis-%E2%80%9Ceinstein-nao-seria-considerado-pesquisador-top-no-cnpq-brasileiro%E2%80%9D/#.Tr1UNtt6tlo.facebook

-- 
fad

ahhata alati, awienta Wilushati
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l

[Logica-l] Um "Banco de Teminologia"

[Walter Carnielli]

Caros Anderson  e Rodrigo,  caros todos os que têm  se esmerado na discussão
(notadamente, o João Marcos, Andréia e  Daniel, que me parece que mais
debateram ):

Parabenizo a todos pelo enorme esforço em digitar   milhares de
linhas e   manter  o  foco  da  discussão.

Acho que esta  proposta do Anderson é  muito boa:  talvez  fosse o
caso de   termos  um
"banco terminológico"  (não de  "notações", mas de termos sugeridos),
sem obviamente  nenhuma  "patrulha terminológica",  mas   que
nos ajudassem a escrever melhor.

Entro então na discussão colocando meus problemas  terminológicos  e
a solução que tenho adotado, para  iniciar a coisa:

- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
- - - - - - - - - - - - - - - - - - - - - - - - - - - -
Sugestões: Terminologia em Lógica e  Filosofia em Língua Portuguesa


1) "Forcing" (substantivo) :  Relação de forçamento

2) "Frame" (substantivo) :  enquadramento

3) "tableau"  e "tableaux"  (substantivos):   tablô e  tablôs

4) "claim"  (verbo) :  sustentar   ou alegar

5) "claim" (substantivo)  :  alegação

6) "dialethea" (substantivo) :   dialetéia

7) "dialetheic" (adjetivo)  :  dialetéica(o)

8) "model-theoretical" (adjetivo)  :  teórica(a) ou  modelo-teórica(o)

9) "negation-free" (adjetivo):  livre de  negações

10) " proof"  (substantivo) :   preferencialmente  'demonstração', mas
   mantendo   "Teoria da Prova"  no caso  específico da área.


- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
- - - - - - - - - - - - - - - - - - - - - - - - - - - -
Acho que a questão é importante: há  pouco tempo  o Chateaubriand me
escreveu  perguntando   como eu usaria
 "dialetheic"  para não confundir com "dialético".

*Não quero*  dizer  com isso  que uma discussão mais  profunda, como
aquela sobre  "consequência sintática"e "semântica, ou sobre a
distinção ( se  houver) entre "prova" e "demonstração"  devam ser
canceladas--simplesmente  não creio que esse tipo  de discussão se
resolve  na  Lista.
Talvez se  inicie na Lista, mas  só vai prosperar   (penso) com um
artigo competente e bem feito endereçando-se à questão.

Há  muito mais. Ficam como desafio "turnstile", "top" e  "bottom"...

Abs,

Walter

Em 11 de novembro de 2011 15:09, Anderson de Araújo
 escreveu:
> Rodrigo, concordo com você em ambos os pontos.
>
> É duro de engolir a expressão `computacionalmente saturado', mas,
> infelizmente, não tenho argumentos melhores do que aqueles apresentados
> pelo Soare e outros. Então, quando tenho em vista a versão informal, uso
> `efetivamente saturado' mas, quando está em questão uma versão formal
> qualquer, uso, a contragosto, `computacionalmente saturado'.
>
> Quanto à notação em lógica, realmente a situação é problemática; sobretudo
> em teoria dos modelos e teoria da computabilidade. Em particular, o exemplo
> que você apontou sobre a substituição de termos é emblemático. Algum tempo
> atrás, li alguns artigos de pesquisadores renomados em teoria dos modelos
> sobre quantificadores ramificados e fiquei incomodado com o descuido - e
> justo nesse tema no qual qualquer deslize compromete muito a compreensão
> dos resultados.
>
> Talvez fosse o caso de abrir uma linha de discussão sobre a notação em
> lógica aqui na lista. Quem sabe a coisa avança e no próximo EBL tenhamos
> uma espécie de `Convensão Notacional da SBL', construída via debate. Se
> essa iniciativa for endossada pelos membros mais experientes da lista, ela
> ganhará força.
>
> A unidade, assim como a discórdia, em ciência é um fator positivo. Também
> acredito que passaria uma boa imagem para os lógicos de `outros mares'
> saber que no Brasil há algo do tipo `Convensão Notacional da SBL'.
>
> Abraços,
>
> Anderson
>
>
>
> Em 11 de novembro de 2011 09:31, Rodrigo Freire 
> escreveu:
>
>> Claro Anderson, entendo o que você escreveu. Apenas apontei que as vezes
>> simplesmente não soa bem substituir "recursivamente" por "computavelmente".
>> Efetivamente saturado ficou bom.
>>
>> Outro ponto sobre a linguagem usada em lógica: notações. Acho que notação
>> é um ponto crítico em lógica.
>>
>> Acho que ainda não há um padrão de notação em lógica que seja
>> satisfatório. Por exemplo o símbolo usado para a relação de consequncia
>> semântica, uma barrinha vertical seguida por duas barrinhas horinzontais,
>> que é mais ou menos standard agora, é usado no mínimo para duas coisas
>> diferentes: para expressar que uma sentença é válida em uma estrutura e
>> para expressar que uma sentença é consequencia de uma teoria.
>>
>> Outra coisa: notação para substituição de termos: por exemplo, é comum
>> encontrarmos a notação A(a_1,...,a_n) para expressar a substituição
>> simultanea de variáveis x_1,..., x_n por a_1,...,a_n na fórmula A. É comum
>> também encontrar outras notações para a mesma coisa que explicitam as
>> variáveis x_1,..,x_n. Como há outras operações que podem ser realizadas nas
>> fórmulas, as vezes a notação não deixa claro qual é a ordem das operações.
>> Já vi uma

Re: [Logica-l] Um "Banco de Teminologia"

[Rodrigo Freire]

Olá Walter


Vou acrescentar uma sugestão:

11) set-theoretic: conjuntista.

E uma pergunta:

12) proof-theoretic: prova-teorética(o)?

Abraço
Rodrigo




2011/11/12 Walter Carnielli 

> Caros Anderson  e Rodrigo,  caros todos os que têm  se esmerado na
> discussão
> (notadamente, o João Marcos, Andréia e  Daniel, que me parece que mais
> debateram ):
>
> Parabenizo a todos pelo enorme esforço em digitar   milhares de
> linhas e   manter  o  foco  da  discussão.
>
> Acho que esta  proposta do Anderson é  muito boa:  talvez  fosse o
> caso de   termos  um
> "banco terminológico"  (não de  "notações", mas de termos sugeridos),
> sem obviamente  nenhuma  "patrulha terminológica",  mas   que
> nos ajudassem a escrever melhor.
>
> Entro então na discussão colocando meus problemas  terminológicos  e
> a solução que tenho adotado, para  iniciar a coisa:
>
> - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
> - - - - - - - - - - - - - - - - - - - - - - - - - - - -
> Sugestões: Terminologia em Lógica e  Filosofia em Língua Portuguesa
>
>
> 1) "Forcing" (substantivo) :  Relação de forçamento
>
> 2) "Frame" (substantivo) :  enquadramento
>
> 3) "tableau"  e "tableaux"  (substantivos):   tablô e  tablôs
>
> 4) "claim"  (verbo) :  sustentar   ou alegar
>
> 5) "claim" (substantivo)  :  alegação
>
> 6) "dialethea" (substantivo) :   dialetéia
>
> 7) "dialetheic" (adjetivo)  :  dialetéica(o)
>
> 8) "model-theoretical" (adjetivo)  :  teórica(a) ou  modelo-teórica(o)
>
> 9) "negation-free" (adjetivo):  livre de  negações
>
> 10) " proof"  (substantivo) :   preferencialmente  'demonstração', mas
>   mantendo   "Teoria da Prova"  no caso  específico da área.
>
>
> - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
> - - - - - - - - - - - - - - - - - - - - - - - - - - - -
> Acho que a questão é importante: há  pouco tempo  o Chateaubriand me
> escreveu  perguntando   como eu usaria
>  "dialetheic"  para não confundir com "dialético".
>
> *Não quero*  dizer  com isso  que uma discussão mais  profunda, como
> aquela sobre  "consequência sintática"e "semântica, ou sobre a
> distinção ( se  houver) entre "prova" e "demonstração"  devam ser
> canceladas--simplesmente  não creio que esse tipo  de discussão se
> resolve  na  Lista.
> Talvez se  inicie na Lista, mas  só vai prosperar   (penso) com um
> artigo competente e bem feito endereçando-se à questão.
>
> Há  muito mais. Ficam como desafio "turnstile", "top" e  "bottom"...
>
> Abs,
>
> Walter
>
> Em 11 de novembro de 2011 15:09, Anderson de Araújo
>  escreveu:
> > Rodrigo, concordo com você em ambos os pontos.
> >
> > É duro de engolir a expressão `computacionalmente saturado', mas,
> > infelizmente, não tenho argumentos melhores do que aqueles apresentados
> > pelo Soare e outros. Então, quando tenho em vista a versão informal, uso
> > `efetivamente saturado' mas, quando está em questão uma versão formal
> > qualquer, uso, a contragosto, `computacionalmente saturado'.
> >
> > Quanto à notação em lógica, realmente a situação é problemática;
> sobretudo
> > em teoria dos modelos e teoria da computabilidade. Em particular, o
> exemplo
> > que você apontou sobre a substituição de termos é emblemático. Algum
> tempo
> > atrás, li alguns artigos de pesquisadores renomados em teoria dos modelos
> > sobre quantificadores ramificados e fiquei incomodado com o descuido - e
> > justo nesse tema no qual qualquer deslize compromete muito a compreensão
> > dos resultados.
> >
> > Talvez fosse o caso de abrir uma linha de discussão sobre a notação em
> > lógica aqui na lista. Quem sabe a coisa avança e no próximo EBL tenhamos
> > uma espécie de `Convensão Notacional da SBL', construída via debate. Se
> > essa iniciativa for endossada pelos membros mais experientes da lista,
> ela
> > ganhará força.
> >
> > A unidade, assim como a discórdia, em ciência é um fator positivo. Também
> > acredito que passaria uma boa imagem para os lógicos de `outros mares'
> > saber que no Brasil há algo do tipo `Convensão Notacional da SBL'.
> >
> > Abraços,
> >
> > Anderson
> >
> >
> >
> > Em 11 de novembro de 2011 09:31, Rodrigo Freire  >escreveu:
> >
> >> Claro Anderson, entendo o que você escreveu. Apenas apontei que as vezes
> >> simplesmente não soa bem substituir "recursivamente" por
> "computavelmente".
> >> Efetivamente saturado ficou bom.
> >>
> >> Outro ponto sobre a linguagem usada em lógica: notações. Acho que
> notação
> >> é um ponto crítico em lógica.
> >>
> >> Acho que ainda não há um padrão de notação em lógica que seja
> >> satisfatório. Por exemplo o símbolo usado para a relação de consequncia
> >> semântica, uma barrinha vertical seguida por duas barrinhas
> horinzontais,
> >> que é mais ou menos standard agora, é usado no mínimo para duas coisas
> >> diferentes: para expressar que uma sentença é válida em uma estrutura e
> >> para expressar que uma sentença é consequencia de uma teoria.
> >>
> >> Outra coisa: notação para substituição de termos: por exe

Re: [Logica-l] Um "Banco de Teminologia"

[Francisco Antonio Doria]

2011/11/12 Rodrigo Freire 

> Olá Walter
>
>
> Vou acrescentar uma sugestão:
>
> 11) set-theoretic: conjuntista.
>
> E uma pergunta:
>
> 12) proof-theoretic: prova-teorética(o)?
>

Feio paca...

>
> Abraço
> Rodrigo
>
>
>
>
> 2011/11/12 Walter Carnielli 
>
> > Caros Anderson  e Rodrigo,  caros todos os que têm  se esmerado na
> > discussão
> > (notadamente, o João Marcos, Andréia e  Daniel, que me parece que mais
> > debateram ):
> >
> > Parabenizo a todos pelo enorme esforço em digitar   milhares de
> > linhas e   manter  o  foco  da  discussão.
> >
> > Acho que esta  proposta do Anderson é  muito boa:  talvez  fosse o
> > caso de   termos  um
> > "banco terminológico"  (não de  "notações", mas de termos sugeridos),
> > sem obviamente  nenhuma  "patrulha terminológica",  mas   que
> > nos ajudassem a escrever melhor.
> >
> > Entro então na discussão colocando meus problemas  terminológicos  e
> > a solução que tenho adotado, para  iniciar a coisa:
> >
> > - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
> > - - - - - - - - - - - - - - - - - - - - - - - - - - - -
> > Sugestões: Terminologia em Lógica e  Filosofia em Língua Portuguesa
> >
> >
> > 1) "Forcing" (substantivo) :  Relação de forçamento
> >
> > 2) "Frame" (substantivo) :  enquadramento
> >
> > 3) "tableau"  e "tableaux"  (substantivos):   tablô e  tablôs
> >
> > 4) "claim"  (verbo) :  sustentar   ou alegar
> >
> > 5) "claim" (substantivo)  :  alegação
> >
> > 6) "dialethea" (substantivo) :   dialetéia
> >
> > 7) "dialetheic" (adjetivo)  :  dialetéica(o)
> >
> > 8) "model-theoretical" (adjetivo)  :  teórica(a) ou  modelo-teórica(o)
> >
> > 9) "negation-free" (adjetivo):  livre de  negações
> >
> > 10) " proof"  (substantivo) :   preferencialmente  'demonstração', mas
> >   mantendo   "Teoria da Prova"  no caso  específico da área.
> >
> >
> > - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
> > - - - - - - - - - - - - - - - - - - - - - - - - - - - -
> > Acho que a questão é importante: há  pouco tempo  o Chateaubriand me
> > escreveu  perguntando   como eu usaria
> >  "dialetheic"  para não confundir com "dialético".
> >
> > *Não quero*  dizer  com isso  que uma discussão mais  profunda, como
> > aquela sobre  "consequência sintática"e "semântica, ou sobre a
> > distinção ( se  houver) entre "prova" e "demonstração"  devam ser
> > canceladas--simplesmente  não creio que esse tipo  de discussão se
> > resolve  na  Lista.
> > Talvez se  inicie na Lista, mas  só vai prosperar   (penso) com um
> > artigo competente e bem feito endereçando-se à questão.
> >
> > Há  muito mais. Ficam como desafio "turnstile", "top" e  "bottom"...
> >
> > Abs,
> >
> > Walter
> >
> > Em 11 de novembro de 2011 15:09, Anderson de Araújo
> >  escreveu:
> > > Rodrigo, concordo com você em ambos os pontos.
> > >
> > > É duro de engolir a expressão `computacionalmente saturado', mas,
> > > infelizmente, não tenho argumentos melhores do que aqueles apresentados
> > > pelo Soare e outros. Então, quando tenho em vista a versão informal,
> uso
> > > `efetivamente saturado' mas, quando está em questão uma versão formal
> > > qualquer, uso, a contragosto, `computacionalmente saturado'.
> > >
> > > Quanto à notação em lógica, realmente a situação é problemática;
> > sobretudo
> > > em teoria dos modelos e teoria da computabilidade. Em particular, o
> > exemplo
> > > que você apontou sobre a substituição de termos é emblemático. Algum
> > tempo
> > > atrás, li alguns artigos de pesquisadores renomados em teoria dos
> modelos
> > > sobre quantificadores ramificados e fiquei incomodado com o descuido -
> e
> > > justo nesse tema no qual qualquer deslize compromete muito a
> compreensão
> > > dos resultados.
> > >
> > > Talvez fosse o caso de abrir uma linha de discussão sobre a notação em
> > > lógica aqui na lista. Quem sabe a coisa avança e no próximo EBL
> tenhamos
> > > uma espécie de `Convensão Notacional da SBL', construída via debate. Se
> > > essa iniciativa for endossada pelos membros mais experientes da lista,
> > ela
> > > ganhará força.
> > >
> > > A unidade, assim como a discórdia, em ciência é um fator positivo.
> Também
> > > acredito que passaria uma boa imagem para os lógicos de `outros mares'
> > > saber que no Brasil há algo do tipo `Convensão Notacional da SBL'.
> > >
> > > Abraços,
> > >
> > > Anderson
> > >
> > >
> > >
> > > Em 11 de novembro de 2011 09:31, Rodrigo Freire  > >escreveu:
> > >
> > >> Claro Anderson, entendo o que você escreveu. Apenas apontei que as
> vezes
> > >> simplesmente não soa bem substituir "recursivamente" por
> > "computavelmente".
> > >> Efetivamente saturado ficou bom.
> > >>
> > >> Outro ponto sobre a linguagem usada em lógica: notações. Acho que
> > notação
> > >> é um ponto crítico em lógica.
> > >>
> > >> Acho que ainda não há um padrão de notação em lógica que seja
> > >> satisfatório. Por exemplo o símbolo usado para a relação de
> consequncia
> > >> semântica, uma barrinha vertical seguida 

Re: [Logica-l] Lançamento do livro "The Functional Interpretation of Logical Deduction" (World Scientific)

[Décio Krause]

Parabéns Ruy e demais autores. Certamente mais um excelente trabalho.
Abraço 
Décio

--
Décio Krause
Departamento de Filosofia
Universidade Federal de Santa Catarina
88040-900 Florianópolis - SC - Brasil
http://www.cfh.ufsc.br/~dkrause
--


Em 11/11/2011, às 21:18, Ruy de Queiroz  escreveu:

> Caros(as),
> 
> Estão todos convidados a comparecer ao lançamento do nosso livro (em
> parceria com Anjolina e Dov Gabbay):
> 
> The Functional Interpretation of Logical
> Deduction(World
> Scientific, Oct 2011):
> 
> 
> Onde: *SBS Livraria Internacional* (Av. Conselheiro Rosa e Silva 1519,
> Recife, em frente à ABA-Aflitos)
> Quando: 6a. Feira, 02/12/11, às 19hs.
> 
> *Todos são bem-vindos!*
> 
> RSVP para r...@cin.ufpe.br
> 
> Ruy
> ___
> 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

Re: [Logica-l] "provas" x "demonstrações", em Lógica

[Joao Marcos]

PessoALL:

Que bela se revelou esta discussão, afinal!  Mais uma vez a lista
mostrou que pode ser arena para discordâncias, concordâncias, e muito
debate racional e inteligente.  Os colegas apresentaram argumentos tão
superiores aos argumentos iniciais que ousei propor que ao fim fico
até tentado a concluir que Descartes estava afinal errado, e o bom
senso NÃO é a coisa mais bem distribuída deste mundo. :-)

Felicíssimos me pareceram ter sido, em particular, Anderson com o seu
PS esclarecedor e Daniel com sua inteligente Digressão Lúdica.
Anderson lembrou muito bem lembrado do imenso esforço recente que
custou à área de Computabilidade decidir-se pela maior adequação
conceitual da terminologia "computavelmente enumerável" onde antes,
por décadas, dominaram os termos "recursivamente enumerável",
"semidecidível" ou "Turing-reconhecível".  O custo de mudarmos os
nossos hábitos lusófonos (orais, antes de mais nada) no que diz
respeito à boa tradução de "Beweis" será claramente muito menor.
Daniel mostrou ainda que "Teoria das Evidências" poderia se constituir
em uma tradução até mais adequada ao que a "Proof Theory" _deveria ter
sido_, para além do mero estudo da noção lógico-matemática de
*demonstração*.  Deu-me até vontade de propor a revisão da
terminologia em todas as outras línguas, para manter a nossa
terminologia atual. :-)  Mas vou ficar mesmo com "Teoria das
Demonstrações", que até agora me pareceu superior em termos de
adequação conceitual e etimológica --- deixando claro que, como
disseram os colegas, assim como a matemática não pode ser um
substituto para a filosofia (Kripke), a escolha de uma *terminologia
sã* não pode ser um bom substituto para o verdadeiro *esclarecimento
conceitual* por ela pressuposto.

Curiosamente, outro tema que foi recentemente citado nesta discussão e
em outra que tivemos antes trouxe justamente à baila um termo que
também tem estado atualmente em processo de transformação, na
literatura, a saber: aquele que outrora foi amplamente conhecido como
"Isomorfismo de Curry-Howard" e que hoje cada vez mais é conhecido
como "Correspondência de Curry-Howard", para evitar uma possível
imprecisão paradoxalmente ligada ao significado matemático preciso do
termo "isomorfismo".  Por motivos semelhantes, também houve esforços
(menos bem-sucedidos) para rebatizar a famosa "Tese de Church-Turing"
como "Conjectura de Church-Turing".  Por outro lado, quase ninguém
chamaria o "Último Teorema de Fermat" de "Última Conjectura de
Fermat", embora pareça claro que uma _demonstração_ do teorema não
havia realmente sido produzida pelo jurista que lhe deu o nome.  (E na
informática ninguém cogitou, obviamente, substituir o termo anedótico
"Lei de Moore" por algo mais _adequado_.)  Todas estas histórias
testemunham vivamente o quanto as linguagens técnicas evoluem, em
concurso com as linguagens naturais, e mostram como esta evolução pode
ser parcialmente dirigida pelos usuários/utentes destas mesmas
linguagens.

Finalmente, no que diz respeito à proposta recente de criação de uma
*Convenção Notacional da SBL*, ou de um *banco de terminologia* que
"nos ajudasse a escrever melhor", confesso-me um pouco descrente da
iniciativa --- e até temeroso.  O bonito deste tipo de discussão que
estamos tendo agora está justamente na _possibilidade_ que temos de
propor a emenda, por exemplo, de termos técnicos que se revelem a
médio prazo conceitualmente (ou etimologicamente) equivocados, tais
como "consequência sintática" ou "teoria da prova".  Ao decidirmos
contudo por uma convenção particular "universalmente partilhada em
nosso território", em detrimento de outras que possam ser _igualmente
adequadas_, engessamos outra vez a língua, e passamos a correr o risco
de falar de "erros" que, com mais tolerância, enxergaríamos justamente
como propostas de _revisão da norma_.  Será que precisamos de mais
academias ditando regras?  Parece-me mais saudável, ao contrário,
conviver com a diversidade, desde que bem justificada!

% % %

Termino com uma anedota.  Quando eu vivia em Viena, surpreendeu-me o
comentário de um colega que afirmou que eu havia usado, em uma
apresentação, uma "convenção terminológica totalmente divergente do
padrão da literatura".  O motivo da minha surpresa estava justamente
no fato de que eu havia usado a exata terminologia que encontrei na
literatura que eu li durante toda a minha formação, no Brasil, ou que
em alguns casos ajudei a desenvolver cuidadosamente, terminologia esta
que eu havia encontrado também em muitos artigos escritos por colegas
de várias partes do mundo.  Notei contudo que estes colegas de outras
partes do mundo muitas vezes não deixavam de ser, por assim dizer,
"simpáticos à literatura produzida no Brasil".  E compreendi por fim
que o que os colegas vienenses chamava de "padrão na literatura"
consistia simplesmente no padrão da _literatura escrita por eles_
(aliás, por um grupo pequeno deles, já que eles não hesitaram também a
me apontar um dentre eles que, detestavelmente, insis

Re: [Logica-l] Lançamento do livro "The Functional Interpretation of Logical Deduction" (World Scientific)

[ana]

Parabéns, Ruy e Anjolina, pelo livro e pelo trabalho realizado!

Bjs e abraços,
Ana


> Caro Ruy:
>
> meus  sinceros parabéns à Angiolina, a você e ao Dov. Infelizmente,
> esta  mensagem não vale como "RSVP"
> porque Recife  está um tanto  longe... :-)
> Mas  o Dov Gabbay tem tido  tantas  parcerias  por aqui que  já merece
>  ser  considerado "um  lógioc  brasileiro", assim como
> os australianos consideram o David Lewis  "an Australasian  logician"!
>
> Abraços,
>
> Walter
>
>
>>> > Estão todos convidados a comparecer ao lançamento do nosso livro
>>> (em
>>> > parceria com Anjolina e Dov Gabbay):
>>> >
>>> > The Functional Interpretation of Logical
>>> > Deduction(World
>>> > Scientific, Oct 2011):
>>> >
>>> >
>>> > Onde: *SBS Livraria Internacional* (Av. Conselheiro Rosa e Silva
>>> 1519,
>>> > Recife, em frente à ABA-Aflitos)
>>> > Quando: 6a. Feira, 02/12/11, às 19hs.
>>> >
>>> > *Todos são bem-vindos!*
>>> >
>>> > RSVP para r...@cin.ufpe.br
>>> >
>>> > Ruy
>>> > ___
>>> > Logica-l mailing list
>>> > Logica-l@dimap.ufrn.br
>>> > http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
>
> ---
> Prof. Dr. Walter Carnielli
> Director
> Centre for Logic, Epistemology and the History of Science – CLE
> State University of Campinas –UNICAMP
> 13083-859 Campinas -SP, Brazil
> Phone: (+55) (19) 3521-6517
> Fax: (+55) (19) 3289-3269
> Institutional e-mail: walter.carnie...@cle.unicamp.br
> Website: http://www.cle.unicamp.br/prof/carnielli
> ___
> 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

[Logica-l] breves observações terminológicas

[Joao Marcos]

Rodrigo Freire escreveu:
>
> Outro ponto sobre a linguagem usada em lógica: notações.
> Acho que notação é um ponto crítico em lógica.

Tendo esclarecido que não me parece possível, e nem muito menos
necessário, termos uma notação _universalmente partilhada_, ofereço
aqui apenas algumas sugestões para questões levantadas pelos colegas.

(Insisto: não pretendo fazer propostas com caráter normativo, por isso
ninguém precisa se revoltar e dizer que vai adotar uma convenção
inteiramente contrária ao que eu proponho a seguir simplesmente porque
não gosta de mim ou da forma como eu me expresso, quando defendo
animadamente aquilo em que acredito.)

> Outra coisa: notação para substituição de termos: por exemplo, é comum
> encontrarmos a notação A(a_1,...,a_n) para expressar a substituição
> simultanea de variáveis x_1,..., x_n por a_1,...,a_n na fórmula A. É comum
> também encontrar outras notações para a mesma coisa que explicitam as
> variáveis x_1,..,x_n. Como há outras operações que podem ser realizadas nas
> fórmulas, as vezes a notação não deixa claro qual é a ordem das operações.

Talvez não haja uma forma de ser absolutamente claro com relação ao
caráter _simultâneo_ da noção de *substituição* sem usar uma notação
bidimensional, que podemos adotar ao escrever por exemplo o mapa de
substituição como uma matriz-coluna.  Não terá sido, contudo, um dos
pontos menos antipáticos da escrita-conceitual de Frege justamente o
seu caráter bidimensional...

Mais grave me parece o problema anterior de usarmos a notação E[t/x],
usando a convenção anglófona, para expressar a substituição da
variável x pelo termo t na expressão E.  Neste caso a leitura em Bom
Inglês é "substitute t for x in E".  No entanto, uma alternativa de
leitura mais próxima do uso natural das preposições em português, e em
muitas outras línguas naturais, seria "substitute x by t in E", ou
seja, "substituir x por t em E" ou "a expressão E, com x substituído
por t".  Notem que esta história toda fica particularmente confusa
quando o termo t é ele próprio uma variável y: qual a leitura de
E[y/x], "substitute y for x" ou "substitute y by x" --- são duas
substituições completamente diferentes!  Para evitar este tipo de
confusão e imprimir um caráter de direcionalidade à substituição,
tenho preferido escrever E[x \mapsto t], que revela justamente x como
parte do domínio da função de substituição e t como parte de seu
contra-domínio, e ainda mostra a substituição como um tipo de manobra
_sintática_ que fazemos em uma linguagem de programação (ou na teoria
da reescrita).  Mas não julgo que esta convenção E[x \mapsto t] seja
"melhor" do que outras; ela é apenas vantajosa em não permitir que eu
erre ao me confundir com o significado de "substitute t for x", em
inglês.

% % %

Ainda sobre "notações bidimensionais", parece-me que em muitos casos
não dá para evitá-las, ou sequer é vantajoso fazê-lo.  Em outras
ocasiões, contudo, podemos perfeitamente separar "aspectos práticos"
de "aspectos implementacionais".  Por exemplo, ao pensar numa
gramática regular, ou numa linguagem formal, ou numa álgebra abstrata,
podemos obviamente pensar e escrever seus termos como strings.  Mas
certamente facilitará o parsing destes termos, bem como a definição de
funções recursivas e o estabelecimento de demonstrações indutivas
sobre eles, se os _implementarmos_ como árvores, ou outra estrutura de
dados mais adequada!

Um ilustração.  Muitos dos colegas devem se encontrar, como eu, em uma
certa lista de mensagens em que não pediu para entrar, e terão
recebido uma mensagem recente do Corcoran sobre uma certa "string
theory" que ele continua a desenvolver há anos.  Se temos razão
contudo em pensar que as strings são apenas um _disfarce sintático_
para uma estrutura de dados mais profunda cujo proveito podemos tirar,
é difícil perceber se haveria algum real interesse lógico no estudo de
fórmulas-como-strings.  Como lógicos praticamente nunca fazemos, por
exemplo, indução sobre strings.  Algumas vezes até fazemos
demonstrações por indução sobre números naturais (que "traduzem" as
estruturas envolvidas).  Mas a "verdade" sobre a maior parte das
induções que nos interessam é que eles são *estruturais*!  Ignorar a
estrutura é esconder parte da verdade...

Demorei a compreender a importância e o alcance do conceito de
"estrutura de dado" justamente por ter feito parte da minha formação
inicial na Filosofia.

% % %

Walter Carnielli escreveu:
>
> 1) "Forcing" (substantivo) :  Relação de forçamento

E a *técnica de forcing*, de Cohen?

> 2) "Frame" (substantivo) :  enquadramento

Este já está "consagrado", não?

> 3) "tableau"  e "tableaux"  (substantivos):   tablô e  tablôs

Esta é engraçada, pois o termo *tableau(x)* foi justamente um
galicismo proposto e "consagrado" por um holandês (Beth) e um
estadunidense (Smullyan)...

> 10) " proof"  (substantivo) :   preferencialmente  'demonstração',
> mas mantendo   "Teoria da Prova"  no caso  específico da área.

Vou manter não... :-)

> *Não q

Re: [Logica-l] Um "Banco de Teminologia"

[Joao Marcos]

Esqueci-me desta:

> 12) proof-theoretic: prova-teorética(o)?

"Demonstracional"?

JM

-- 
http://sequiturquodlibet.googlepages.com/
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l

Re: [Logica-l] breves observações terminológicas

[Rodrigo Freire]

Olá João.


Mais grave me parece o problema anterior de usarmos a notação E[t/x],
> usando a convenção anglófona, para expressar a substituição da
> variável x pelo termo t na expressão E.  Neste caso a leitura em Bom
> Inglês é "substitute t for x in E".  No entanto, uma alternativa de
> leitura mais próxima do uso natural das preposições em português, e em
> muitas outras línguas naturais, seria "substitute x by t in E", ou
> seja, "substituir x por t em E" ou "a expressão E, com x substituído
> por t".  Notem que esta história toda fica particularmente confusa
> quando o termo t é ele próprio uma variável y: qual a leitura de
> E[y/x], "substitute y for x" ou "substitute y by x" --- são duas
> substituições completamente diferentes!  Para evitar este tipo de
> confusão e imprimir um caráter de direcionalidade à substituição,
> tenho preferido escrever E[x \mapsto t], que revela justamente x como
> parte do domínio da função de substituição e t como parte de seu
> contra-domínio, e ainda mostra a substituição como um tipo de manobra
> _sintática_ que fazemos em uma linguagem de programação (ou na teoria
> da reescrita).  Mas não julgo que esta convenção E[x \mapsto t] seja
> "melhor" do que outras; ela é apenas vantajosa em não permitir que eu
> erre ao me confundir com o significado de "substitute t for x", em
> inglês.
>


Boa observação.

Vou explicar um pouco o que eu acho mais confuso com relação a substituição.

Suponha que vamos fazer a substituição em uma expressão E. Depois da
substituição, obtemos a expressão E[t/x].
Em muitas situações em que estamos lidando com uma fórmula específica, não
escrevemos E e depois E[t/x], mas apenas a expressão obtida.
Por exemplo, a expressão inicial pode ser E: P(x,y) & F(x)=z. E[t/x} é
P(t,y) & F(t)=z.

O problema é que, apenas escrever a expressão final não indica qual o E
inicial nem qual foi a substituição: ela pode, em geral, ser obtida de
diferentes expressões por substituição. No exemplo acima, se temos diante
de nossos olhos apenas P(t,y) & F(t)=z, não temos indicação do que foi
feito e como essa expressão foi obtida. Por exemplo, pode ter sido obtida
de P(x,y) & w=z pela substituição de x por t e w por F(t), entre
(infinitas) outras possibilidades.


Se estamos em um contexto em que duas operações são realizadas na expressão
(muito comum em lógica) e vemos na nossa frente apenas a expressão final
(também é muito comum em textos de lógica encontrar passagens puladas)
ficamos perdidos facilmente. Com a expressão final em nossa frente não é
claro quais foram as operações realizadas nem a ordem em que as operações
foram realizadas.


Para eliminar isso, só com uma notação que indique a expressão inicial e as
operações em uma ordem. Em matemática há uma notação standard para
composição de funções, mas para muitas dessas operações a notação standard
não é funcional.

Isso também tem o custo de tornar a notação mais carregada, o que também
não é muito desejável...

Abraço
Rodrigo
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l

Re: [Logica-l] breves observações terminológicas

[Joao Marcos]

A linha de investigação que me parece mais próxima de resolver este
problema específico é a dos *cálculos com substituição explícita*, que
aparecem em alguns ramos de estudo da teoria da reescrita e do cálculo
lambda.
http://en.wikipedia.org/wiki/Explicit_substitution

Bastarão?
JM


2011/11/12 Rodrigo Freire :
> Olá João.
>
>
>> Mais grave me parece o problema anterior de usarmos a notação E[t/x],
>> usando a convenção anglófona, para expressar a substituição da
>> variável x pelo termo t na expressão E.  Neste caso a leitura em Bom
>> Inglês é "substitute t for x in E".  No entanto, uma alternativa de
>> leitura mais próxima do uso natural das preposições em português, e em
>> muitas outras línguas naturais, seria "substitute x by t in E", ou
>> seja, "substituir x por t em E" ou "a expressão E, com x substituído
>> por t".  Notem que esta história toda fica particularmente confusa
>> quando o termo t é ele próprio uma variável y: qual a leitura de
>> E[y/x], "substitute y for x" ou "substitute y by x" --- são duas
>> substituições completamente diferentes!  Para evitar este tipo de
>> confusão e imprimir um caráter de direcionalidade à substituição,
>> tenho preferido escrever E[x \mapsto t], que revela justamente x como
>> parte do domínio da função de substituição e t como parte de seu
>> contra-domínio, e ainda mostra a substituição como um tipo de manobra
>> _sintática_ que fazemos em uma linguagem de programação (ou na teoria
>> da reescrita).  Mas não julgo que esta convenção E[x \mapsto t] seja
>> "melhor" do que outras; ela é apenas vantajosa em não permitir que eu
>> erre ao me confundir com o significado de "substitute t for x", em
>> inglês.
>
>
> Boa observação.
>
> Vou explicar um pouco o que eu acho mais confuso com relação a substituição.
>
> Suponha que vamos fazer a substituição em uma expressão E. Depois da
> substituição, obtemos a expressão E[t/x].
> Em muitas situações em que estamos lidando com uma fórmula específica, não
> escrevemos E e depois E[t/x], mas apenas a expressão obtida.
> Por exemplo, a expressão inicial pode ser E: P(x,y) & F(x)=z. E[t/x} é
> P(t,y) & F(t)=z.
>
> O problema é que, apenas escrever a expressão final não indica qual o E
> inicial nem qual foi a substituição: ela pode, em geral, ser obtida de
> diferentes expressões por substituição. No exemplo acima, se temos diante de
> nossos olhos apenas P(t,y) & F(t)=z, não temos indicação do que foi feito e
> como essa expressão foi obtida. Por exemplo, pode ter sido obtida de P(x,y)
> & w=z pela substituição de x por t e w por F(t), entre (infinitas) outras
> possibilidades.
>
>
> Se estamos em um contexto em que duas operações são realizadas na expressão
> (muito comum em lógica) e vemos na nossa frente apenas a expressão final
> (também é muito comum em textos de lógica encontrar passagens puladas)
> ficamos perdidos facilmente. Com a expressão final em nossa frente não é
> claro quais foram as operações realizadas nem a ordem em que as operações
> foram realizadas.
>
>
> Para eliminar isso, só com uma notação que indique a expressão inicial e as
> operações em uma ordem. Em matemática há uma notação standard para
> composição de funções, mas para muitas dessas operações a notação standard
> não é funcional.
>
> Isso também tem o custo de tornar a notação mais carregada, o que também não
> é muito desejável...
>
> Abraço
> Rodrigo
>
>
>



-- 
http://sequiturquodlibet.googlepages.com/
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l

Re: [Logica-l] breves observações terminológicas

[Rodrigo Freire]

Entendo que no contexto de programação essa ambiguidade é inadmissível e
isso resolve sim, você está certo. Mas eu gostaria de algo mais humano,
para apresentar nos textos básicos sem transformá-los em sopa de letrinhas.

Abraço
Rodrigo





2011/11/12 Joao Marcos 

> A linha de investigação que me parece mais próxima de resolver este
> problema específico é a dos *cálculos com substituição explícita*, que
> aparecem em alguns ramos de estudo da teoria da reescrita e do cálculo
> lambda.
> http://en.wikipedia.org/wiki/Explicit_substitution
>
> Bastarão?
> JM
>
>
> 2011/11/12 Rodrigo Freire :
> > Olá João.
> >
> >
> >> Mais grave me parece o problema anterior de usarmos a notação E[t/x],
> >> usando a convenção anglófona, para expressar a substituição da
> >> variável x pelo termo t na expressão E.  Neste caso a leitura em Bom
> >> Inglês é "substitute t for x in E".  No entanto, uma alternativa de
> >> leitura mais próxima do uso natural das preposições em português, e em
> >> muitas outras línguas naturais, seria "substitute x by t in E", ou
> >> seja, "substituir x por t em E" ou "a expressão E, com x substituído
> >> por t".  Notem que esta história toda fica particularmente confusa
> >> quando o termo t é ele próprio uma variável y: qual a leitura de
> >> E[y/x], "substitute y for x" ou "substitute y by x" --- são duas
> >> substituições completamente diferentes!  Para evitar este tipo de
> >> confusão e imprimir um caráter de direcionalidade à substituição,
> >> tenho preferido escrever E[x \mapsto t], que revela justamente x como
> >> parte do domínio da função de substituição e t como parte de seu
> >> contra-domínio, e ainda mostra a substituição como um tipo de manobra
> >> _sintática_ que fazemos em uma linguagem de programação (ou na teoria
> >> da reescrita).  Mas não julgo que esta convenção E[x \mapsto t] seja
> >> "melhor" do que outras; ela é apenas vantajosa em não permitir que eu
> >> erre ao me confundir com o significado de "substitute t for x", em
> >> inglês.
> >
> >
> > Boa observação.
> >
> > Vou explicar um pouco o que eu acho mais confuso com relação a
> substituição.
> >
> > Suponha que vamos fazer a substituição em uma expressão E. Depois da
> > substituição, obtemos a expressão E[t/x].
> > Em muitas situações em que estamos lidando com uma fórmula específica,
> não
> > escrevemos E e depois E[t/x], mas apenas a expressão obtida.
> > Por exemplo, a expressão inicial pode ser E: P(x,y) & F(x)=z. E[t/x} é
> > P(t,y) & F(t)=z.
> >
> > O problema é que, apenas escrever a expressão final não indica qual o E
> > inicial nem qual foi a substituição: ela pode, em geral, ser obtida de
> > diferentes expressões por substituição. No exemplo acima, se temos
> diante de
> > nossos olhos apenas P(t,y) & F(t)=z, não temos indicação do que foi
> feito e
> > como essa expressão foi obtida. Por exemplo, pode ter sido obtida de
> P(x,y)
> > & w=z pela substituição de x por t e w por F(t), entre (infinitas) outras
> > possibilidades.
> >
> >
> > Se estamos em um contexto em que duas operações são realizadas na
> expressão
> > (muito comum em lógica) e vemos na nossa frente apenas a expressão final
> > (também é muito comum em textos de lógica encontrar passagens puladas)
> > ficamos perdidos facilmente. Com a expressão final em nossa frente não é
> > claro quais foram as operações realizadas nem a ordem em que as operações
> > foram realizadas.
> >
> >
> > Para eliminar isso, só com uma notação que indique a expressão inicial e
> as
> > operações em uma ordem. Em matemática há uma notação standard para
> > composição de funções, mas para muitas dessas operações a notação
> standard
> > não é funcional.
> >
> > Isso também tem o custo de tornar a notação mais carregada, o que também
> não
> > é muito desejável...
> >
> > Abraço
> > Rodrigo
> >
> >
> >
>
>
>
> --
> http://sequiturquodlibet.googlepages.com/
>
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l

Re: [Logica-l] Um "Banco de Teminologia"

[Elaine Pimentel]

On Nov 12, 2011, at 4:46 PM, Joao Marcos wrote:

> Esqueci-me desta:
> 
>> 12) proof-theoretic: prova-teorética(o)?
> 
> "Demonstracional"?
> 

Credo…

Elaine.

___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l

[Logica-l] Reportagem: Cérebros para o Brasil

[psdias2]

A quem possa interessar:

A TV Senado tem um programa chamado "Repórter Senado", de boa qualidade,
que costuma abordar temas bem interessantes.

Uma das reportagens é o "Cérebros para o Brasil", que mostra os trabalhos
de pesquisadores (Miguel Nicolelis, Sidarta Ribeiro, etc.) e institutos do
Rio Grande do Norte, da área de Neurociências.

Para assistir online:

a) Entrar no site abaixo:
http://www.senado.gov.br/TV/

b) Na parte superior da página, e à direita, há um campo chamado "Pesquisa".
Digitar a palavra "cérebros" (sem aspas) e clicar em "Buscar"

c) Aparecerão 3 programas.  Os que mencionei acima são os dos dias
06/10/2011 (um resumo sobre o programa "Cérebros para o Brasil",
e 19/10/2011 (o programa propriamente dito, em 3 partes)

d) Para assistir o programa do dia 06/10/2011 clicar no texto logo abaixo
do título.  O vídeo será apresentado no alto da tela.  Para ver o 
programa do dia
19/10/2011, clicar onde está escrito em "Parte 1", "Parte 2" e "Parte 3" 
e aguardar

o vídeo aparecer (sempre no alto da tela)

e) É possível baixar os vídeos, em formato .FLV, para assistir off-line.
Há um botão escrito "Baixar", logo abaixo da janela do vídeo.

Obs.: Por algum problema do site, às vezes os programas aparecem 
repetidos, na listagem
que resulta do processo de busca (por exemplo, o programa de 06/10/2011 
aparece duas

vezes, mas trata-se do mesmo vídeo).

Atenciosamente
Paulo

___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l

Re: [Logica-l] breves observações terminológicas

[Eduardo Ochs]

...pra substituição eu uso uma convenção que não é comum, mas que acho
que é bem clara: E[x:=t], e quando preciso de substituição simultânea
eu em geral ponho os ":=" empilhados, cada um numa linha. O código em
LaTeX é:

  \def\sm#1{\begin{smallmatrix}#1\end{smallmatrix}}
  \def\subst#1{\left[\sm{#1}\right]}

  Exemplo: $A\subst{ x := t \\ y := u}$

Em algumas situações é conveniente pôr o bloquinho de substituição
antes da expressão, e aí dá pra usar algo como:

  Exemplo: $\subst{ t =: x \\ u =: y } A$

invertendo a ordem de tudo pra manter as variáveis mais perto da
expressão que os termos, e usando "=:" ao invés de ":=". Se você
preferir inverter a direção do \mapsto o truque é este - que não é
totalmente óbvio:

  \def\mapsot{\leftarrow\mapsfromchar}

Abraços,
  Eduardo Ochs
  eduardoo...@gmail.com
  http://angg.twu.net/


2011/11/12 Rodrigo Freire 

> Entendo que no contexto de programação essa ambiguidade é inadmissível e
> isso resolve sim, você está certo. Mas eu gostaria de algo mais humano,
> para apresentar nos textos básicos sem transformá-los em sopa de letrinhas.
>
> Abraço
> Rodrigo
>
>
>
>
>
> 2011/11/12 Joao Marcos 
>
> > A linha de investigação que me parece mais próxima de resolver este
> > problema específico é a dos *cálculos com substituição explícita*, que
> > aparecem em alguns ramos de estudo da teoria da reescrita e do cálculo
> > lambda.
> > http://en.wikipedia.org/wiki/Explicit_substitution
> >
> > Bastarão?
> > JM
> >
> >
> > 2011/11/12 Rodrigo Freire :
> > > Olá João.
> > >
> > >
> > >> Mais grave me parece o problema anterior de usarmos a notação E[t/x],
> > >> usando a convenção anglófona, para expressar a substituição da
> > >> variável x pelo termo t na expressão E.  Neste caso a leitura em Bom
> > >> Inglês é "substitute t for x in E".  No entanto, uma alternativa de
> > >> leitura mais próxima do uso natural das preposições em português, e em
> > >> muitas outras línguas naturais, seria "substitute x by t in E", ou
> > >> seja, "substituir x por t em E" ou "a expressão E, com x substituído
> > >> por t".  Notem que esta história toda fica particularmente confusa
> > >> quando o termo t é ele próprio uma variável y: qual a leitura de
> > >> E[y/x], "substitute y for x" ou "substitute y by x" --- são duas
> > >> substituições completamente diferentes!  Para evitar este tipo de
> > >> confusão e imprimir um caráter de direcionalidade à substituição,
> > >> tenho preferido escrever E[x \mapsto t], que revela justamente x como
> > >> parte do domínio da função de substituição e t como parte de seu
> > >> contra-domínio, e ainda mostra a substituição como um tipo de manobra
> > >> _sintática_ que fazemos em uma linguagem de programação (ou na teoria
> > >> da reescrita).  Mas não julgo que esta convenção E[x \mapsto t] seja
> > >> "melhor" do que outras; ela é apenas vantajosa em não permitir que eu
> > >> erre ao me confundir com o significado de "substitute t for x", em
> > >> inglês.
> > >
> > >
> > > Boa observação.
> > >
> > > Vou explicar um pouco o que eu acho mais confuso com relação a
> > substituição.
> > >
> > > Suponha que vamos fazer a substituição em uma expressão E. Depois da
> > > substituição, obtemos a expressão E[t/x].
> > > Em muitas situações em que estamos lidando com uma fórmula específica,
> > não
> > > escrevemos E e depois E[t/x], mas apenas a expressão obtida.
> > > Por exemplo, a expressão inicial pode ser E: P(x,y) & F(x)=z. E[t/x} é
> > > P(t,y) & F(t)=z.
> > >
> > > O problema é que, apenas escrever a expressão final não indica qual o E
> > > inicial nem qual foi a substituição: ela pode, em geral, ser obtida de
> > > diferentes expressões por substituição. No exemplo acima, se temos
> > diante de
> > > nossos olhos apenas P(t,y) & F(t)=z, não temos indicação do que foi
> > feito e
> > > como essa expressão foi obtida. Por exemplo, pode ter sido obtida de
> > P(x,y)
> > > & w=z pela substituição de x por t e w por F(t), entre (infinitas)
> outras
> > > possibilidades.
> > >
> > >
> > > Se estamos em um contexto em que duas operações são realizadas na
> > expressão
> > > (muito comum em lógica) e vemos na nossa frente apenas a expressão
> final
> > > (também é muito comum em textos de lógica encontrar passagens puladas)
> > > ficamos perdidos facilmente. Com a expressão final em nossa frente não
> é
> > > claro quais foram as operações realizadas nem a ordem em que as
> operações
> > > foram realizadas.
> > >
> > >
> > > Para eliminar isso, só com uma notação que indique a expressão inicial
> e
> > as
> > > operações em uma ordem. Em matemática há uma notação standard para
> > > composição de funções, mas para muitas dessas operações a notação
> > standard
> > > não é funcional.
> > >
> > > Isso também tem o custo de tornar a notação mais carregada, o que
> também
> > não
> > > é muito desejável...
> > >
> > > Abraço
> > > Rodrigo
> > >
> > >
> > >
> >
> >
> >
> > --
> > http://sequiturquodlibet.googlepages.com/
> >
> 

Re: [Logica-l] breves observações terminológicas

[Rodrigo Freire]

Obrigado Eduardo.

2011/11/12 Eduardo Ochs 

> ...pra substituição eu uso uma convenção que não é comum, mas que acho
> que é bem clara: E[x:=t], e quando preciso de substituição simultânea
> eu em geral ponho os ":=" empilhados, cada um numa linha. O código em
> LaTeX é:
>
>   \def\sm#1{\begin{smallmatrix}#1\end{smallmatrix}}
>   \def\subst#1{\left[\sm{#1}\right]}
>
>   Exemplo: $A\subst{ x := t \\ y := u}$
>
> Em algumas situações é conveniente pôr o bloquinho de substituição
> antes da expressão, e aí dá pra usar algo como:
>
>   Exemplo: $\subst{ t =: x \\ u =: y } A$
>
> invertendo a ordem de tudo pra manter as variáveis mais perto da
> expressão que os termos, e usando "=:" ao invés de ":=". Se você
> preferir inverter a direção do \mapsto o truque é este - que não é
> totalmente óbvio:
>
>   \def\mapsot{\leftarrow\mapsfromchar}
>
> Abraços,
>   Eduardo Ochs
>   eduardoo...@gmail.com
>   http://angg.twu.net/
>
>
> 2011/11/12 Rodrigo Freire 
>
>> Entendo que no contexto de programação essa ambiguidade é inadmissível e
>> isso resolve sim, você está certo. Mas eu gostaria de algo mais humano,
>> para apresentar nos textos básicos sem transformá-los em sopa de
>> letrinhas.
>>
>> Abraço
>> Rodrigo
>>
>>
>>
>>
>>
>> 2011/11/12 Joao Marcos 
>>
>> > A linha de investigação que me parece mais próxima de resolver este
>> > problema específico é a dos *cálculos com substituição explícita*, que
>> > aparecem em alguns ramos de estudo da teoria da reescrita e do cálculo
>> > lambda.
>> > http://en.wikipedia.org/wiki/Explicit_substitution
>> >
>> > Bastarão?
>> > JM
>> >
>> >
>> > 2011/11/12 Rodrigo Freire :
>> > > Olá João.
>> > >
>> > >
>> > >> Mais grave me parece o problema anterior de usarmos a notação E[t/x],
>> > >> usando a convenção anglófona, para expressar a substituição da
>> > >> variável x pelo termo t na expressão E.  Neste caso a leitura em Bom
>> > >> Inglês é "substitute t for x in E".  No entanto, uma alternativa de
>> > >> leitura mais próxima do uso natural das preposições em português, e
>> em
>> > >> muitas outras línguas naturais, seria "substitute x by t in E", ou
>> > >> seja, "substituir x por t em E" ou "a expressão E, com x substituído
>> > >> por t".  Notem que esta história toda fica particularmente confusa
>> > >> quando o termo t é ele próprio uma variável y: qual a leitura de
>> > >> E[y/x], "substitute y for x" ou "substitute y by x" --- são duas
>> > >> substituições completamente diferentes!  Para evitar este tipo de
>> > >> confusão e imprimir um caráter de direcionalidade à substituição,
>> > >> tenho preferido escrever E[x \mapsto t], que revela justamente x como
>> > >> parte do domínio da função de substituição e t como parte de seu
>> > >> contra-domínio, e ainda mostra a substituição como um tipo de manobra
>> > >> _sintática_ que fazemos em uma linguagem de programação (ou na teoria
>> > >> da reescrita).  Mas não julgo que esta convenção E[x \mapsto t] seja
>> > >> "melhor" do que outras; ela é apenas vantajosa em não permitir que eu
>> > >> erre ao me confundir com o significado de "substitute t for x", em
>> > >> inglês.
>> > >
>> > >
>> > > Boa observação.
>> > >
>> > > Vou explicar um pouco o que eu acho mais confuso com relação a
>> > substituição.
>> > >
>> > > Suponha que vamos fazer a substituição em uma expressão E. Depois da
>> > > substituição, obtemos a expressão E[t/x].
>> > > Em muitas situações em que estamos lidando com uma fórmula específica,
>> > não
>> > > escrevemos E e depois E[t/x], mas apenas a expressão obtida.
>> > > Por exemplo, a expressão inicial pode ser E: P(x,y) & F(x)=z. E[t/x} é
>> > > P(t,y) & F(t)=z.
>> > >
>> > > O problema é que, apenas escrever a expressão final não indica qual o
>> E
>> > > inicial nem qual foi a substituição: ela pode, em geral, ser obtida de
>> > > diferentes expressões por substituição. No exemplo acima, se temos
>> > diante de
>> > > nossos olhos apenas P(t,y) & F(t)=z, não temos indicação do que foi
>> > feito e
>> > > como essa expressão foi obtida. Por exemplo, pode ter sido obtida de
>> > P(x,y)
>> > > & w=z pela substituição de x por t e w por F(t), entre (infinitas)
>> outras
>> > > possibilidades.
>> > >
>> > >
>> > > Se estamos em um contexto em que duas operações são realizadas na
>> > expressão
>> > > (muito comum em lógica) e vemos na nossa frente apenas a expressão
>> final
>> > > (também é muito comum em textos de lógica encontrar passagens puladas)
>> > > ficamos perdidos facilmente. Com a expressão final em nossa frente
>> não é
>> > > claro quais foram as operações realizadas nem a ordem em que as
>> operações
>> > > foram realizadas.
>> > >
>> > >
>> > > Para eliminar isso, só com uma notação que indique a expressão
>> inicial e
>> > as
>> > > operações em uma ordem. Em matemática há uma notação standard para
>> > > composição de funções, mas para muitas dessas operações a notação
>> > standard
>> > > não é funcional.
>> > >
>> > > Isso também tem o custo de tornar a notação mais carregada,