Re: [Logica-l] Texto na área do Direito com termos lógicos

2017-06-30 Por tôpico Marcelo Finger 
2017-06-23 18:18 GMT-03:00 Joao Marcos :
> (ali descobri que a sigla IME pode ter um significado bem diferente do
> que eu imaginava)

Eu considero esta nova acepção um elogio!

[]s


-- 
 Marcelo Finger
 Departament of Computer Science, IME
 University of Sao Paulo
 http://www.ime.usp.br/~mfinger

-- 
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/CABqmzx3ZkJjokyTyUBAJ2hba90aL0zgxJU18%3DPyZHksw4kRmLQ%40mail.gmail.com.

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

2017-06-30 Por tôpico Bruno Bentzen 
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ê 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/23459f67-99f7-42db-85b9-87198d98e2ed%40dimap.ufrn.br.