[Logica-l] Seminário

[Mario Benevides]

Caros,

No dia 3/10 teremos um seminário aqui na UFRJ como parte das atividades do
grupo de interesse em Lógica no Rio de Janeiro,
http://www.rio-logic.org/ . Gostaria de convidar a todos, para maiores
detalhes ver: http://www.rio-logic.org/start1.html

Todos são muito benvindos.

Um abraço,

Mario

+++


Raúl Fervari
Universidade de Códoba
http://cs.famaf.unc.edu.ar/~rfervari/

Data: 3/10
Horário14:00
Local: COPPE/Sistemas na sala H-324-A, no CT da UFRJ, Cidade Universitária.


Title: Dynamic Modal Logics - Changing Structures

==
Abstract: In this talk I will present some modal languages that allows
a real dynamic perspective over relational models.
First of all, I will introduce the basic modal logic just to fix some
notation, and then I will discuss two languages  specially
designed to express dynamic properties of models: Memory Logic and Swap
Logic.

I will discuss some of the results we have already obtained for these
logic as examples of their behavior.  In particular I will show that
the model checking problem for Memory Logic is PSpace-Complete (i.e.,
as hard as model checking full first-order logic); and a
characterization of Swap Logic as a fragment of First Order Logic.
The general message is that dynamic logics as the ones we presented
are very expressive, and that while general techniques can be adapted
to treat them, sometimes a new perspective is required.






-- 
Federal University of Rio de Janeiro
www.cos.ufrj.br/~mario
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l

[Logica-l] Defesa de Dissertação de Mestrado : Antonio Marmo da Cunha Oliveira (Tony Marmo)

[Walter Carnielli]

Prezados  Colegas, prezados estudantes:

Gostaria  de convidar a  todos para assistir  à Defesa de Dissertação
de Mestrado do meu estudante
Antonio Marmo da Cunha Oliveira (Tony Marmo):


``Sistemas, Pressuposições e Implicaturas: Uma Investigação
Exploratória, Lógica e Filosófica''


Horário e  local:

Sexta-feira, 30/09/2011, às 14h00,
Sala de Defesa de Teses, IFCH- UNICAMP

com a  banca  titular composta  pelos professores:

Walter  Carnelli (CLE -IFCH, UNICAMP, orientador)
Itala D'Ottaviano (CLE- IFCH  UNICAMP)
Juliana Bueno-Soler (CCNE, UFABC Santo André)
e respectivos suplentes

Atenciosamente,

Walter Carnielli

-- 
---
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

Re: [Logica-l] trabalho do Nelson

[Valeria de Paiva]

Rodrigo,
Muito obrigada pela informacao detalhada abaixo! Aprendi muito, mas
continuo com uma duvidas basica.

Nao, eu nao quero fazer "aritmetica limitada" e  nao quero perder consistencia.

Mas quero saber se voce (e todo mundo que a gente acredita) tambem
acha que PRA realmente 'e garantidamente consistente.

obrigada,
valeria

2011/9/29 Rodrigo Freire :
> Minha dúvida sobre o trabalho do Nelson é de outra natureza: mesmo que
> todas as expectativas se confirmem e realmente a coisa esteja furada,
> o que ainda poderá ser dito da *alternativa finitista* que ele propõe
> para "consertar PRA"?  Será um sistema metamatemático cujo interesse
> poderá subsistir de modo independente a todo o resto?
>
>
>
> Parte do trabalho do Nelson já está incorporada na lógica. Ele é um dos
> precursores da aritmética limitada.
> O livro predicative arithmetic, de 1986, está disponível online na página
> dele. Contém os primeiros passos do projeto dele.
>
> De especial interesse para lógicos é a aritmetização dos teoremas da lógica
> básica em sistemas interpretaveis em Q.
> Ele segue o Shoenfield, cap. 1 a 4. Ele consegue provar uma boa parte dos
> resultados, mas não consegue alguns resultados centrais.
> Nessa parte, acho que o melhor que ele conseguiu foi demonstrar o teorema de
> extensões funcionais (com unicidade) em um sistema compatível com Q e sem
> ter que fazer a prova enfadonha que tem no Kleene (que aliás é um livro é
> pouco humano). A prova desse teorema no Shoenfield não cabe em sistemas
> aceitáveis para o Nelson.
>
> Os resultados centrais que ele não consegue: Hilbert-Ackerman, Herbrand,
> Skolem (sobre extensões funcionais em geral) e tudo o mais relacionado a
> esses. Por que não dá para obter esses resultados? Hilbert-Ackerman e
> Herbrand provam a consistência de Q. O teorema de Skolem, eu não sei. Quem
> trabalha com aritmética limitada deve saber. O segundo teorema da
> incompletude também é modificado.
>
> Como Hilbert-Ackerman tem um papel central para o Nelson, ele consegue
> versões restritas do teorema (também dá para conseguir versões restritas de
> eliminação do corte e outros). Essa história de limitar rank e level das
> constantes especiais nas provas é para isso: a teoria que ele chama de Q* só
> prova a consistência das "subteorias" tais que as provas são por
> consequência tautológica de axiomas com rank e level limitados.
>
> Com isso ele consegue um mínimo de teoria de sistemas formais para, pelo
> menos, dar sentido para "formalização". Não é grande coisa. Considero que
> perder Herbrand é muito sério: a pureza de métodos está indo embora. Mas
> acho que é possível aceitar que trabalhando nessa aritmética limitada como
> metateoria dos sistemas formais (no lugar de PRA)  faz sentido falar em
> "formalização".
>
> A partir daí você pode ter dois pontos de vista:
>
> 1) Essencialmente o ponto de vista de Hilbert trocando PRA por Q, Q* e
> outras teorias dessa aritmética do Nelson. Nesse caso, você formaliza a
> matemática em ZFC e trabalha normalmente, sempre lembrando que a metateoria
> é essa aritmética limitada. Isso vai gerar algumas preocupações só para quem
> trabalha em fundamentos. É preciso ver se forcing por exemplo é finitário
> nesse sentido. O resto da matemática fica igual. Não é possível dar provas
> de consistência, mas tudo bem, você continua praticamente como estamos hoje.
>
> 2) O ponto de vista atual do Nelson: PRA é inconsistente. Aí eu acho que não
> dá para fazer nada. Nem entendo o que significam essas afirmações dele. É
> praticamente uma contradição referencial ele dizer que exibe dois números n
> e m tal que a tetração n tetra m não existe. É aquela pergunta: o que faz o
> algoritmo que calcula essa superexponencial em termos das anteriores nesse
> caso?
>
>
> O erro desse trabalho do Nelson, que acredito já foi encontrado, está onde
> teria que estar. O erro está no plano básico do argumento, não em detalhes
> excruciantes de aritmetização (alguns desses detalhes podem ser encontrados
> já nesse livro de 1986). A aritmetização do teorema de Chaitin não fornece o
> que ele gostaria que fosse o caso. Se o erro estivesse em detalhes da
> aritmetização, o argumento dele seria usado para provar que ZFC prova que PA
> é inconsistente, já que em ZFC não há problemas de falta de recurso para
> codificação. Ou seja, se o plano dele estivesse correto, mas os detalhes
> não, ele conseguiria pelo menos uma prova da inconsistencia de ZF, o que já
> seria suficientemente interessante. E ele está gastanto centenas de páginas
> de aritmetização e está apenas no começo...
>
>
> Abraço
> Rodrigo
>
>
>
>
>
>
>
>
>
>
>
>



-- 
Valeria de Paiva
http://www.cs.bham.ac.uk/~vdp/
http://valeriadepaiva.org/www/
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l

Re: [Logica-l] trabalho do Nelson

[Francisco Antonio Doria]

Por que não acreditar na prova de consistência de Goedel para PA? Ou na de
Kunen, baseada num algoritmo?

2011/9/30 Valeria de Paiva 

> Rodrigo,
> Muito obrigada pela informacao detalhada abaixo! Aprendi muito, mas
> continuo com uma duvidas basica.
>
> Nao, eu nao quero fazer "aritmetica limitada" e  nao quero perder
> consistencia.
>
> Mas quero saber se voce (e todo mundo que a gente acredita) tambem
> acha que PRA realmente 'e garantidamente consistente.
>
> obrigada,
> valeria
>
> 2011/9/29 Rodrigo Freire :
> > Minha dúvida sobre o trabalho do Nelson é de outra natureza: mesmo que
> > todas as expectativas se confirmem e realmente a coisa esteja furada,
> > o que ainda poderá ser dito da *alternativa finitista* que ele propõe
> > para "consertar PRA"?  Será um sistema metamatemático cujo interesse
> > poderá subsistir de modo independente a todo o resto?
> >
> >
> >
> > Parte do trabalho do Nelson já está incorporada na lógica. Ele é um dos
> > precursores da aritmética limitada.
> > O livro predicative arithmetic, de 1986, está disponível online na página
> > dele. Contém os primeiros passos do projeto dele.
> >
> > De especial interesse para lógicos é a aritmetização dos teoremas da
> lógica
> > básica em sistemas interpretaveis em Q.
> > Ele segue o Shoenfield, cap. 1 a 4. Ele consegue provar uma boa parte dos
> > resultados, mas não consegue alguns resultados centrais.
> > Nessa parte, acho que o melhor que ele conseguiu foi demonstrar o teorema
> de
> > extensões funcionais (com unicidade) em um sistema compatível com Q e sem
> > ter que fazer a prova enfadonha que tem no Kleene (que aliás é um livro é
> > pouco humano). A prova desse teorema no Shoenfield não cabe em sistemas
> > aceitáveis para o Nelson.
> >
> > Os resultados centrais que ele não consegue: Hilbert-Ackerman, Herbrand,
> > Skolem (sobre extensões funcionais em geral) e tudo o mais relacionado a
> > esses. Por que não dá para obter esses resultados? Hilbert-Ackerman e
> > Herbrand provam a consistência de Q. O teorema de Skolem, eu não sei.
> Quem
> > trabalha com aritmética limitada deve saber. O segundo teorema da
> > incompletude também é modificado.
> >
> > Como Hilbert-Ackerman tem um papel central para o Nelson, ele consegue
> > versões restritas do teorema (também dá para conseguir versões restritas
> de
> > eliminação do corte e outros). Essa história de limitar rank e level das
> > constantes especiais nas provas é para isso: a teoria que ele chama de Q*
> só
> > prova a consistência das "subteorias" tais que as provas são por
> > consequência tautológica de axiomas com rank e level limitados.
> >
> > Com isso ele consegue um mínimo de teoria de sistemas formais para, pelo
> > menos, dar sentido para "formalização". Não é grande coisa. Considero que
> > perder Herbrand é muito sério: a pureza de métodos está indo embora. Mas
> > acho que é possível aceitar que trabalhando nessa aritmética limitada
> como
> > metateoria dos sistemas formais (no lugar de PRA)  faz sentido falar em
> > "formalização".
> >
> > A partir daí você pode ter dois pontos de vista:
> >
> > 1) Essencialmente o ponto de vista de Hilbert trocando PRA por Q, Q* e
> > outras teorias dessa aritmética do Nelson. Nesse caso, você formaliza a
> > matemática em ZFC e trabalha normalmente, sempre lembrando que a
> metateoria
> > é essa aritmética limitada. Isso vai gerar algumas preocupações só para
> quem
> > trabalha em fundamentos. É preciso ver se forcing por exemplo é finitário
> > nesse sentido. O resto da matemática fica igual. Não é possível dar
> provas
> > de consistência, mas tudo bem, você continua praticamente como estamos
> hoje.
> >
> > 2) O ponto de vista atual do Nelson: PRA é inconsistente. Aí eu acho que
> não
> > dá para fazer nada. Nem entendo o que significam essas afirmações dele. É
> > praticamente uma contradição referencial ele dizer que exibe dois números
> n
> > e m tal que a tetração n tetra m não existe. É aquela pergunta: o que faz
> o
> > algoritmo que calcula essa superexponencial em termos das anteriores
> nesse
> > caso?
> >
> >
> > O erro desse trabalho do Nelson, que acredito já foi encontrado, está
> onde
> > teria que estar. O erro está no plano básico do argumento, não em
> detalhes
> > excruciantes de aritmetização (alguns desses detalhes podem ser
> encontrados
> > já nesse livro de 1986). A aritmetização do teorema de Chaitin não
> fornece o
> > que ele gostaria que fosse o caso. Se o erro estivesse em detalhes da
> > aritmetização, o argumento dele seria usado para provar que ZFC prova que
> PA
> > é inconsistente, já que em ZFC não há problemas de falta de recurso para
> > codificação. Ou seja, se o plano dele estivesse correto, mas os detalhes
> > não, ele conseguiria pelo menos uma prova da inconsistencia de ZF, o que
> já
> > seria suficientemente interessante. E ele está gastanto centenas de
> páginas
> > de aritmetização e está apenas no começo...
> >
> >
> > Abraço
> > Rodrigo
> >
> >
> >
> >
> >
> >
> >
> >

Re: [Logica-l] trabalho do Nelson

[Rodrigo Freire]

Oi Valéria


Vou tentar responder da forma mais clara que eu consigo:


-Acho que perguntar sobre a consistência de PRA é sem sentido. O problema
não se coloca para PRA porque essa teoria é parte da significatividade do
problema.


-Em outras palavras, acho sem sentido questionar se alguma função primitiva
recursiva é ou não total. É como se estivéssemos questionando as condições
pelas quais o questionamento faz sentido.

-A sentença usual que expressa a consistência de PA, por exemplo, CON(PA) é
uma sentença Pi_1. Ela afirma que a máquina de Turing que procura uma prova
de 0=1 não para.


-Se não assumimos que as funções primitivas recursivas são totais, não
entendo mais o significado de CON(PA). Não parece ter mais nada a ver com a
afirmação que uma máquina de Turing para ou não. Provas de 0=1 em PA de
tamanho grande não existem? O que isso quer dizer? Como mencionei antes,
parece uma contradição referencial.

-A proposta do Nelson era exibir uma função primitiva recursiva f e um
argumento n tal que f(n) é uma prova de 0=1 em Q. Disso ele gostaria de
concluir que f(n) não existe. Não entendo o que quer dizer essa conclusão.


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] trabalho do Nelson

[Rodrigo Freire]

Mais uma pequena observação que talvez ajude a esclarecer:


O segundo teorema da incompletude, formulado apropriadamente, vale para Q:
se Q é consistente (e é) então Q não prova CON(Q), onde CON(Q) é uma
sentença da consistencia de Q. Nada surpreendente, Q é uma teoria muito
fraca, e não prova a CON(Q).

O problema é que Q é tão fraca que Q não "entende" o que é CON(Q).
Formulações diferences da sentença da consistência, que são equivalentes nas
teorias mais fortes que PRA, não são equivalentes em Q. Q não prova as
condições de derivabilidade de Hilbert Bernays, não entende direito o que é
a aritmetização da provabilidade.


Isso pode ser visto como uma formulação precisa do que eu disse acima:
teorias mais fracas que PRA não "entendem" o que significa a sentença da
consistência.

Abraço
Rodrigo







2011/9/30 Rodrigo Freire 

> Oi Valéria
>
>
> Vou tentar responder da forma mais clara que eu consigo:
>
>
> -Acho que perguntar sobre a consistência de PRA é sem sentido. O problema
> não se coloca para PRA porque essa teoria é parte da significatividade do
> problema.
>
>
> -Em outras palavras, acho sem sentido questionar se alguma função primitiva
> recursiva é ou não total. É como se estivéssemos questionando as condições
> pelas quais o questionamento faz sentido.
>
> -A sentença usual que expressa a consistência de PA, por exemplo, CON(PA) é
> uma sentença Pi_1. Ela afirma que a máquina de Turing que procura uma prova
> de 0=1 não para.
>
>
> -Se não assumimos que as funções primitivas recursivas são totais, não
> entendo mais o significado de CON(PA). Não parece ter mais nada a ver com a
> afirmação que uma máquina de Turing para ou não. Provas de 0=1 em PA de
> tamanho grande não existem? O que isso quer dizer? Como mencionei antes,
> parece uma contradição referencial.
>
> -A proposta do Nelson era exibir uma função primitiva recursiva f e um
> argumento n tal que f(n) é uma prova de 0=1 em Q. Disso ele gostaria de
> concluir que f(n) não existe. Não entendo o que quer dizer essa conclusão.
>
>
> 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] trabalho do Nelson

[Joao Marcos]

Olá, Rodrigo:

Vou ter que aprender um pouco mais sobre Aritmética Limitada, com
certeza.  Obrigado pelas lições iniciais!

Tenho uma outra dúvida.  Nem todos conhecem, mas o Putnam publicou um
artigo no NDJFL em 2000 com uma demonstração alternativa, proposta por
Kripke, do primeiro teorema de incompletude, demonstração esta que usa
bem menos Teoria da Recursão do que a versão original de Gödel.  Há
uma discussão bacana deste assunto, que você deve ter acompanhado, em:
http://mathoverflow.net/questions/72062/what-are-some-proofs-of-godels-theorem-which-are-essentially-different-from-th
Aparentemente o segundo teorema de incompletude não é um corolário
óbvio da versão kripkeana, enfraquecida, do primeiro teorema.

Você faz alguma ideia se o argumento kripkeano poderia ser formulado
com os recursos de Q?

JM

2011/9/30 Rodrigo Freire :
> Mais uma pequena observação que talvez ajude a esclarecer:
>
>
> O segundo teorema da incompletude, formulado apropriadamente, vale para Q:
> se Q é consistente (e é) então Q não prova CON(Q), onde CON(Q) é uma
> sentença da consistencia de Q. Nada surpreendente, Q é uma teoria muito
> fraca, e não prova a CON(Q).
>
> O problema é que Q é tão fraca que Q não "entende" o que é CON(Q).
> Formulações diferences da sentença da consistência, que são equivalentes nas
> teorias mais fortes que PRA, não são equivalentes em Q. Q não prova as
> condições de derivabilidade de Hilbert Bernays, não entende direito o que é
> a aritmetização da provabilidade.
>
>
> Isso pode ser visto como uma formulação precisa do que eu disse acima:
> teorias mais fracas que PRA não "entendem" o que significa a sentença da
> consistência.
>
> 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] trabalho do Nelson

[Valeria de Paiva]

Doria,
eu nao conheco a prova do Kunen, nao posso opinar.

quanto a prova do Goedel, se voce estiver falando da prova que usa a
interpretacao dialectica e a "negative translation" a razao pra nao
acreditar 'e dupla: voce pode nao acreditar em logica classica,
somente na intuicionistica e/ou voce pode nao acreditar que os
funcionais necessitados pela interpretacao sejam razoaveis. tem uma
discussao legal nos collected works editados pelo Feferman et al.

pra terminar eu acho que tenho varias razoes pra nao acreditar nas
nocoes usuais de teoria da complexidade. elas sao "coding" da pior
especie, mascaram a realidade matematica, na minha opiniao.

abs
Valeria

2011/9/30 Francisco Antonio Doria :
> Por que não acreditar na prova de consistência de Goedel para PA? Ou na de
> Kunen, baseada num algoritmo?
>
> 2011/9/30 Valeria de Paiva 
>>
>> Rodrigo,
>> Muito obrigada pela informacao detalhada abaixo! Aprendi muito, mas
>> continuo com uma duvidas basica.
>>
>> Nao, eu nao quero fazer "aritmetica limitada" e  nao quero perder
>> consistencia.
>>
>> Mas quero saber se voce (e todo mundo que a gente acredita) tambem
>> acha que PRA realmente 'e garantidamente consistente.
>>
>> obrigada,
>> valeria
>>
>> 2011/9/29 Rodrigo Freire :
>> > Minha dúvida sobre o trabalho do Nelson é de outra natureza: mesmo que
>> > todas as expectativas se confirmem e realmente a coisa esteja furada,
>> > o que ainda poderá ser dito da *alternativa finitista* que ele propõe
>> > para "consertar PRA"?  Será um sistema metamatemático cujo interesse
>> > poderá subsistir de modo independente a todo o resto?
>> >
>> >
>> >
>> > Parte do trabalho do Nelson já está incorporada na lógica. Ele é um dos
>> > precursores da aritmética limitada.
>> > O livro predicative arithmetic, de 1986, está disponível online na
>> > página
>> > dele. Contém os primeiros passos do projeto dele.
>> >
>> > De especial interesse para lógicos é a aritmetização dos teoremas da
>> > lógica
>> > básica em sistemas interpretaveis em Q.
>> > Ele segue o Shoenfield, cap. 1 a 4. Ele consegue provar uma boa parte
>> > dos
>> > resultados, mas não consegue alguns resultados centrais.
>> > Nessa parte, acho que o melhor que ele conseguiu foi demonstrar o
>> > teorema de
>> > extensões funcionais (com unicidade) em um sistema compatível com Q e
>> > sem
>> > ter que fazer a prova enfadonha que tem no Kleene (que aliás é um livro
>> > é
>> > pouco humano). A prova desse teorema no Shoenfield não cabe em sistemas
>> > aceitáveis para o Nelson.
>> >
>> > Os resultados centrais que ele não consegue: Hilbert-Ackerman, Herbrand,
>> > Skolem (sobre extensões funcionais em geral) e tudo o mais relacionado a
>> > esses. Por que não dá para obter esses resultados? Hilbert-Ackerman e
>> > Herbrand provam a consistência de Q. O teorema de Skolem, eu não sei.
>> > Quem
>> > trabalha com aritmética limitada deve saber. O segundo teorema da
>> > incompletude também é modificado.
>> >
>> > Como Hilbert-Ackerman tem um papel central para o Nelson, ele consegue
>> > versões restritas do teorema (também dá para conseguir versões restritas
>> > de
>> > eliminação do corte e outros). Essa história de limitar rank e level das
>> > constantes especiais nas provas é para isso: a teoria que ele chama de
>> > Q* só
>> > prova a consistência das "subteorias" tais que as provas são por
>> > consequência tautológica de axiomas com rank e level limitados.
>> >
>> > Com isso ele consegue um mínimo de teoria de sistemas formais para, pelo
>> > menos, dar sentido para "formalização". Não é grande coisa. Considero
>> > que
>> > perder Herbrand é muito sério: a pureza de métodos está indo embora. Mas
>> > acho que é possível aceitar que trabalhando nessa aritmética limitada
>> > como
>> > metateoria dos sistemas formais (no lugar de PRA)  faz sentido falar em
>> > "formalização".
>> >
>> > A partir daí você pode ter dois pontos de vista:
>> >
>> > 1) Essencialmente o ponto de vista de Hilbert trocando PRA por Q, Q* e
>> > outras teorias dessa aritmética do Nelson. Nesse caso, você formaliza a
>> > matemática em ZFC e trabalha normalmente, sempre lembrando que a
>> > metateoria
>> > é essa aritmética limitada. Isso vai gerar algumas preocupações só para
>> > quem
>> > trabalha em fundamentos. É preciso ver se forcing por exemplo é
>> > finitário
>> > nesse sentido. O resto da matemática fica igual. Não é possível dar
>> > provas
>> > de consistência, mas tudo bem, você continua praticamente como estamos
>> > hoje.
>> >
>> > 2) O ponto de vista atual do Nelson: PRA é inconsistente. Aí eu acho que
>> > não
>> > dá para fazer nada. Nem entendo o que significam essas afirmações dele.
>> > É
>> > praticamente uma contradição referencial ele dizer que exibe dois
>> > números n
>> > e m tal que a tetração n tetra m não existe. É aquela pergunta: o que
>> > faz o
>> > algoritmo que calcula essa superexponencial em termos das anteriores
>> > nesse
>> > caso?
>> >
>> >
>> > O erro desse trabalho do Nelson, que acredit

Re: [Logica-l] trabalho do Nelson

[Rodrigo Freire]

Oi João


Obrigado pela indicação. Não, eu não conhecia essa discussão. Também não
conheço a prova do Kripke.

O primeiro teorema da incompletude vale em Q:

Q representa a funções recursivas e o primeiro teorema da incompletude exige
basicamente isso.

Não tenho idéia do que a prova do Kripke exige, eu precisaria estudá-la para
responder.
Desculpe.

Abraço
Rodrigo





2011/9/30 Joao Marcos 

> Olá, Rodrigo:
>
> Vou ter que aprender um pouco mais sobre Aritmética Limitada, com
> certeza.  Obrigado pelas lições iniciais!
>
> Tenho uma outra dúvida.  Nem todos conhecem, mas o Putnam publicou um
> artigo no NDJFL em 2000 com uma demonstração alternativa, proposta por
> Kripke, do primeiro teorema de incompletude, demonstração esta que usa
> bem menos Teoria da Recursão do que a versão original de Gödel.  Há
> uma discussão bacana deste assunto, que você deve ter acompanhado, em:
>
> http://mathoverflow.net/questions/72062/what-are-some-proofs-of-godels-theorem-which-are-essentially-different-from-th
> Aparentemente o segundo teorema de incompletude não é um corolário
> óbvio da versão kripkeana, enfraquecida, do primeiro teorema.
>
> Você faz alguma ideia se o argumento kripkeano poderia ser formulado
> com os recursos de Q?
>
> JM
>
> 2011/9/30 Rodrigo Freire :
> > Mais uma pequena observação que talvez ajude a esclarecer:
> >
> >
> > O segundo teorema da incompletude, formulado apropriadamente, vale para
> Q:
> > se Q é consistente (e é) então Q não prova CON(Q), onde CON(Q) é uma
> > sentença da consistencia de Q. Nada surpreendente, Q é uma teoria muito
> > fraca, e não prova a CON(Q).
> >
> > O problema é que Q é tão fraca que Q não "entende" o que é CON(Q).
> > Formulações diferences da sentença da consistência, que são equivalentes
> nas
> > teorias mais fortes que PRA, não são equivalentes em Q. Q não prova as
> > condições de derivabilidade de Hilbert Bernays, não entende direito o que
> é
> > a aritmetização da provabilidade.
> >
> >
> > Isso pode ser visto como uma formulação precisa do que eu disse acima:
> > teorias mais fracas que PRA não "entendem" o que significa a sentença da
> > consistência.
> >
> > 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] trabalho do Nelson

[Rodrigo Freire]

Oi Valéria

voce pode nao acreditar que os
funcionais necessitados pela interpretacao sejam razoaveis.


É, acho que esse é o principal motivo: se usar funcionais de tipo superior
não é legítimo para definir funções então a prova de consistência vai por
água abaixo.

O Shoenfield adaptou a interpretação dialética para aplicá-la direto a PA
sem passar por HA. Então não sei se essa preocupação com a tradução de Godel
é realmente significativa.


pra terminar eu acho que tenho varias razoes pra nao acreditar nas
nocoes usuais de teoria da complexidade. elas sao "coding" da pior
especie, mascaram a realidade matematica, na minha opiniao.



Não entendo nada de teoria da complexidade, mas também fico um pouco cético
com relação às noções usuais dessa teoria. Talvez ainda não tenha encontrado
a perspectiva correta. Talvez falta um pouco de semântica. Mas como eu
falei, não entendo nada disso e esses palpites apenas expressam uma
sensação, não tem bases muito sólidas.

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] trabalho do Nelson

[Rodrigo Freire]

Apenas uma observação:

O lógico Bruno Poizat tem uma abordagem modelo teórica para a complexidade
apresentada no livro:

http://www.amazon.com/petits-cailloux-modele-theorique-lalgorithmie-wa-al-marifah/dp/2908016583/ref=sr_1_1?ie=UTF8&qid=1317402575&sr=8-1



Não conheço o trabalho, tem gente na lista bem melhor que eu para comentar.

Abraço
Rodrigo




2011/9/30 Rodrigo Freire 

> Oi Valéria
>
>
> voce pode nao acreditar que os
> funcionais necessitados pela interpretacao sejam razoaveis.
>
>
> É, acho que esse é o principal motivo: se usar funcionais de tipo superior
> não é legítimo para definir funções então a prova de consistência vai por
> água abaixo.
>
> O Shoenfield adaptou a interpretação dialética para aplicá-la direto a PA
> sem passar por HA. Então não sei se essa preocupação com a tradução de Godel
> é realmente significativa.
>
>
>
> pra terminar eu acho que tenho varias razoes pra nao acreditar nas
> nocoes usuais de teoria da complexidade. elas sao "coding" da pior
> especie, mascaram a realidade matematica, na minha opiniao.
>
>
>
> Não entendo nada de teoria da complexidade, mas também fico um pouco cético
> com relação às noções usuais dessa teoria. Talvez ainda não tenha encontrado
> a perspectiva correta. Talvez falta um pouco de semântica. Mas como eu
> falei, não entendo nada disso e esses palpites apenas expressam uma
> sensação, não tem bases muito sólidas.
>
> 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] trabalho do Nelson

[Francisco Antonio Doria]

Oi, Valeria,

Minha msg foi uma provocação... Concordo com seu último parágrafo, como
tenh0 insistido aqui - sobretudo porque a noção de conjunto de máquinas
polinomiais, exponenciais, etc, só tem sentido se referida a algum sistema
formal.

Na prova de Kunen vc vê a indução transfinita, sob forma de um cálculo de
função que representa um sistema de notação de ordinais construtivos. PA não
sabe disso, mas a gente sabe: o cálculo chega ao fim.

2011/9/30 Valeria de Paiva 

> Doria,
> eu nao conheco a prova do Kunen, nao posso opinar.
>
> quanto a prova do Goedel, se voce estiver falando da prova que usa a
> interpretacao dialectica e a "negative translation" a razao pra nao
> acreditar 'e dupla: voce pode nao acreditar em logica classica,
> somente na intuicionistica e/ou voce pode nao acreditar que os
> funcionais necessitados pela interpretacao sejam razoaveis. tem uma
> discussao legal nos collected works editados pelo Feferman et al.
>
> pra terminar eu acho que tenho varias razoes pra nao acreditar nas
> nocoes usuais de teoria da complexidade. elas sao "coding" da pior
> especie, mascaram a realidade matematica, na minha opiniao.
>
> abs
> Valeria
>
> 2011/9/30 Francisco Antonio Doria :
> > Por que não acreditar na prova de consistência de Goedel para PA? Ou na
> de
> > Kunen, baseada num algoritmo?
> >
> > 2011/9/30 Valeria de Paiva 
> >>
> >> Rodrigo,
> >> Muito obrigada pela informacao detalhada abaixo! Aprendi muito, mas
> >> continuo com uma duvidas basica.
> >>
> >> Nao, eu nao quero fazer "aritmetica limitada" e  nao quero perder
> >> consistencia.
> >>
> >> Mas quero saber se voce (e todo mundo que a gente acredita) tambem
> >> acha que PRA realmente 'e garantidamente consistente.
> >>
> >> obrigada,
> >> valeria
> >>
> >> 2011/9/29 Rodrigo Freire :
> >> > Minha dúvida sobre o trabalho do Nelson é de outra natureza: mesmo que
> >> > todas as expectativas se confirmem e realmente a coisa esteja furada,
> >> > o que ainda poderá ser dito da *alternativa finitista* que ele propõe
> >> > para "consertar PRA"?  Será um sistema metamatemático cujo interesse
> >> > poderá subsistir de modo independente a todo o resto?
> >> >
> >> >
> >> >
> >> > Parte do trabalho do Nelson já está incorporada na lógica. Ele é um
> dos
> >> > precursores da aritmética limitada.
> >> > O livro predicative arithmetic, de 1986, está disponível online na
> >> > página
> >> > dele. Contém os primeiros passos do projeto dele.
> >> >
> >> > De especial interesse para lógicos é a aritmetização dos teoremas da
> >> > lógica
> >> > básica em sistemas interpretaveis em Q.
> >> > Ele segue o Shoenfield, cap. 1 a 4. Ele consegue provar uma boa parte
> >> > dos
> >> > resultados, mas não consegue alguns resultados centrais.
> >> > Nessa parte, acho que o melhor que ele conseguiu foi demonstrar o
> >> > teorema de
> >> > extensões funcionais (com unicidade) em um sistema compatível com Q e
> >> > sem
> >> > ter que fazer a prova enfadonha que tem no Kleene (que aliás é um
> livro
> >> > é
> >> > pouco humano). A prova desse teorema no Shoenfield não cabe em
> sistemas
> >> > aceitáveis para o Nelson.
> >> >
> >> > Os resultados centrais que ele não consegue: Hilbert-Ackerman,
> Herbrand,
> >> > Skolem (sobre extensões funcionais em geral) e tudo o mais relacionado
> a
> >> > esses. Por que não dá para obter esses resultados? Hilbert-Ackerman e
> >> > Herbrand provam a consistência de Q. O teorema de Skolem, eu não sei.
> >> > Quem
> >> > trabalha com aritmética limitada deve saber. O segundo teorema da
> >> > incompletude também é modificado.
> >> >
> >> > Como Hilbert-Ackerman tem um papel central para o Nelson, ele consegue
> >> > versões restritas do teorema (também dá para conseguir versões
> restritas
> >> > de
> >> > eliminação do corte e outros). Essa história de limitar rank e level
> das
> >> > constantes especiais nas provas é para isso: a teoria que ele chama de
> >> > Q* só
> >> > prova a consistência das "subteorias" tais que as provas são por
> >> > consequência tautológica de axiomas com rank e level limitados.
> >> >
> >> > Com isso ele consegue um mínimo de teoria de sistemas formais para,
> pelo
> >> > menos, dar sentido para "formalização". Não é grande coisa. Considero
> >> > que
> >> > perder Herbrand é muito sério: a pureza de métodos está indo embora.
> Mas
> >> > acho que é possível aceitar que trabalhando nessa aritmética limitada
> >> > como
> >> > metateoria dos sistemas formais (no lugar de PRA)  faz sentido falar
> em
> >> > "formalização".
> >> >
> >> > A partir daí você pode ter dois pontos de vista:
> >> >
> >> > 1) Essencialmente o ponto de vista de Hilbert trocando PRA por Q, Q* e
> >> > outras teorias dessa aritmética do Nelson. Nesse caso, você formaliza
> a
> >> > matemática em ZFC e trabalha normalmente, sempre lembrando que a
> >> > metateoria
> >> > é essa aritmética limitada. Isso vai gerar algumas preocupações só
> para
> >> > quem
> >> > trabalha em fundamentos. É preciso ver se forcing por

Re: [Logica-l] trabalho do Nelson

[Rodrigo Freire]

Oi Valeria

Para ficar bem claro: acredito que PRA é consistente, mas é bem mais do que
isso. Acredito que dizer que PRA é inconsistente é sem sentido.

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] trabalho do Nelson

[Francisco Antonio Doria]

Enfim algo sensato... Pensei que, se mudarmos o modelo standard, talvez -
mas esse novo modelo standard seria inatural (PRA como que mimetiza nossas
intuições no modelo standard).

2011/9/30 Rodrigo Freire 

> Oi Valeria
>
> Para ficar bem claro: acredito que PRA é consistente, mas é bem mais do que
> isso. Acredito que dizer que PRA é inconsistente é sem sentido.
>
> Abraço
> Rodrigo
>



-- 
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] trabalho do Nelson

[Valeria de Paiva]

oi Rodrigo,

Obrigada pela mensagem abaixo, eu tb estou na mesma situacao de:
>não entendo nada disso e esses palpites apenas expressam uma
> sensação, não tem bases muito sólidas.
"gut feelings", sem argumentos solidos, aqui tambem...

eu tentei uma vez ensinar complexidade pra computacao sem usar logica
classica, usando programas funcionais e raciocinio constructivo, mas
nao consegui fazer nem a primeira aula direito. Alguem devia
faze-lo...

Mas a minha visao 'e diferente quanto a:
>O Shoenfield adaptou a interpretação dialética para aplicá-la direto a PA
> sem passar por HA. Então não sei se essa preocupação com a tradução de Godel
> é realmente significativa.
voce leu a minha preocupacao com HA da maneira inversa do que a que eu
pretendia. eu gosto de passar por HA, o que eu gostaria na verdade e'
de fazer logica classica mais parecida com logica intuicionista, de
providenciar Curry-Howard pra logica classica de uma maneira
canonica...dai o que eu quero 'e extrair das preocupacoes do Nelson,
as que eu compartilho...

eu tambem acredito que PRA 'e consistente, por isso gostaria de
entender melhor porque o Nelson acha que nao 'e, pois nao concordo
contigo quando voce diz que ``dizer que PRA é inconsistente é sem
sentido". Pode ser que nao faca sentido da forma como as definicoes
estao organizadas, mas a regra do jogo 'e descobrir quais sao as
definicoes que fazem mais sentido pra gente, nao? qual 'e a definicao
de numero natural, de principio de inducao que faz mais sentido e
prova mais teoremas, sem introduzir conceitos duvidosos que nem o
"terceiro excluido"--essas sao as perguntas que queremos responder,
nao?

obrigada pelas explicacoes,
Valeria


2011/9/30 Rodrigo Freire :
> Oi Valéria
>
> voce pode nao acreditar que os
> funcionais necessitados pela interpretacao sejam razoaveis.
>
>
> É, acho que esse é o principal motivo: se usar funcionais de tipo superior
> não é legítimo para definir funções então a prova de consistência vai por
> água abaixo.
>
> O Shoenfield adaptou a interpretação dialética para aplicá-la direto a PA
> sem passar por HA. Então não sei se essa preocupação com a tradução de Godel
> é realmente significativa.
>
>
> pra terminar eu acho que tenho varias razoes pra nao acreditar nas
> nocoes usuais de teoria da complexidade. elas sao "coding" da pior
> especie, mascaram a realidade matematica, na minha opiniao.
>
>
>
> Não entendo nada de teoria da complexidade, mas também fico um pouco cético
> com relação às noções usuais dessa teoria. Talvez ainda não tenha encontrado
> a perspectiva correta. Talvez falta um pouco de semântica. Mas como eu
> falei, não entendo nada disso e esses palpites apenas expressam uma
> sensação, não tem bases muito sólidas.
>
> Abraço
> Rodrigo
>



-- 
Valeria de Paiva
http://www.cs.bham.ac.uk/~vdp/
http://valeriadepaiva.org/www/
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l

Re: [Logica-l] trabalho do Nelson

[Rodrigo Freire]

Oi Valéria

Até onde posso compreender, o Nelson acredita que PRA é inconsistente por
acreditar que algumas funções primitivas recursivas não são totais. Não
consigo entender o que isso significa.

Mais especificamente: Nelson acredita que superexponenciação não é total.

Considere a seguinte sequencia de funções primitivas recursivas: constante
igua a 0, sucessor,  soma, produto, exponenciação com base 2,
superexponenciação com base 2. Nelson acredita que uma dessas não é total e
não é 0 nem sucessor. Considere a primeira. Chamemos ela de f. Considere o
primeiro argumento n em que f não "dá resultado". O que acontece com o
algoritmo que calcula f(n) em termos das funções primitivas recursivas
anteriores (que são totais) e de f para argumentos menores que n (que
existem)?

Você pode mudar o sentido de número e decretar que números acima de algum
valor não existem. A função sucessor não é mais total, etc. Mas isso é
destruir a noção de número.


Também é possível mudar o que significa "consistência". Por exemplo dizendo
que não há provas de complexidade menor ou igual a n de 0=1, para alguma
noção de complexidade e algum n. Aí o problema da consistência pode passar a
fazer sentido para PRA. No sentido usual do termo, o problema da
consistência não se coloca para PRA.
De novo, o que está acontecendo é uma destruição da noção de prova, e da
noção dependente de consistência.  As regras de inferência não são mais
totais? Por que não?


De acordo com a sua pergunta: essas não são as noções de número e de prova
que fazem mais sentido, que colocam restrições artificiais nas noções
clássicas sem nenhuma razão para fazer isso.

Essa citação do Harvey Friedman expressa a situação:

"I raised just this objection with the (extreme) ultrafinitist Esenin-Volpin
during a lecture of his. He asked me to be more specific. I then proceeded
to start with 2^1 and asked him whether this is “real” or something to that
effect. He virtually immediately said yes. Then I asked about 2^2, and he
again said yes, but with a perceptible delay. Then 2^3, and yes, but with
more delay. This continued for a couple of more times, till it was obvious
how he was handling this objection. Sure, he was prepared to always answer
yes, but he was going to take 2^100 times as long to answer yes to 2^100
then he would to answering 2^1. There is no way that I could get very far
with this."



Abraço
Rodrigo


2011/9/30 Valeria de Paiva 

> oi Rodrigo,
>
> Obrigada pela mensagem abaixo, eu tb estou na mesma situacao de:
> >não entendo nada disso e esses palpites apenas expressam uma
> > sensação, não tem bases muito sólidas.
> "gut feelings", sem argumentos solidos, aqui tambem...
>
> eu tentei uma vez ensinar complexidade pra computacao sem usar logica
> classica, usando programas funcionais e raciocinio constructivo, mas
> nao consegui fazer nem a primeira aula direito. Alguem devia
> faze-lo...
>
> Mas a minha visao 'e diferente quanto a:
> >O Shoenfield adaptou a interpretação dialética para aplicá-la direto a PA
> > sem passar por HA. Então não sei se essa preocupação com a tradução de
> Godel
> > é realmente significativa.
> voce leu a minha preocupacao com HA da maneira inversa do que a que eu
> pretendia. eu gosto de passar por HA, o que eu gostaria na verdade e'
> de fazer logica classica mais parecida com logica intuicionista, de
> providenciar Curry-Howard pra logica classica de uma maneira
> canonica...dai o que eu quero 'e extrair das preocupacoes do Nelson,
> as que eu compartilho...
>
> eu tambem acredito que PRA 'e consistente, por isso gostaria de
> entender melhor porque o Nelson acha que nao 'e, pois nao concordo
> contigo quando voce diz que ``dizer que PRA é inconsistente é sem
> sentido". Pode ser que nao faca sentido da forma como as definicoes
> estao organizadas, mas a regra do jogo 'e descobrir quais sao as
> definicoes que fazem mais sentido pra gente, nao? qual 'e a definicao
> de numero natural, de principio de inducao que faz mais sentido e
> prova mais teoremas, sem introduzir conceitos duvidosos que nem o
> "terceiro excluido"--essas sao as perguntas que queremos responder,
> nao?
>
> obrigada pelas explicacoes,
> Valeria
>
>
>
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l

Re: [Logica-l] trabalho do Nelson

[Valeria de Paiva]

Rodrigo,
Deixa eu tentar explicar o que eu acho que o Nelson *pode* estar querendo dizer.

>Você pode mudar o sentido de número e decretar que números acima de algum
> valor não existem. A função sucessor não é mais total, etc. Mas isso é
> destruir a noção de número.

sim, mas nao 'e isso que queremos. e acho que nao 'e isso que o Nelson
esta' fazendo. a funcao sucessor 'e total, como a gente normalmente
considera, pode ser descrita pelo lambda termo (\lambda x. x+1) e 1 'e
um numero legal e somar com 1 tambem funciona bem.

a gente tambem pode definir adicao e multiplicacao usando lambda
termos e podemos talvez pensar no tempo/espaco que leva pra normalizar
o termo correspondente. isto 'e no esforco/trabalho que da' pra
reduzir \lambda x. ( suc(suc(suc(Zero +  \lambda x.
((suc(suc(Zero pra 5.


Dai talvez faca algum sentido dizer que superexponenciacao 'e
diferente da funcao sucessor e que uma sempre termina, mas a outra
nao. nao sei se 'e isso que ele esta dizendo e em vez de ficar falando
bobagens eu devia era ler o famoso documento de 100 paginas, mas
pensando em reducoes de lambda termos eu pelo menos consigo ver que
pode existir uma nocao de prova bem parecida com a minha, que leva em
consideracao alguma nocao de complexidade para produzir um resultado
aritmetico.

dai que pode existir uma nocao nada artificial que coloque restricoes
nas nocoes classicas e leve o Nelson a dizer que superexponenciacao
nao termina sempre(ou melhor que nao podemos garantir que a
superexponenciacao sempre termine). eu nao sei se 'e isso que ele
esta' dizendo, e achei que alguem saberia me dizer, sem muito esforco.

obrigada pela conversa,
Valeria

2011/9/30 Rodrigo Freire :
> Oi Valéria
>
> Até onde posso compreender, o Nelson acredita que PRA é inconsistente por
> acreditar que algumas funções primitivas recursivas não são totais. Não
> consigo entender o que isso significa.
>
> Mais especificamente: Nelson acredita que superexponenciação não é total.
>
> Considere a seguinte sequencia de funções primitivas recursivas: constante
> igua a 0, sucessor,  soma, produto, exponenciação com base 2,
> superexponenciação com base 2. Nelson acredita que uma dessas não é total e
> não é 0 nem sucessor. Considere a primeira. Chamemos ela de f. Considere o
> primeiro argumento n em que f não "dá resultado". O que acontece com o
> algoritmo que calcula f(n) em termos das funções primitivas recursivas
> anteriores (que são totais) e de f para argumentos menores que n (que
> existem)?
>
> Você pode mudar o sentido de número e decretar que números acima de algum
> valor não existem. A função sucessor não é mais total, etc. Mas isso é
> destruir a noção de número.
>
>
> Também é possível mudar o que significa "consistência". Por exemplo dizendo
> que não há provas de complexidade menor ou igual a n de 0=1, para alguma
> noção de complexidade e algum n. Aí o problema da consistência pode passar a
> fazer sentido para PRA. No sentido usual do termo, o problema da
> consistência não se coloca para PRA.
> De novo, o que está acontecendo é uma destruição da noção de prova, e da
> noção dependente de consistência.  As regras de inferência não são mais
> totais? Por que não?
>
>
> De acordo com a sua pergunta: essas não são as noções de número e de prova
> que fazem mais sentido, que colocam restrições artificiais nas noções
> clássicas sem nenhuma razão para fazer isso.
>
> Essa citação do Harvey Friedman expressa a situação:
>
> "I raised just this objection with the (extreme) ultrafinitist Esenin-Volpin
> during a lecture of his. He asked me to be more specific. I then proceeded
> to start with 2^1 and asked him whether this is “real” or something to that
> effect. He virtually immediately said yes. Then I asked about 2^2, and he
> again said yes, but with a perceptible delay. Then 2^3, and yes, but with
> more delay. This continued for a couple of more times, till it was obvious
> how he was handling this objection. Sure, he was prepared to always answer
> yes, but he was going to take 2^100 times as long to answer yes to 2^100
> then he would to answering 2^1. There is no way that I could get very far
> with this."
>
>
>
> Abraço
> Rodrigo
>
>
> 2011/9/30 Valeria de Paiva 
>>
>> oi Rodrigo,
>>
>> Obrigada pela mensagem abaixo, eu tb estou na mesma situacao de:
>> >não entendo nada disso e esses palpites apenas expressam uma
>> > sensação, não tem bases muito sólidas.
>> "gut feelings", sem argumentos solidos, aqui tambem...
>>
>> eu tentei uma vez ensinar complexidade pra computacao sem usar logica
>> classica, usando programas funcionais e raciocinio constructivo, mas
>> nao consegui fazer nem a primeira aula direito. Alguem devia
>> faze-lo...
>>
>> Mas a minha visao 'e diferente quanto a:
>> >O Shoenfield adaptou a interpretação dialética para aplicá-la direto a PA
>> > sem passar por HA. Então não sei se essa preocupação com a tradução de
>> > Godel
>> > é realmente significativa.
>> voce leu a minha preocupacao com HA da mane

[Logica-l] Tools for Teaching Logic

[Adolfo Neto]

Olá,

Já está disponível (com texto parcial) na Biblioteca  do Google o livro

Tools for Teaching Logic: Third International Congress, TICTTL 2011,
Salamanca, Spain, June 1-4, 2011, Proceedings
Patrick Blackburn, Hans van Ditmarsch, Maria Manzano, Fernando Soler-Toscano

http://books.google.com/books?hl=es&lr=&id=be-pTR5TmZIC&oi=fnd&pg=PA239&ots=Od7aGgQM7p&sig=2FFI2t4ZNp4ODXnt_pS_JAfrjzY#v=onepage&q&f=false

Aproveitando a oportunidade, quero pedir aos que ensinam Lógica por aí que
dêem *sugestões para a implementacao de alguma ferramenta que possa ser útil
para os professores de Lógica*.

Ano passado, na minha disciplina Métodos Ágeis para o Desenvolvimento de
Software,
eu e meus alunos implementamos o Logicamente-UTFPR:

https://github.com/adolfont/Logicamente-UTFPR

cujo .jar mais recente pode ser baixado de

https://github.com/downloads/adolfont/Logicamente-UTFPR/logicamente-utfpr-alfa-5.1.jar

A ferramenta tem sido muito útil para mim. Uso nas minhas aulas e deixo os
alunos usando no laboratório. [A ideia do Logicamente-UTFPR era implementar
em Java algo que já estivesse implementado no Logicamente original
]

Um artigo sobre o Logicamente no Tools for Teaching Logic está em

http://books.google.com/books?id=be-pTR5TmZIC&pg=PA223&hl=es&source=gbs_toc_r&cad=4#v=onepage&q&f=false

Voltando ao "Tools for Teaching Logic 2010", tem uma ferramenta lá que achei
interessante:

http://books.google.com/books?id=be-pTR5TmZIC&pg=PA239&hl=es&source=gbs_toc_r&cad=4#v=onepage&q&f=false

mas o jar que está em

http://www.fdi.ucm.es/profesor/rdelvado/TICTTL2011/

não roda...

O ASA CALCPRO

http://www.asacalcpro.com.br/

também não funciona mais (tentei no WIndows 7 e no Ubuntu 11.04).

Alguém conhece alguma ferramenta relativamente amigável que use tablôs
marcados para lógica proposcional clássica?


[]s
Adolfo

==
Adolfo Neto
Assistant Professor - Federal University of Technology, Paraná
Web: http://www.dainf.ct.utfpr.edu.br/~adolfo
Twitter: http://twitter.com/adolfont
Mestrado em Computação Aplicada: http://www.ppgca.ct.utfpr.edu.br
==
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l

[Logica-l] Nelson, etc

[Francisco Antonio Doria]

Muitos dos problemas que têm sido assinalados nessa discussão sobre  Nelson
resultam de um fato simples: sistemas axiomáticos como os usuais
(consistentes, incluem bastante aritmética, possuem um conjunto r.e. de
teoremas, têm por linguagem a lógica clássica) não se prestam à teoria da
computação: muitos fatos simples e intuitivamente claros resultam, na versão
formal, em sentenças indecidíveis. Me parece que a teoria da computação
exige algum tipo de regra infinitária na sua axiomatização, se desejarmos
que nossas intuições a respeito se reflitam em teoremas da teoria.

-- 
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