Axiomatizando a teoria da computação

57 views
Skip to first unread message

Francisco Antonio Doria

unread,
Feb 19, 2017, 12:19:11 AM2/19/17
to logi...@dimap.ufrn.br
Como se sabe, ZF, ZFC, e mesmo PA (aritmética de Peano) não servem para axiomatizarmos a teoria da computação, já que uma infinidade de funções recursivas terão propriedades formalmente indecidíveis mas trivialmente verdadeiras. A gente fica sem poder provar uma infinidade de propriedades óbvias.

Alguém já viu uma axiomática para a teoria da computação como PA + Regra omega de Shoenfield?

Claudio Andrés Callejas Olguín

unread,
Feb 19, 2017, 10:11:44 PM2/19/17
to Lista dos Logicos Brasileiros

Bom dia Fracisco Antonio,

 

Eu não conheço nenhuma axiomática como a da sua pergunta, mas provavelmente pode ser do seu interesse a axiomática para as funções totais recursivas apresentada no Teorema I.3.6 na página 43 do excelente livro “Classical recursion theory” vol.1 de Odifreddi.

 

Atenciosamente,

Claudio Callejas.


2017-02-19 2:19 GMT-03:00 Francisco Antonio Doria <fama...@gmail.com>:
Como se sabe, ZF, ZFC, e mesmo PA (aritmética de Peano) não servem para axiomatizarmos a teoria da computação, já que uma infinidade de funções recursivas terão propriedades formalmente indecidíveis mas trivialmente verdadeiras. A gente fica sem poder provar uma infinidade de propriedades óbvias.

Alguém já viu uma axiomática para a teoria da computação como PA + Regra omega de Shoenfield?

--
Você recebeu essa mensagem porque está inscrito no grupo "LOGICA-L" dos Grupos do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+unsubscribe@dimap.ufrn.br.
Para postar nesse grupo, envie um e-mail para logi...@dimap.ufrn.br.
Acesse esse grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CA%2BuR7BLUEnW7aLShc8j5qtYZM54yvjBZsNV7LWNxSvRcN-cgMQ%40mail.gmail.com.

Francisco Antonio Doria

unread,
Feb 20, 2017, 4:14:49 AM2/20/17
to logi...@dimap.ufrn.br
Obrigado! Funções recursivas totais são justamente o problema com essas axiomatizações, porque o conjunto das provadamente totais na teoria é estritamente menor que aquele das `verdadeiramente' totais, numa interpretação standard. 

2017-02-20 0:11 GMT-03:00 Claudio Andrés Callejas Olguín <ccalleja...@gmail.com>:

Bom dia Fracisco Antonio,

 

Eu não conheço nenhuma axiomática como a da sua pergunta, mas provavelmente pode ser do seu interesse a axiomática para as funções totais recursivas apresentada no Teorema I.3.6 na página 43 do excelente livro “Classical recursion theory” vol.1 de Odifreddi.

 

Atenciosamente,

Claudio Callejas.

2017-02-19 2:19 GMT-03:00 Francisco Antonio Doria <fama...@gmail.com>:
Como se sabe, ZF, ZFC, e mesmo PA (aritmética de Peano) não servem para axiomatizarmos a teoria da computação, já que uma infinidade de funções recursivas terão propriedades formalmente indecidíveis mas trivialmente verdadeiras. A gente fica sem poder provar uma infinidade de propriedades óbvias.

Alguém já viu uma axiomática para a teoria da computação como PA + Regra omega de Shoenfield?

--
Você recebeu essa mensagem porque está inscrito no grupo "LOGICA-L" dos Grupos do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+u...@dimap.ufrn.br.

Para postar nesse grupo, envie um e-mail para logi...@dimap.ufrn.br.
Acesse esse grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CA%2BuR7BLUEnW7aLShc8j5qtYZM54yvjBZsNV7LWNxSvRcN-cgMQ%40mail.gmail.com.

--
Você recebeu essa mensagem porque está inscrito no grupo "LOGICA-L" dos Grupos do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+unsubscribe@dimap.ufrn.br.
Para postar nesse grupo, envie um e-mail para logi...@dimap.ufrn.br.
Acesse esse grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAE_57e1wLh2QNPxLyrKHsbrG1U%3DgG%2BjmS-UP6nBTvs51ZpH2EQ%40mail.gmail.com.



--
fad

ahhata alati, awienta Wilushati

Francisco Antonio Doria

unread,
Feb 20, 2017, 4:18:39 AM2/20/17
to logi...@dimap.ufrn.br
Daí resulta que - por exemplo - uma infinidade de conjuntos de máquinas de Turing polinomiais no tempo, na interpretação standard, têm justo essa propriedade, indecidível. 

2017-02-20 6:14 GMT-03:00 Francisco Antonio Doria <fama...@gmail.com>:
Obrigado! Funções recursivas totais são justamente o problema com essas axiomatizações, porque o conjunto das provadamente totais na teoria é estritamente menor que aquele das `verdadeiramente' totais, numa interpretação standard. 
2017-02-20 0:11 GMT-03:00 Claudio Andrés Callejas Olguín <ccalleja...@gmail.com>:

Bom dia Fracisco Antonio,

 

Eu não conheço nenhuma axiomática como a da sua pergunta, mas provavelmente pode ser do seu interesse a axiomática para as funções totais recursivas apresentada no Teorema I.3.6 na página 43 do excelente livro “Classical recursion theory” vol.1 de Odifreddi.

 

Atenciosamente,

Claudio Callejas.


2017-02-19 2:19 GMT-03:00 Francisco Antonio Doria <fama...@gmail.com>:
Como se sabe, ZF, ZFC, e mesmo PA (aritmética de Peano) não servem para axiomatizarmos a teoria da computação, já que uma infinidade de funções recursivas terão propriedades formalmente indecidíveis mas trivialmente verdadeiras. A gente fica sem poder provar uma infinidade de propriedades óbvias.

Alguém já viu uma axiomática para a teoria da computação como PA + Regra omega de Shoenfield?

--
Você recebeu essa mensagem porque está inscrito no grupo "LOGICA-L" dos Grupos do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+u...@dimap.ufrn.br.
Para postar nesse grupo, envie um e-mail para logi...@dimap.ufrn.br.
Acesse esse grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CA%2BuR7BLUEnW7aLShc8j5qtYZM54yvjBZsNV7LWNxSvRcN-cgMQ%40mail.gmail.com.

--
Você recebeu essa mensagem porque está inscrito no grupo "LOGICA-L" dos Grupos do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+u...@dimap.ufrn.br.
Para postar nesse grupo, envie um e-mail para logi...@dimap.ufrn.br.
Acesse esse grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
--
fad

ahhata alati, awienta Wilushati

Claus Akira Horodynski Matsushigue

unread,
Feb 20, 2017, 6:11:34 AM2/20/17
to Lista acadêmica brasileira dos profissionais e estudantes da área de LOGICA, Claus Akira Horodynski Matsushigue

Prezado Dória....



 > Como se sabe, ZF, ZFC, e mesmo PA (aritmética de Peano) não servem
 > para axiomatizarmos a teoria da computação, já que uma infinidade de 
 > funções recursivas terão propriedades formalmente indecidíveis mas
 > trivialmente verdadeiras. A gente fica sem poder provar uma infinidade de
 > propriedades óbvias.

Sim!

 > Alguém já viu uma axiomática para a teoria da computação como PA + Regra omega de Shoenfield?

Mão, não é suficiente.  Acho que já conversamos isso aqui na lista.


Forte abraço, Claus



2017-02-19 2:19 GMT-03:00 Francisco Antonio Doria <fama...@gmail.com>:
Como se sabe, ZF, ZFC, e mesmo PA (aritmética de Peano) não servem para axiomatizarmos a teoria da computação, já que uma infinidade de funções recursivas terão propriedades formalmente indecidíveis mas trivialmente verdadeiras. A gente fica sem poder provar uma infinidade de propriedades óbvias.

Alguém já viu uma axiomática para a teoria da computação como PA + Regra omega de Shoenfield?

--
Você recebeu essa mensagem porque está inscrito no grupo "LOGICA-L" dos Grupos do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+unsubscribe@dimap.ufrn.br.

Francisco Antonio Doria

unread,
Feb 20, 2017, 6:15:37 AM2/20/17
to logi...@dimap.ufrn.br
Pois é, minha dúvida é essa, pois juntar a regra omega tout court é bastante, e a regra de Shoenfield - que eu saiba - prova as sentenças aritméticas verdadeiras (no modelo standard). 

2017-02-20 8:11 GMT-03:00 Claus Akira Horodynski Matsushigue <clau...@mat.unb.br>:

Prezado Dória....



 > Como se sabe, ZF, ZFC, e mesmo PA (aritmética de Peano) não servem
 > para axiomatizarmos a teoria da computação, já que uma infinidade de 
 > funções recursivas terão propriedades formalmente indecidíveis mas
 > trivialmente verdadeiras. A gente fica sem poder provar uma infinidade de
 > propriedades óbvias.

Sim!

 > Alguém já viu uma axiomática para a teoria da computação como PA + Regra omega de Shoenfield?

Mão, não é suficiente.  Acho que já conversamos isso aqui na lista.


Forte abraço, Claus


2017-02-19 2:19 GMT-03:00 Francisco Antonio Doria <fama...@gmail.com>:
Como se sabe, ZF, ZFC, e mesmo PA (aritmética de Peano) não servem para axiomatizarmos a teoria da computação, já que uma infinidade de funções recursivas terão propriedades formalmente indecidíveis mas trivialmente verdadeiras. A gente fica sem poder provar uma infinidade de propriedades óbvias.

Alguém já viu uma axiomática para a teoria da computação como PA + Regra omega de Shoenfield?

--
Você recebeu essa mensagem porque está inscrito no grupo "LOGICA-L" dos Grupos do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+u...@dimap.ufrn.br.

--
Você recebeu essa mensagem porque está inscrito no grupo "LOGICA-L" dos Grupos do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+unsubscribe@dimap.ufrn.br.
Para postar nesse grupo, envie um e-mail para logi...@dimap.ufrn.br.
Acesse esse grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAJh6kGVQ7TNkt9Fs%3DjmzC0bib1%2Bg-WH7md0_3%3DhfP3SVVBKXCA%40mail.gmail.com.

Francisco Antonio Doria

unread,
Feb 20, 2017, 6:25:21 AM2/20/17
to logi...@dimap.ufrn.br
Pois é, minha dúvida é essa, pois juntar a regra omega tout court é bastante, e a regra de Shoenfield - que eu saiba - prova as sentenças aritméticas verdadeiras (no modelo standard). 
2017-02-20 8:11 GMT-03:00 Claus Akira Horodynski Matsushigue <clau...@mat.unb.br>:

Prezado Dória....



 > Como se sabe, ZF, ZFC, e mesmo PA (aritmética de Peano) não servem
 > para axiomatizarmos a teoria da computação, já que uma infinidade de 
 > funções recursivas terão propriedades formalmente indecidíveis mas
 > trivialmente verdadeiras. A gente fica sem poder provar uma infinidade de
 > propriedades óbvias.

Sim!

 > Alguém já viu uma axiomática para a teoria da computação como PA + Regra omega de Shoenfield?

Mão, não é suficiente.  Acho que já conversamos isso aqui na lista.


Forte abraço, Claus


2017-02-19 2:19 GMT-03:00 Francisco Antonio Doria <fama...@gmail.com>:
Como se sabe, ZF, ZFC, e mesmo PA (aritmética de Peano) não servem para axiomatizarmos a teoria da computação, já que uma infinidade de funções recursivas terão propriedades formalmente indecidíveis mas trivialmente verdadeiras. A gente fica sem poder provar uma infinidade de propriedades óbvias.

Alguém já viu uma axiomática para a teoria da computação como PA + Regra omega de Shoenfield?

--
Você recebeu essa mensagem porque está inscrito no grupo "LOGICA-L" dos Grupos do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+u...@dimap.ufrn.br.

--
Você recebeu essa mensagem porque está inscrito no grupo "LOGICA-L" dos Grupos do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+u...@dimap.ufrn.br.

Para postar nesse grupo, envie um e-mail para logi...@dimap.ufrn.br.
Acesse esse grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.

Francisco Antonio Doria

unread,
Feb 20, 2017, 6:34:27 AM2/20/17
to logi...@dimap.ufrn.br
Cito o resultado de Shoenfield: PA + regra omega equivale a PA + regra omega recursiva. 

Sho en eld has shown that PA

rule PA
The sequent calculus enriched with the recursively restricted rule in place of the rule

page2image17432 page2image17600

The rule is said to b e constructive if there is a recursive

n f n is a G odel

numb er of P n where P n is de ned Takeuti This is equivalent

page2image20360

is equivalent to PA recursively restrict      

Claudio Andrés Callejas Olguín

unread,
Feb 20, 2017, 6:38:08 PM2/20/17
to Lista dos Logicos Brasileiros

Boa noite Francisco Antônio,

 

No ano 2015 tentei obter algum novo resultado sobre alguma axiomática para as funções totais recursivas (como é de práxis vou me referir a elas como funções recursivas). Sabia que pelos teoremas da incompletude de Gödel a axiomática não poderia ser completa (ver por exemplo a seção 7.8 do livro de Rogers). Como é bem sabido que o conjunto de índices das funções recursivas é produtivo pensei em tentar obter algum resultado que conectasse aritmética com os conjuntos produtivos e assim ocupar esse resultado para as funções recursivas, mas desisti quando vi que essa conexão já tinha sido estudada no artigo [1] de Horowitz. Aparentemente a tese de doutorado dele (baixo a orientação do Smullyan) foi sobre isso, mas não consegui na época ter acesso a essa tese. Logo disso procurei outras alternativas para estudar as funções recursivas.

 

Provavelmente possa ser do seu interesse o artigo [2], que eu acabei descartando na época por fugir muito da minha área de conhecimento.


 

[1] Horowitz, B.M. Arithmetical analogues of productive and universal sets. Zeitschr. f. math. Logik und Grundlwen d. Math, 203—210, 1982.

[2] Fairtlough, M. and Wainer, S. Hierarchies of provably recursive functions. In Handbook of proof theory, 1998.


Caso você consiga algum novo resultado sobre este assunto gostaria muito que você o compartilhasse nesta lista.


Atenciosamente,

Claudio Callejas.


Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+unsubscribe@dimap.ufrn.br.

Para postar nesse grupo, envie um e-mail para logi...@dimap.ufrn.br.
Acesse esse grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CA%2BuR7BKeoi46ZO174WPmMiUFSgZhY0J2AgVx1bUpt3DExcrUiQ%40mail.gmail.com.

Famadoria

unread,
Feb 20, 2017, 6:48:49 PM2/20/17
to logi...@dimap.ufrn.br
O Wainer estudou, que eu conheça, a hierarquia até $\epsilon_0$, a função cuja totalidade prova que PA é consistente. Newton e eu demos provas para o lema crucial aqui. 

Sent from my iPhone
Reply all
Reply to author
Forward
0 new messages