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

[Marcelo Finger]

Caros.

Quando o Kripke esteve na Unicamp há alguns anos, acho que ele
apresentou um esboço desta prova.  SE não me engano, naquela época p
único escrito sobre isso era um relatório de outro pesquisador sobre a
prova de Kripke.  Ele começava contando o que se sabia sobre o assunto
ANTES de Goedel.

Alguém mais se lembra disso?

[]s

2017-07-03 22:42 GMT-03:00 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ê 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-2VBAoYxTAtVz9NOBUe8uQ77Yuxe30tR-wKiqQkYX1asg%40mail.gmail.com.



-- 
 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/CABqmzx24iiZ118OKTqJHE6o935EEcju4ZTz_JnXL5qGN%2BApRGA%40mail.gmail.com.

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

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

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

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

[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] How do we construct the Gödel’s sentence in Martin-Löf type theory?

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

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

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

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

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

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

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

[Rodrigo Freire]

Olá Hermógenes,


> A interpretação sintática do teorema permanece inalterada.
>
> Na minha hulmide opinião, interpretações semâmticas do teorema, que
> apelam a noções semânticas como "verdade" ou alguma noção semântica de
> "negação", *não fazem o menor sentido*.  Mesmo no caso clássico.

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?

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?


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%2B%3Dbt8W743zAG0PEcYBZ9s3Yc_P92sdE9hmYkszRMVTYQ%40mail.gmail.com.

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

[Anderson Nakano]

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

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.

Além disso, salvo engano, nesses sistemas (chamemos de NA) não faz muito 
sentido a noção de ω-inconsistência (separada da de inconsistência), pois é 
possível provar que, se NA ⊢ ∃xA(x), então, para algum numeral n, NA ⊢ A(n).




-- 
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/545d6474-5036-48c2-9e50-63fd689b4b7a%40dimap.ufrn.br.

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

[Hermógenes Oliveira]

Anderson Nakano  escreveu:

> Boa tarde, pessoal. 

Olá, Anderson.

>
> [...]
>
> 1. Como o primeiro teorema da incompletude poderia ser construído em
> sistemas formais da aritmética sem negação? Refiro-me, em particular,
> ao sistema introduzido por Krivtsov em "A Negationless Interpretation
> of Intuitionistic Axiomatic Theories".

Não conheço o sistema de Krivtsov, mas gostaria de observar o seguinte.

A demonstração de Gödel não depende de nenhuma noção semântica, seja a
noção *semântica* de "negação" ou "verdade".

Dado que a lógica clássica pode ser interpretada na lógica mínima[#],
via lógica intuicionista, imagino que não seria difícil ajustar a noção
Gödeliana de representabilidade à um sistema "sem negação", por exemplo,
à um sistema no qual ¬A ≡ A → (1=0), com a noção de igualdade e
desigualdade (diferença) determinada por axiomas construtivos
adicionais.

Desde que o sistema formal em questão seja poderoso o suficiente para
representar sua própria sintaxe, é possivel diagonalizar e obtair daí
uma sentença indecidível.

Algo similar acontece com o teorema de Church: a tradução da lógica
clássica na lógica intuicionista é comumente usada para transferir o
resultado de indecidibilidade da lógica clássica de primeira ordem para
o caso intuicionista.

>
> [...]
>
> 3. Além disso, a prova do primeiro teorema demonstra a
> indecidibilidade da sentença G levando a hipótese da decidibilidade
> (seja de G ou de ¬G) a uma contradição. Para um intuicionista que não
> aceita que a refutação (P → ⊥) seja de fato o sentido da negação na
> matemática (penso na linha de Freudenthal, Griss, ...) e que vão
> trabalhar com axiomas para a relação de diferença (no lugar da
> negação), não me é claro qual seria a interpretação correta do teorema
> neste caso.

A interpretação sintática do teorema permanece inalterada.

Na minha hulmide opinião, interpretações semâmticas do teorema, que
apelam a noções semânticas como "verdade" ou alguma noção semântica de
"negação", *não fazem o menor sentido*.  Mesmo no caso clássico.

Nota:

[#] Interpretações da lógica clássica na lógica intuicionista e mínima
foram exploradas por Kolmogorov, Bernays, Gentzen e Gödel, dentre
outros.  Um apanhado geral dos resultados e traduções pode ser
encontrado em: D. Prawitz and P. E. Malmnäs. A survey of some
connections between classical, intuitionistic and minimal logic. In
H. Arnold Schmidt, K. Schütte, and H. J. Thiele, editors, Contributions
to Mathematical Logic, Proceedings of the Logic Colloquium, Hannover
1966, pages 215-229. North-Holland Publishing Company, 1968.

-- 
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/878tk7te6a.fsf_-_%40camelot.oliveira.

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

[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 

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

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

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

[Francisco Antonio Doria]

Posso fazer uma observação?

Para teorias S com um conjunto recursivamente enumerável de teoremas (e
mais outras condições simples, tipo ``aritmética suficiente'') existem
infinidades de sentenças indecidíveis. E todas,  se o desejarmos, com
significado matemático sensato. Um exemplo (em ZFC, suposto consistente e
sound) de que gosto muito: podemos escrever as tábuas de um conjunto
infinito X de máquinas de Turing tais que a sentença ``X é um conjunto de
máquinas de Turing polinomiais no tempo'' é indecidível em tal ZFC. E é
óbvio que esse conjunto só tem máquinas polinomiais.

Ah, essa sentença não é Pi^0_1.

Estamos agora catando uma sentença indecidivel em todos esses sistemas S.
Simples e com significado matemático óbvio.

2017-06-29 10:58 GMT-03:00 Fernando Yamauti :

>  Olá a todos,
>
>   Primeiramente, só queria levantar dois pontos.
>
>  1) Eu, como havia comentado aqui ou na HoTT Café (não me lembro ao
> certo), também achava que \neg \neg G somente poderia ser considerada
> verdadeira, mas fui chamado a atenção (pelo Matt Oliveri) de que G já é
> construtivamente verdadeira: uma prova de G leva a uma contradição e,
> portanto, G não é provável é verdadeiro, logo G é verdadeiro.
>
>  2) Com relação ao comentário do Rodrigo, a melhor definição de verdade no
> intuicionismo que achei até agora é a dada por realizações através funções
> parciais recursivas, a realização de Kleene (uma exposição breve usando
> lambda termos não tipados, https://www.fing.edu.
> uy/~amiquel/intro-kleene.pdf) ou, mais geralmente, as meaning
> explanations do ML (http://www.cs.tufts.edu/~nr/c
> s257/archive/per-martin-lof/constructive-math.pdf), que nunca foi escrita
> formalmente até onde eu saiba. Lembrando, funções parciais recursivas,
> lambda termos (untyped) e máquinas de Turing são a mesma coisa. Nesse caso,
> qualquer \PI_1^0 fórmula é trivialmente verdadeira. Em particular, G é
> canonicamente verdadeira. Como G é verdadeira, \neg Prov (G) é verdadeira.
> Isso significa exatamente que qualquer máquina de Turing não realiza Prov
> (G).
>
>
>  Agora, com relação a questão em geral. Para enunciar e provar a
> incompletude parece mais fácil provar na categoria sintática. Existe um
> argumento do Lawvere de diagonalização e e uma prova da indefinibildade da
> verdade (no caso Booleano) para categorias cartesianas fechadas (
> http://tac.mta.ca/tac/reprints/articles/15/tr15.pdf). Acho que essa foi a
> sugestão pelo comentário dos pretopos aritméticos. Mas vale notar que mesmo
> um topos elementar com números naturais não tem todos os tipos indutivos
> (ele não precisa ter todas as algebras livres sobre uma teoria algébrica
> infinitaria), então acho que um pretopos aritmético ainda é insuficiente
> para um enunciado geral. Também existiriam mais problemas para o caso
> intensional (por exemplo, deixar tudo fibrante  e requerir quocientes
> homotópicos e blá, blá , blá...)
>
>   Abs.,
>
>   Fernando
>
>
>
> Em 29 de junho de 2017 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+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/di
>> map.ufrn.br/group/logica-l/.
>> Para ver essa discussão na Web, acesse https://groups.google.com/a/di
>> map.ufrn.br/d/msgid/logica-l/c155c92b-0bce-4012-aa97-6b79c4
>> 4e769d%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 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-2_Lvk%2BxNXTi5a7vx4L_
> hK-4D_Z%3DyypkKJ%2BRUA3%2BfNp5w%40mail.gmail.com
> 
> .
>

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

[Fernando Yamauti]

 Olá a todos,

  Primeiramente, só queria levantar dois pontos.

 1) Eu, como havia comentado aqui ou na HoTT Café (não me lembro ao certo),
também achava que \neg \neg G somente poderia ser considerada verdadeira,
mas fui chamado a atenção (pelo Matt Oliveri) de que G já é
construtivamente verdadeira: uma prova de G leva a uma contradição e,
portanto, G não é provável é verdadeiro, logo G é verdadeiro.

 2) Com relação ao comentário do Rodrigo, a melhor definição de verdade no
intuicionismo que achei até agora é a dada por realizações através funções
parciais recursivas, a realização de Kleene (uma exposição breve usando
lambda termos não tipados, https://www.fing.edu.uy/~amiquel/intro-kleene.pdf)
ou, mais geralmente, as meaning explanations do ML (
http://www.cs.tufts.edu/~nr/cs257/archive/per-martin-lof/co
nstructive-math.pdf), que nunca foi escrita formalmente até onde eu saiba.
Lembrando, funções parciais recursivas, lambda termos (untyped) e máquinas
de Turing são a mesma coisa. Nesse caso, qualquer \PI_1^0 fórmula é
trivialmente verdadeira. Em particular, G é canonicamente verdadeira. Como
G é verdadeira, \neg Prov (G) é verdadeira. Isso significa exatamente que
qualquer máquina de Turing não realiza Prov (G).


 Agora, com relação a questão em geral. Para enunciar e provar a
incompletude parece mais fácil provar na categoria sintática. Existe um
argumento do Lawvere de diagonalização e e uma prova da indefinibildade da
verdade (no caso Booleano) para categorias cartesianas fechadas (
http://tac.mta.ca/tac/reprints/articles/15/tr15.pdf). Acho que essa foi a
sugestão pelo comentário dos pretopos aritméticos. Mas vale notar que mesmo
um topos elementar com números naturais não tem todos os tipos indutivos
(ele não precisa ter todas as algebras livres sobre uma teoria algébrica
infinitaria), então acho que um pretopos aritmético ainda é insuficiente
para um enunciado geral. Também existiriam mais problemas para o caso
intensional (por exemplo, deixar tudo fibrante  e requerir quocientes
homotópicos e blá, blá , blá...)

  Abs.,

  Fernando



Em 29 de junho de 2017 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+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/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/CAJGvw-2_Lvk%2BxNXTi5a7vx4L_hK-4D_Z%3DyypkKJ%2BRUA3%2BfNp5w%40mail.gmail.com.

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

[Rodrigo Freire]

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+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/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/96E74213-D3E9-4EC8-8CB3-24DF32BE3F61%40gmail.com.