[Logica-l] Provas do Teorema de Gödel

2017-07-03 Por tôpico Walter Carnielli 
Caro Jean-Yves,  caros todos:


Tenho comigo há alguns anos no CLE a transcrição e as fitas de uma prova do
primeiro Teorema de  Gödel (o segundo é corolário)
que o Kripke deu em Campinas.

A prova é substancialmente  diferente de uma que ele deu  na China e que já
apareceu publicada, mas gostaria de comparar com essa de Paris.

Já pedi a ele pessoalmente várias vezes que me desse permissão para
publicar (em seu none, obviamente,) mas ele sempre diz que está pensando...

Essa de Paris vai sair publicada?

 abraços,

Walter





Em 3 de jul de 2017 20:43, "Fernando Yamauti" 
escreveu:



Em 3 de julho de 2017 09:40, jyb  escreveu:

> Gostaria de apontar que o Saul Kripke apresentou em Paris uma prova
> semantica do teroema de Gödel
> "A Model Theoretic Approach to Gödel's Theorem"
> http://www.logic-in-question.org/
> Bem detalhada mas ainda não publicada, todavia a palestra foi gravada ...
> Saudações
> JYB
>

  Oi Jean-Yves,

  A gravação está disponível em algum lugar online? Eu falhei em encontrar
videos no site da conferencia. Slides já seriam o suficiente (caso ele
tenha usado), mas também não achei algo do tipo.

  Abs.,

  Fernando

-- 
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+unsubscr...@dimap.ufrn.br.
Para postar nesse grupo, envie um e-mail para logica-l@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/CAJGvw-2VBAoYxTAtVz9NOBUe8uQ77Yuxe30t
R-wKiqQkYX1asg%40mail.gmail.com

.

-- 
Você está recebendo esta mensagem porque se inscreveu 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+unsubscr...@dimap.ufrn.br.
Para postar neste grupo, envie um e-mail para logica-l@dimap.ufrn.br.
Visite este grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
Para ver esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CA%2Bob58NOF-Km46wcH8YwEqbt5LRiVb6B38gCVq3_aWs-s3KbDA%40mail.gmail.com.

Re: [Logica-l] How do we construct the Gödel’s sentence in Martin-Löf type theory?

2017-07-03 Por tôpico Fernando Yamauti 
Em 3 de julho de 2017 09:40, jyb  escreveu:

> Gostaria de apontar que o Saul Kripke apresentou em Paris uma prova
> semantica do teroema de Gödel
> "A Model Theoretic Approach to Gödel's Theorem"
> http://www.logic-in-question.org/
> Bem detalhada mas ainda não publicada, todavia a palestra foi gravada ...
> Saudações
> JYB
>

  Oi Jean-Yves,

  A gravação está disponível em algum lugar online? Eu falhei em encontrar
videos no site da conferencia. Slides já seriam o suficiente (caso ele
tenha usado), mas também não achei algo do tipo.

  Abs.,

  Fernando

-- 
Você está recebendo esta mensagem porque se inscreveu 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+unsubscr...@dimap.ufrn.br.
Para postar neste grupo, envie um e-mail para logica-l@dimap.ufrn.br.
Visite este grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
Para ver esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAJGvw-2VBAoYxTAtVz9NOBUe8uQ77Yuxe30tR-wKiqQkYX1asg%40mail.gmail.com.

Re: [Logica-l] How do we construct the Gödel’s sentence in Martin-Löf type theory?

2017-07-03 Por tôpico Rodrigo Freire 
Olá Bruno e Hermógenes,

O Bruno explicou bem, mas ainda vou resumir o meu ponto de modo direto.

Acho que estamos desviando da questão central, Hermógenes. Meu ponto é
muito simples:
- Não há como distinguir a incompletude da aritmética da incompletude da
teoria de grupos sem reconhecer um elemento semântico.

Você pode chamar ou conceber esse elemento semântico de modo diverso: Pode
chamar de noção de número, de modelo standard, de verdade, etc. Tanto faz.

Aceitando o ponto acima, e sabendo da irrelevância da incompletude trivial
da teoria de grupos, concluímos que, quando desprovido do aspecto
semântico, o teorema da incompletude não tem relevância. Isso está em
oposição com o que foi dito que interpretações semânticas do teorema não
querem dizer nada.



> Não. Não há um predicado para "número natural" que ocorre nos
>> axiomas da aritmética [...]
>>
>
> 
>
> Então eu não sei o que você entende por axiomas de Peano.  No meu
> livro, o primeiro axioma já reza:
>
> 1. O zero é um número natural.
>
> :-)
>


Entendo a axiomatização como sistema formal de primeira ordem de tipo
usual, tal como se encontra no livro do Shoenfield, página 204. Os símbolos
primitivos são 0, S, +, ., <. Não há predicado para número. O nome da
teoria encontra-se nessa mesma página: Aritmética de Peano.




Abraço
Rodrigo

-- 
Você está recebendo esta mensagem porque se inscreveu 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+unsubscr...@dimap.ufrn.br.
Para postar neste grupo, envie um e-mail para logica-l@dimap.ufrn.br.
Visite este grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
Para ver esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAExWzU%2B8QObosE2Esz5rHdsUQwAz2iOwjGEsqYwb8GbsKW8S%3Dw%40mail.gmail.com.

Re: [Logica-l] How do we construct the Gödel’s sentence in Martin-Löf type theory?

2017-07-03 Por tôpico Hermógenes Oliveira 

Rodrigo Freire  escreveu:


Não. Não há um predicado para "número natural" que ocorre nos
axiomas da aritmética [...]




Então eu não sei o que você entende por axiomas de Peano.  No meu
livro, o primeiro axioma já reza:

1. O zero é um número natural.

:-)



[...]

Alem disso, apelar para uma "noção de número natural" que aritmética
pretende capturar já é introduzir um elemento semântico que vai além
da sintaxe [...]


Eu concordo com isso (talvez trocando "introduzir" por "reconhecer" ou
"aceitar").


[...] justamente para avaliar a "limitação do formalismo".


Mas *não* concordo com isso, ao menos da forma como está expresso.

O fato de que reconhecemos noções pré-teóricas (supostamente de
caráter semântico, embora não exatamente num sentido técnico do termo
"semântico", e.g. Teoria dos Modelos) que nos guiam na formulação de
sistemas formais não implica, *por si só*, limitações inerentes do
formalismo.


Não há diferença puramente formal entre o caso aritmético e o caso
da teoria de grupos, o que trivializaria sim a relevância
fundacional do teorema na ausência de algum elemento semântico (pois
o caso da incompletude dos grupos é irrelevante).


Bem, o teorema, conforme demonstrado em 1931, é puramente sintático e
responde a uma importante questão de *decidibilidade formal* que havia
sido formulada e estudada no contexto da Escola Hilbertiana desde o
início do século passado.  Portanto, acho que podemos concordar que o
teorema, mesmo na sua formulação original sintática, *não* é trivial.

Quanto à uma suposta "relevância fundacional" que só poderia ser
reconhecida numa interpretação semântica do teorema, eu não saberia
dizer.  Como observei anteriormente, as interpretações semânticas do
teorema, assim como tentativas de formular e demonstrar o teorema em
termos semânticos não fazem o menor sentido para mim.  Claro, esta
observação pode ser tomada como nada além de evidência da minha
própria ignorância e/ou incapacidade.  Para mim, contudo, ela
constitui evidência de que a interpretação semântica do teorema,
juntamente com seus usos e abusos em alegações sobre os "limites da
matemática" (ou formalismo) e "existência de sentenças verdadeiras
indemonstráveis", não passam de histórias pra boi dormir.  Porém, eu
continuo sinceramente buscando evidências contrárias, e, em vista das
informações do JYB, estou curioso para saber o que Kripke tem a dizer
sobre o assunto.  Até agora, contudo, apresentações "semânticas" do
teorema de Gödel tem me decepcionado, inclusive aquelas presentes no
excelente livro de Smullyan sobre o assunto.


--
Hermógenes Oliveira

--
Você está recebendo esta mensagem porque se inscreveu 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+unsubscr...@dimap.ufrn.br.
Para postar neste grupo, envie um e-mail para logica-l@dimap.ufrn.br.
Visite este grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
Para ver esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/20170703164531.Horde.8p6u9YWznSErZ9myGml-znU%40webmail.uni-tuebingen.de.

Re: [Logica-l] How do we construct the Gödel’s sentence in Martin-Löf type theory?

2017-07-03 Por tôpico Bruno Bentzen 
Oi Hermógenes,

Em linhas gerais, acho que o ponto é que muitas teorias são também 
incompletas de uma forma “boring”.
 
Há até mesmo casos em que a sentença indecidível em questão é falsa na 
interpretação pretendida. Aqui é interessante observar que, na aritmética 
de Robinson, Q, por exemplo, a sentença falsa ‘∃x (s(x) = x)’ é 
indecidível.¹
 
Diria que privar os teoremas da incompletude de seu aspecto semântico, é, 
de certa forma, desmembrar um de seus aspectos mais fascinantes: não se 
trata apenas de demonstrar a incompletude, de apresentar uma sentença 
indecidível; trata-se de construir uma sentença verdadeira mas 
indemonstrável, provando assim que em tais teorias da aritmética 
“razoáveis”,  como PA, nunca poderão cumprir a ambição de capturar o 
conjunto de sentenças verdadeiras de sua interpretação pretendida.
 
Abraços,
Bruno
 
¹Construa uma interpretação não-standard cujo domínio compreenda os números 
naturais e um único elemento intruso, c (digamos, Julío César). Agora 
defina a função sucessor da seguinte forma: s’(n)=s(n) para n ∈ ℕ, onde ‘s’ 
denota a função sucessor usual, e, sobretudo, s’(c)=c. Além disso, defina: 
m +’ n = m + n para todo m,n ∈ ℕ, onde ‘+’ denota a adição usual, mas n +’ 
c = c +’ n = c. Similarmente, estipulemos o seguinte (além da definição 
usual da multiplicação para números naturais): n ×’ c = c ×’ n = 0 se n for 
0; n ×’ c = c ×’ n = c caso contrário, para n ∈ ℕ. Essa interpretação 
respeita todos os axiomas de Q, contudo a sentença ‘∃x (s(x) = x’ é 
verdadeira, visto que s’(c)=c.

--
Bruno Bentzen
https://sites.google.com/site/bbentzena/

On Monday, July 3, 2017 at 8:37:42 PM UTC+8, Hermógenes Oliveira wrote:
>
> Rodrigo Freire  escreveu: 
>
> > 
> > [...] 
> > 
> > O vocabulário da teoria de grupos é exclusivamente matemático, e os 
> > axiomas são tomados como determinantes exaustivos das noções 
> > matemáticas envolvidas (operação de grupo), muito mais que no caso 
> > da aritmética. 
>
> Não sei se compreendi muito bem a analogia. 
>
> Normalmente, a noção de grupo é definida como *uma* operação sob um 
> conjunto de elementos que satisfazem determinados axiomas.  Porém, 
> diversas operações *distintas* satisfazem os axiomas de grupo.  Em que 
> sentido poderíamos dizer que os axiomas determinam exaustivamente a 
> operação? 
>
> Em contraste, você conseguiria ver como os axiomas de AP determinariam 
> exaustivamente (ou pelo menos, possuem a pretensão de determinar 
> exaustivamente) a noção de número natural? 
>
>
> -- 
> Hermógenes Oliveira 
>
>

-- 
Você está recebendo esta mensagem porque se inscreveu 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+unsubscr...@dimap.ufrn.br.
Para postar neste grupo, envie um e-mail para logica-l@dimap.ufrn.br.
Visite este grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
Para ver esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/9d73231d-c6f5-4812-842c-e3d47fc91c1b%40dimap.ufrn.br.

Re: [Logica-l] SBL: nova diretoria

2017-07-03 Por tôpico Gisele Secco 
Prezados colegas, saudações

Parabenizo a nova diretoria e me coloco à disposição para colaborar,
especialmente no que diz respeito a iniciativas envolvendo o ensino de
lógica na graduação e no ensino médio, e ao estímulo à igualdade de gênero
na área.

Temos realizado singelas ações de ensino, pesquisa e extensão acerca desses
tópicos na UFRGS, e tenho notícia de colegas de outras instituições
concernidos com os mesmos.

Cordialmente,


2017-07-01 11:41 GMT-03:00 :

> Prezadas colegas, prezados colegas,
>
> como vocês devem saber, durante o XVIII Encontro Brasileiro de Lógica em
> Pirenópolis, em maio, a Sociedade Brasileira de Lógica (SBL) realizou a
> eleição de uma nova diretoria, que somos nós, a saber:
>
> Presidente: Cezar Augusto Mortari (Universidade Federal de Santa Catarina
> - filosofia)
> 1o Vice-Presidente: Juliana Bueno-Soler (Universidade Estadual de Campinas
> - filosofia)
> 2o Vice-Presidente: Samuel Gomes da Silva (Universidade Federal da Bahia -
> matemática)
> Tesoureiro: Cassiano Terra Rodrigues (Pontifícia Universidade Católica de
> São Paulo - filosofia)
> 1o Secretário: Bruno Lopes (Universidade Federal Fluminense - computação)
> 2o Secretário: Cláudia Nalon (Universidade de Brasília - computação)
>
> Conforme decisão da assembléia que nos elegeu, estamos assumindo hoje,
> primeiro de julho, a direção. Listamos a seguir, de maneira bem breve,
> alguns dos pontos sobre os quais pretendemos trabalhar para a melhoria da
> SBL:
>
> * atualizar o Estatuto da SBL visando obter o registro da associação e
> conta bancária próprios;
>
> * reformular e manter atualizada a página da SBL, registrando um domínio
> próprio;
>
> * voltar a editar boletins com informações de interesse dos associados
> (eventos, publicações, concursos etc.) através de uma lista de email
> exclusiva para anúncios aos sócios;
>
> * além de incentivar a pesquisa, achamos que a SBL também deveria, a
> exemplo do que fazem outras associações, iniciar e estimular a discussão
> sobre lógica e educação (por exemplo, discutindo que conteúdos de lógica
> poderiam/deveriam ser ministrados em curso de graduação, ou mesmo no ensino
> médio, e estimulando produção bibliográfica a respeito disso; a página da
> SBL poderia conter um link para questões de ensino, com indicações sobre
> textos, softwares etc.);
>
> * estimular mais publicações na área de lógica (talvez seja interessante
> ter uma revista publicada pela SBL, que poderia incluir tanto trabalhos de
> pesquisa quanto sobre questões de ensino);
>
> * continuar estimulando a realização de eventos (o próximo EBL será em
> 2019 em João Pessoa);
>
> * construir e efetivar ações em prol da igualdade de gêneros (i.e.
> estimular a participação ​de mulheres na área, política já adotada pela ASL
> e outras associações das áreas acadêmicas e científicas).
>
> Estes são apenas alguns pontos, de caráter geral, que indicam a direção em
> que pretendemos trabalhar. Gostaríamos de aproveitar a oportunidade para
> dizer que estamos abertos a sugestões sobre o que mais a SBL poderia fazer.
> (Informaremos em breve um email para contatos.)
>
> Cordialmente,
>
> Cezar, Juliana, Samuel, Cassiano, Bruno e Cláudia
>
> --
> Você está recebendo esta mensagem porque se inscreveu 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+unsubscr...@dimap.ufrn.br.
> Para postar neste grupo, envie um e-mail para logica-l@dimap.ufrn.br.
> Visite este grupo em https://groups.google.com/a/di
> map.ufrn.br/group/logica-l/.
> Para ver esta discussão na web, acesse https://groups.google.com/a/di
> map.ufrn.br/d/msgid/logica-l/7065dc6401186ead5215eb0b9878c60
> 0%40cfh.ufsc.br.
>



-- 
Gisele Dalva Secco
UFRGS/Brasil

-- 
Você está recebendo esta mensagem porque se inscreveu 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+unsubscr...@dimap.ufrn.br.
Para postar neste grupo, envie um e-mail para logica-l@dimap.ufrn.br.
Visite este grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
Para ver esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CADjHNnrqBKw3ni5acMO4JM28f7pcZEGojqOBveqAYjZWdnr2%2Bw%40mail.gmail.com.

Re: [Logica-l] How do we construct the Gödel’s sentence in Martin-Löf type theory?

2017-07-03 Por tôpico Rodrigo Freire 


>> 
>> [...]
>> 
>> O vocabulário da teoria de grupos é exclusivamente matemático, e os
>> axiomas são tomados como determinantes exaustivos das noções
>> matemáticas envolvidas (operação de grupo), muito mais que no caso
>> da aritmética.
> 
> Não sei se compreendi muito bem a analogia.
> 
> Normalmente, a noção de grupo é definida como *uma* operação sob um
> conjunto de elementos que satisfazem determinados axiomas.  Porém,
> diversas operações *distintas* satisfazem os axiomas de grupo.  Em que
> sentido poderíamos dizer que os axiomas determinam exaustivamente a
> operação?
> 
> Em contraste, você  ver como os axiomas de AP determinariam
> exaustivamente (ou pelo menos, possuem a pretensão de determinar
> exaustivamente) a noção de número natural?
> 

Não. Não há um predicado para "número natural" que ocorre nos axiomas da 
aritmética, assim como não há predicado para "elemento de grupo" ou 
"permutação" na teoria de grupos. Alem disso, apelar para uma "noção de número 
natural" que aritmética pretende capturar já é introduzir um elemento semântico 
que vai além da sintaxe, justamente para avaliar a "limitação do formalismo".  
Não há diferença puramente formal entre o caso aritmético e o caso da teoria de 
grupos, o que trivializaria sim a relevância fundacional do teorema na ausência 
de algum elemento semântico (pois o caso da incompletude dos grupos é 
irrelevante). 





-- 
Você está recebendo esta mensagem porque se inscreveu 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+unsubscr...@dimap.ufrn.br.
Para postar neste grupo, envie um e-mail para logica-l@dimap.ufrn.br.
Visite este grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
Para ver esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/DA9AB450-7100-4A8A-B97D-3A785E303260%40gmail.com.

Re: [Logica-l] How do we construct the Gödel’s sentence in Martin-Löf type theory?

2017-07-03 Por tôpico Hermógenes Oliveira 

Rodrigo Freire  escreveu:



[...]

O vocabulário da teoria de grupos é exclusivamente matemático, e os
axiomas são tomados como determinantes exaustivos das noções
matemáticas envolvidas (operação de grupo), muito mais que no caso
da aritmética.


Não sei se compreendi muito bem a analogia.

Normalmente, a noção de grupo é definida como *uma* operação sob um
conjunto de elementos que satisfazem determinados axiomas.  Porém,
diversas operações *distintas* satisfazem os axiomas de grupo.  Em que
sentido poderíamos dizer que os axiomas determinam exaustivamente a
operação?

Em contraste, você conseguiria ver como os axiomas de AP determinariam
exaustivamente (ou pelo menos, possuem a pretensão de determinar
exaustivamente) a noção de número natural?


--
Hermógenes Oliveira

--
Você está recebendo esta mensagem porque se inscreveu 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+unsubscr...@dimap.ufrn.br.
Para postar neste grupo, envie um e-mail para logica-l@dimap.ufrn.br.
Visite este grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
Para ver esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/20170703143740.Horde.9xe98xEwRy44Xs6N4kGOSVa%40webmail.uni-tuebingen.de.

Re: [Logica-l] How do we construct the Gödel’s sentence in Martin-Löf type theory?

2017-07-03 Por tôpico Rodrigo Freire 
Ok, Hermógenes, então podemos focar na questão levantada.


>
> O problema é que só com essa "interpretação sintática do teorema" é
>> impossível distinguir o teorema de Godel de uma trivialidade
>> irrelevante como, por exemplo: Há uma sentença G da teoria de grupos
>> (suposta consistente) tal que G não é teorema e ~G também não. De
>> fato, sintaticamente, como sistemas formais sem algum tipo de
>> "interpretação semântica", a aritmética de Peano e a teoria de
>> grupos são o mesmo tipo de coisa. Onde estaria a diferença? De onde
>> viria a pretensão de completude da aritmética de Peano, e por que
>> isso estaria ausente na teoria de grupos, por exemplo?
>>
>
> O estado medíocre do meu atual conhecimento de álgebra não me permite
> comentar com precisão o exemplo que você citou.  Mas eu me interessei
> pelo exemplo e também planejo remediar a minha ignorância de álgebra,
> portanto referências pontuais são bem-vindas (pode enviar em privado).
>


Considere G a sentença 'para todos x e y, x.y=y.x'. Essa sentença é
indecidível na teoria de grupos, mas ninguém chama isso de teorema da
incompletude da teoria de grupos.


>
> O que posso comentar no momento, assumindo aqui que o exemplo
> algébrico não é essencial à questão, é que, no caso de sistemas como
> AP (aritmética de Peano), no qual o vocabulário é exclusivamente
> matemático e os axiomas são tomados como determinantes exaustivos das
> noções matemáticas envolvidas, haveria sim a pretensão de que o
> sistema formal possa decidir qualquer sentença matemática A por meio
> de uma derivação de A ou de uma refutação de A.


O vocabulário da teoria de grupos é exclusivamente matemático, e os axiomas
são tomados como determinantes exaustivos das noções matemáticas envolvidas
(operação de grupo), muito mais que no caso da aritmética. Ainda assim, não
há pretensão de completude.
Essa "leitura sintática" trivializa o teorema de Godel.

Abraço
Rodrigo

-- 
Você está recebendo esta mensagem porque se inscreveu 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+unsubscr...@dimap.ufrn.br.
Para postar neste grupo, envie um e-mail para logica-l@dimap.ufrn.br.
Visite este grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
Para ver esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAExWzULrYsHZ21azbX%3Ds6T%3DXXi_4ZZ%2Bwqx8xvr9%3DY%2BM_de1wFA%40mail.gmail.com.

[Logica-l] Generalizações dos Teoremas da Incompletude de Gödel

2017-07-03 Por tôpico jean-yves beziau 
Aproveito esta discussão sobre Gödel no MathOverflow
para ver se tem pessoas interessadas a escrever artigos sobre
generalizações dos teoremas da incompletude Gödel no espirito da lógica
universal,
i.e. examinar sistematicamente condições lógicas para estes teoremas.
Até agora ainda pouco foi feito nesta direção sobre estes teoremas, ou
outros.

Ja publicamos um primeiro volume de Logica Universalis sobre esta tematica
"Scope of Logic Theorems" no qual tem um artigo sobre o primeiro teorema do
Gödel
"The Scope of Gödel’s First Incompleteness Theorem"
https://link.springer.com/article/10.1007/s11787-014-0107-3

Agora estamos trabalhando num segundo volume, mais detalhos aqui:
http://www.logica-universalis.org/sissue

Saudações,
JYB

-- 
Você está recebendo esta mensagem porque se inscreveu 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+unsubscr...@dimap.ufrn.br.
Para postar neste grupo, envie um e-mail para logica-l@dimap.ufrn.br.
Visite este grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
Para ver esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAF2zFLD1KSFYGimu_bzcjqn9qWPb8x%2B0A-XF6Yr_x7VMB2Ta%2Bg%40mail.gmail.com.

Re: [Logica-l] How do we construct the Gödel’s sentence in Martin-Löf type theory?

2017-07-03 Por tôpico Hermógenes Oliveira 

Rodrigo Freire  escreveu:


Olá Hermógenes,


Olá, Rodrigo.


Imagino que a "interpretação sintática do teorema" para um sistema S
(digamos, para a aritmética de Peano) seja: há (construtivamente)
uma sentença G tal que se S é (omega-)consistente, então G não é
teorema e ~G não é teorema. É isso?


Sim.  Em linhas gerais, foi isso o que Gödel demonstrou em 1931, não?


O problema é que só com essa "interpretação sintática do teorema" é
impossível distinguir o teorema de Godel de uma trivialidade
irrelevante como, por exemplo: Há uma sentença G da teoria de grupos
(suposta consistente) tal que G não é teorema e ~G também não. De
fato, sintaticamente, como sistemas formais sem algum tipo de
"interpretação semântica", a aritmética de Peano e a teoria de
grupos são o mesmo tipo de coisa. Onde estaria a diferença? De onde
viria a pretensão de completude da aritmética de Peano, e por que
isso estaria ausente na teoria de grupos, por exemplo?


O estado medíocre do meu atual conhecimento de álgebra não me permite
comentar com precisão o exemplo que você citou.  Mas eu me interessei
pelo exemplo e também planejo remediar a minha ignorância de álgebra,
portanto referências pontuais são bem-vindas (pode enviar em privado).

O que posso comentar no momento, assumindo aqui que o exemplo
algébrico não é essencial à questão, é que, no caso de sistemas como
AP (aritmética de Peano), no qual o vocabulário é exclusivamente
matemático e os axiomas são tomados como determinantes exaustivos das
noções matemáticas envolvidas, haveria sim a pretensão de que o
sistema formal possa decidir qualquer sentença matemática A por meio
de uma derivação de A ou de uma refutação de A.

--
Hermógenes Oliveira

--
Você está recebendo esta mensagem porque se inscreveu 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+unsubscr...@dimap.ufrn.br.
Para postar neste grupo, envie um e-mail para logica-l@dimap.ufrn.br.
Visite este grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
Para ver esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/20170703111937.Horde.kV8xZb9MxZVutIIoGf1WlHp%40webmail.uni-tuebingen.de.

Re: [Logica-l] How do we construct the Gödel’s sentence in Martin-Löf type theory?

2017-07-03 Por tôpico Hermógenes Oliveira 

Anderson Nakano  escreveu:


Olá, Hermógenes. Muito obrigado pela resposta!


Por nada.


Uma pequena observação: nestes sistemas sem negação, não se trata
apenas de tratar a negação como conectivo derivado (def., p. ex., ¬A
≡ A → (1=0)), mas de banir toda e qualquer "suposição não
realizável" e, com isso, até mesmo o raciocínio hipotético (o "p →
q") da matemática. Isso porque, vai alegar, digamos, o Freudenthal,
uma suposição não realizada não é um "material construtivo" a partir
do qual se poderia partir.


Isso me parece exatamente a situação que temos no caso da lógica
mínima onde não temos o princípio ECQ (ex contradictione quodilibet)
que nos permitiria extrair conseqüências de "suposições não
realizáveis".

Em resumo, o enredo da minha sugestão seria o seguinte.

A negação clássica pode ser interpretada na lógica intuicionista por
meio da conhecida tradução de Gentzen-Gödel.  Porém, ainda resta o
princípio ECQ, característico da negação nos sistemais intuicionistas
usuais, mas que não é aceito por construtivistas como Freudenthal e
Griss.

Contudo, ECQ pode ser interpretado numa lógica mínima por meio da
disjunção.  Aqui, em termos gerais, traduzimos uma sentença A por A∨⊥.
Grosso modo, isto significa que, tendo em vista a regra de introdução
da disjunção, A pode ser obtido pelas vias mínimas normais *ou por
meio de ⊥*, simulando assim os raciocínios por ECQ.  Note que "⊥" não
precisa ser considerada uma constante lógica, mas pode ser uma
sentença refutável qualquer (de acordo com os axiomas aritméticos
subjacentes) como, por exemplo, 1=0.

É claro, resta saber ainda se os sistemas sem negação aos quais você
se refere permitem alguma noção de refutação, ou se há apenas a noção
de demonstração.  Isto é, resta saber se uma demostração de 1≠0
significa o mesmo que uma refutação de 1=0, ou se as noções de
igualdade e desigualdade (diferença) são *completamente independentes*
(i.e. não há nenhum axioma aritimético subjacente conectando, ou
contrastando, as duas noções, o que seria bastante estranho).

Enfim, ao que me parece, a aplicação dos resultados de Gödel a esses
sistemas sem negação dependeria mais da teoria aritmética subjacente
do que dos conectivos lógicos disponíveis.

Não estou certo se a minha sugestão estaria correta, mas, independente
disso, a questão que você levanta é bastante interessante.

--
Hermógenes Oliveira

--
Você está recebendo esta mensagem porque se inscreveu 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+unsubscr...@dimap.ufrn.br.
Para postar neste grupo, envie um e-mail para logica-l@dimap.ufrn.br.
Visite este grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
Para ver esta discussão na web, acesse 
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/20170703103849.Horde.z-lGP8nnk-5NA2nGOLAke_Q%40webmail.uni-tuebingen.de.