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

2017-07-01 Por tôpico Famadoria 
A sentença original de Gödel é Pi_1. Se juntarmos à teoria original todas as 
sentenças verdadeiras Pi_1, não se ganha nada em termos de provabilidade. Mas 
se juntarmos todas as Pi_2 verdadeiras obtemos uma teoria não r.e. mas completa 
na aritmética. 

Kleene, que eu saiba, foi quem primeiro estudou essas outras sentenças. 

Sent from my iPhone

> On 30 Jun 2017, at 14:22, Bruno Bentzen  wrote:
> 
> Olá a todos,
>  
> Obrigado pelos excelentes comentários, também acho o assunto fascinante.
>  
> 1) Agradeço em particular ao Rodrigo por me apontar o equívoco. É possível 
> demonstrar sim construtivamente que sentença de Gödel é verdadeira, e não 
> apenas que ela não pode ser falsa. Se vale a informação, o que me levou a 
> sustentar o contrário anteriormente foi o seguinte: como sabemos, quando 
> assumimos que uma proposição A é falsa e chegamos a uma contradição, 
> construtivamente, apenas podemos provar que A não pode ser falsa. Mas isso, 
> claro, vale apenas em geral. Quando A := ¬P ocorre como uma negação, por 
> exemplo, podemos derivar A de volta através de  ¬¬A através da lei da tripla 
> negação de Brouwer. O descuido, então, esta em esquecer que sentença de Gödel 
> é, em essência, uma negação!
>  
> 2) As indagações do Anderson também são muito interessantes. Me pergunto, 
> contudo, se tais teorias formais da aritmética sem negação seriam capazes de 
> satisfazer os requerimentos dos teoremas da incompletude. Em particular, 
> verifica-se que a linguagem de tal teoria não é capaz de expressar todas as 
> relações numéricas decidíveis (por exemplo, R(x,y) := x ≠ y), quer dizer, o 
> conjunto de “verdades básicas de aritmética”  que a teoria pode demonstrar é 
> razoavelmente limitado.
>  
> 3) Acredito que esta seja essa a discussão na HoTT Cafe que o Fernando esteja 
> se referindo, “Can the judgement (A true) be made into a proposition?”
>  
> https://groups.google.com/d/msg/hott-cafe/jyD2Bhc5GWo/UEzjWj0wAwAJ
>  
> Abraços,
> Bruno
> 
> --
> Bruno Bentzen
> https://sites.google.com/site/bbentzena/
> 
>> On Thursday, June 29, 2017 at 7:53:09 PM UTC+8, Rodrigo Freire wrote:
>> Olá Bruno,
>> 
>> Parabéns para a Valeria e para você pela ótima participação. 
>> 
>> Como é sabido por nós, Martin Loef afirma que verdade não pode ser 
>> identificada com demonstrabilidade em um sistema específico devido ao 
>> teorema de Godel. Por isso a identificação dele seria: verdade é 
>> demonstrabilidade "em geral" (o que também não é claro que muda muita coisa, 
>> mas não esse o ponto da discussão). Ao que parece, ninguém duvida que 
>> qualquer sistema recursivamente enumerável razoavelmente forte pode ser 
>> diagonalizado para produzir uma sentença de Godel, mas um dos problemas 
>> seria como poderíamos dizer construtivamente que a sentença de Godel é 
>> verdadeira. 
>> 
>> A sentença de Godel pode ser canonicamente interpretada como a afirmação que 
>> uma determinada máquina de Turing (que busca uma demonstração da própria 
>> sentença de Godel) nunca para. Você menciona em um comentário que a sentença 
>> de Godel não pode ser dita verdadeira construtivamente, apenas podemos dizer 
>> que ela não é falsa. Usando a interpretação acima, construtivamente 
>> poderíamos dizer então que não é o caso que não é o caso que aquela máquina 
>> de turing não para. Mas isso não seria o mesmo que dizer que aquela máquina 
>> de Turing não para pela eliminação da tripla negação? E isso não é o mesmo 
>> que dizer que G é verdadeira?
>> 
>> Abraço
>> Rodrigo
>> 
>> 
>> 
>> Enviado do meu iPhone
>> 
>>> Em 29 de jun de 2017, às 07:01, Bruno Bentzen  
>>> escreveu:
>>> 
>>> Olá pessoal,
>>> 
>>> Venho acompanhando a thread "How do we construct the Gödel’s sentence in 
>>> Martin-Löf type theory?" no MathOverflow 
>>> 
>>> https://mathoverflow.net/q/272982/58734
>>> 
>>> que tem sido bem popular desde os últimos dias (e contado com a 
>>> participação da Valéria e do Dana Scott).
>>> 
>>> Penso que talvez a discussão seja de interesse para alguns dos colegas da 
>>> lista.
>>> 
>>> Abraços,
>>> Bruno
>>> 
>>> --
>>> Bruno Bentzen
>>> https://sites.google.com/site/bbentzena/
>>> -- 
>>> 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/c155c92b-0bce-4012-aa97-6b79c44e769d%40dimap.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+unsubscr...@dimap.ufrn.br.
> Para postar

[Logica-l] SBL: nova diretoria

2017-07-01 Por tôpico cmortari 

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/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/7065dc6401186ead5215eb0b9878c600%40cfh.ufsc.br.