Referência sobre lógica intuicionista de primeira ordem
Henrique Antunes
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
Walter Carnielli
--
LOGICA-L
Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica <logi...@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+u...@dimap.ufrn.br.
Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/SJ0PR07MB939734A33E48CBE741B9BEE19D579%40SJ0PR07MB9397.namprd07.prod.outlook.com.
Henrique Antunes
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...
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:
>
> 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
>
>
>
>
>
> 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
> 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
> 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....@outlook.com
> [3] mailto:logi...@dimap.ufrn.br
> [4] mailto:logica-l%2Bunsu...@dimap.ufrn.br
> [5] https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/SJ0PR07MB939734A33E48CBE741B9BEE19D579%40SJ0PR07MB9397.namprd07.prod.outlook.com
Hermógenes Oliveira
> Aqui tem um paper mais recente com uma prova *intuicionista*da completude:
>
> 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.
De fato, não creio que esta demonstração tenha muita aceitação, mesmo dentre o grupo em Nijmengen. O artigo é de 1976. Não diria que é "recente". Nele, o próprio autor escreve "Of course the question arises whether we can claim to have found a reasonable semantics of intuitionistic logic; i.e. if the construction gives us a clearer concept "intuitionistically true sentence". I would not say so. Rather, the construction looks like a technical device, which should work for a big class of formal systems". Um diagnóstico similar foi dado por Dummett (The Logical Basis of Metaphysics, a partir da página 152; Elements of Intuitionism, seção 5.7). Realmente, qualquer pessoa que esteja perdendo o sono com o uso de raciocínio estritamente clássico na demonstração de Kripke certamente não passará a dormir tranquilamente com este resultado.
> Discutiamos que a logica intuicionista tinha mais sorte...nao faz sentido uma prova paraconsistentista da logica paraconsistente.
Ora, por que não faria sentido? Demonstrações de completude não costumam lançar mão da explosão. Claro, elementos ideológicos suscitam certa insatisfação por parte de algumas pessoas com o uso de raciocínio clássico na demonstração de completude na semântica de Kripke para a lógica intuicionista. Realmente, nunca ouvi falar de inquietações similares entre pessoas que lidam com lógica paraconsistente.
--
Hermógenes Oliveira
Walter Carnielli
>>Ora, por que não faria sentido? Demonstrações de completude não costumam lançar mão da explosão.
filosófica recorrente. Nada em matemática, que eu conheça (dê-me um
exemplo que me corrija por favor!) usa a explosão. Explosão é para
*não* ser usada! Provas de completude usam, sim, redução ao absurdo,
que suscitam alguma inquietação nos paraconsistentistas, mas isso
vale nas lógicas. paraconsistentes usuais. Contudo, noções
metamatemáticas continuam clássicas -ninguém fala de uma função que
às vezes deixa de ser unívoca , ou de teoremas que se demonstrem e
não se demonstrem.
>>Claro, elementos ideológicos suscitam certa insatisfação por parte de algumas pessoas com o uso de raciocínio clássico na >>demonstração de completude na semântica de Kripke para a lógica intuicionista. Realmente, nunca ouvi falar de inquietações similares >>entre pessoas que lidam com lógica paraconsistente
Abs
Walter
Em sex., 30 de set. de 2022 às 10:11, Hermógenes Oliveira
<oliv...@daad-alumni.de> escreveu:
> LOGICA-L
> Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica <logi...@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+u...@dimap.ufrn.br.
--
========================
Walter Carnielli
Laboratory for Applied Ontology (LOA), ISTC-CNR
Trento, Italy
http://www.loa.istc.cnr.it
and
CLE and Department of Philosophy
University of Campinas –UNICAMP, Brazil
https://waltercarnielli.com/
Joao Marcos
>
> Não é bem que "não faça sentndo", é que não é uma preocupação
> filosófica recorrente. Nada em matemática, que eu conheça (dê-me um
> exemplo que me corrija por favor!) usa a explosão.
junho deste ano:
https://cs.nyu.edu/pipermail/fom/2022-May/thread.html
https://cs.nyu.edu/pipermail/fom/2022-June/thread.html
Alguns exemplos bastante básicos (nível "semana 1" de um curso de
Teoria de Conjuntos) foram propostos por Harvey Friedman, em
particular, em:
https://cs.nyu.edu/pipermail/fom/2022-May/023318.html
(sugiro conferir também a resposta do Arnon Avron em
https://cs.nyu.edu/pipermail/fom/2022-May/023328.html)
> Explosão é para
> *não* ser usada! Provas de completude usam, sim, redução ao absurdo,
> que suscitam alguma inquietação nos paraconsistentistas, mas isso
> vale nas lógicas. paraconsistentes usuais.
digamos, não podem ser válidas em lógicas paraconsistentes, certo?
Poderia fazer perfeito sentido buscar por demonstrações de completude
que não façam uso de estratégias baseadas nestes princípios, não?
> Contudo, noções
> metamatemáticas continuam clássicas -ninguém fala de uma função que
> às vezes deixa de ser unívoca , ou de teoremas que se demonstrem e
> não se demonstrem.
matemáticas na forma A e não-A, pode ocorrer de não podermos produzir
uma *demonstração* de nenhuma das duas (uma asserção bastante óbvia,
se a teoria na qual esta demonstração deva ser construída simplesmente
não tiver recursos dedutivos suficientes para demonstrar muita coisa).
O que haveria de errado em imaginar que o paraconsistentista defenda
(por razões similares às anteriores) que há situações em que não
podemos produzir uma *refutação* de nenhuma destas sentenças? (a
explosão implica que pelo menos uma destas duas sentenças deve ser
refutável)
Joao Marcos
--
http://sequiturquodlibet.googlepages.com/
Hermógenes Oliveira
> Vale notar que este assunto foi discutido na lista FOM entre maio e
> junho deste ano:
> https://cs.nyu.edu/pipermail/fom/2022-May/thread.html
> https://cs.nyu.edu/pipermail/fom/2022-June/thread.html
> Alguns exemplos bastante básicos (nível "semana 1" de um curso de
> Teoria de Conjuntos) foram propostos por Harvey Friedman, em
> particular, em:
> https://cs.nyu.edu/pipermail/fom/2022-May/023318.html
> (sugiro conferir também a resposta do Arnon Avron em
> https://cs.nyu.edu/pipermail/fom/2022-May/023328.html)
Pois é. Também tinha em mente essa discussão, em particular a posição de Tennant de que a lógica mínima seria suficiente para a ampla maioria dos propósitos matemáticos e científicos.
O exemplo de Friedman está baseado na alegação de que a demonstração mais comum (aquela com a qual Friedman e a maioria dos matemáticos está familiarizado) da existência do conjunto vazio aparentemente apela para a explosão. Mas isto está longe de pacificar a questão: podem muito bem haver outras demonstrações. Ainda que não houvessem outras demonstrações, porém, seria legítimo perguntar até que ponto este teorema é indispensável. Em algumas axiomatizações, não é mesmo necessária (pois se trata de um axioma). Na verdade, parece ser relativamente inerte, no sentido de não afetar outras partes da matemática, a não ser no âmbito de certas combinações específicas de axiomatização + interpretação filosófica da teoria dos conjuntos.
Uma dificuldade saliente em toda discussão é identificar criteriosamente quando a explosão está de fato sendo usada. Avron, por exemplo, parece crer que o uso do silogismo disjuntivo é, por si, um uso da explosão. Outras pessoas provavelmente não consideram explosão, se o uso está restrito a contextos disjuntivos. Enfim, há certa liberdade na interpretação de demonstrações informais, de forma que é sempre possível declarar usos explícitos como meramente aparentes, ou fabricar usos essenciais que estariam implícitos, ou escondidos.
A minha tendência é concordar com Walter: Explosão é pra não ser usada.
> As formas usuais de redução ao absurdo e de silogismo disjuntivo,
> digamos, não podem ser válidas em lógicas paraconsistentes, certo?
> Poderia fazer perfeito sentido buscar por demonstrações de completude
> que não façam uso de estratégias baseadas nestes princípios, não?
>
> [...]
>
> Vamos assumir que o paracompletista defenda que, dadas duas sentenças
> matemáticas na forma A e não-A, pode ocorrer de não podermos produzir
> uma *demonstração* de nenhuma das duas (uma asserção bastante óbvia,
> se a teoria na qual esta demonstração deva ser construída simplesmente
> não tiver recursos dedutivos suficientes para demonstrar muita coisa).
> O que haveria de errado em imaginar que o paraconsistentista defenda
> (por razões similares às anteriores) que há situações em que não
> podemos produzir uma *refutação* de nenhuma destas sentenças? (a
> explosão implica que pelo menos uma destas duas sentenças deve ser
> refutável)
Questões interessantes que você levanta! Vou tomar um tempo para pensar a respeito.
--
Hermógenes Oliveira