Muitíssimo obrigado, Walter. Acabei de dar uma olhada no Troelstra & van Dalen. Pelo que pude ver, a completude é provada em relação a uma semântica com domínios variáveis, mas sem identidade. Porém, eles indicam brevemente nas seções 5.11 e 5.12 como lidar com a identidade.
> Quando eu morava na Alemanha em Muenster perto da Holanda, o grupo de lá > visitava muitas vezes o grupo de Amsterdam. > > Lembro-me que o Anne Troelstra dizia que ainda nao havia prova intuicionista > da lógica intuicionista. > > Discutiamos que a logica intuicionista tinha mais sorte...nao faz sentido uma > prova paraconsistentista da logica paraconsistente. > > Falei tambem com van Dalen e Dick de Jong, tempos saudosos... Fico feliz que a minha pergunta tenha trazido boas lembraças :). Forte abraço -- Henrique Antunes On Thu, Sep 29, 2022 at 02:03:05PM -0300, Walter Carnielli wrote: > Ola Henrique > > no livro do Trelstra & van Dalen tem uma prova de completude da lógica > intuicionista de primeira ordem, não sei se com domínios variáveis .Acho que > sim. > > > Aqui tem um paper mais recente com uma prova *intuicionista*da completude: > > [1]https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/ > abs/an-intuitiomstic-completeness-theorem-for-intuitionistic-predicate-logic1/ > 17F2EF19C8BA9421A80CC6154749A4B4 > > > Quando eu morava na Alemanha em Muenster perto da Holanda, o grupo de lá > visitava muitas vezes o grupo de Amsterdam. > > Lembro-me que o Anne Troelstra dizia que ainda nao havia prova intuicionista > da lógica intuicionista. > > Discutiamos que a logica intuicionista tinha mais sorte...nao faz sentido uma > prova paraconsistentista da logica paraconsistente. > > Falei tambem com van Dalen e Dick de Jong, tempos saudosos... > > > Abs > > > > > Em qui., 29 de set. de 2022 12:52, Henrique Antunes <[2] > antunes.henri...@outlook.com> escreveu: > > Prezad@s, > > Boa tarde. > > Estou buscando referências que contenham a prova de completude da lógica > intuicionista de primeira ordem com identidade em relação a uma > semântica com domínios variáveis. Vocês saberiam aonde eu poderia > encontrar? > > Abraços e obrigado > > -- > Henrique Antunes > > > -- > LOGICA-L > Lista acadêmica brasileira dos profissionais e estudantes da área de > Lógica > <[3]logica-l@dimap.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 [4]logica-l+unsubscr...@dimap.ufrn.br. > Para ver esta discussão na web, acesse [5]https://groups.google.com/a/ > dimap.ufrn.br/d/msgid/logica-l/ > > SJ0PR07MB939734A33E48CBE741B9BEE19D579%40SJ0PR07MB9397.namprd07.prod.outlook.com > . > > > References: > > [1] > https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/abs/an-intuitiomstic-completeness-theorem-for-intuitionistic-predicate-logic1/17F2EF19C8BA9421A80CC6154749A4B4 > [2] mailto:antunes.henri...@outlook.com > [3] mailto:logica-l@dimap.ufrn.br > [4] mailto:logica-l%2bunsubscr...@dimap.ufrn.br > [5] > https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/SJ0PR07MB939734A33E48CBE741B9BEE19D579%40SJ0PR07MB9397.namprd07.prod.outlook.com -- LOGICA-L Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica <logica-l@dimap.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 ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/SJ0PR07MB9397A67F626838C4E85925B79D579%40SJ0PR07MB9397.namprd07.prod.outlook.com.
