Demonstrações e Curry-Howard
30 views
Skip to first unread message
Regivan Hugo Nunes Santiago
Feb 10, 2022, 8:57:03 AM2/10/22
to Lista acadêmica brasileira dos profissionais e estudantes da área de LOGICA, Regivan Hugo Nunes Santiago
Caros colegas,
tenho a seguinte dúvida:
Imaginem que vocês solicitem a alguém para demonstrar A (digamos uma propriedade de grupos). Essa pessoa assume A, por inexperiência, e demonstra A sem usar A (usando propriedades mais básicas).
Como vocês veriam essa demonstração? Aceitariam?
Para mim a resposta é óbvia, mas o que vocês acham?
Do meu ponto de vista, isso seria equivalente a fazer um programa que não fosse um programa mínimo (com variáveis que não foram usada nas linhas de código do programa) e levando em consideração o isomorfismo de Curry-Howard e a equivalência de programas do ponto de vista de funções (fazem a mesma coisa) a demonstração seria equivalente a que não usa a hipótese A.
Agora, essa minha argumentação a favor da demonstração só vale por causa do isomorfismo. O que vocês acham? Você conhecem alguma situação (sem o isomorfismo) em que isso não fosse aceito?
Abração,
Regivan
tenho a seguinte dúvida:
Imaginem que vocês solicitem a alguém para demonstrar A (digamos uma propriedade de grupos). Essa pessoa assume A, por inexperiência, e demonstra A sem usar A (usando propriedades mais básicas).
Como vocês veriam essa demonstração? Aceitariam?
Para mim a resposta é óbvia, mas o que vocês acham?
Do meu ponto de vista, isso seria equivalente a fazer um programa que não fosse um programa mínimo (com variáveis que não foram usada nas linhas de código do programa) e levando em consideração o isomorfismo de Curry-Howard e a equivalência de programas do ponto de vista de funções (fazem a mesma coisa) a demonstração seria equivalente a que não usa a hipótese A.
Agora, essa minha argumentação a favor da demonstração só vale por causa do isomorfismo. O que vocês acham? Você conhecem alguma situação (sem o isomorfismo) em que isso não fosse aceito?
Abração,
Regivan
Marcelo Finger
Feb 10, 2022, 9:00:56 AM2/10/22
to Regivan Hugo Nunes Santiago, Lista acadêmica brasileira dos profissionais e estudantes da área de LOGICA
Olá Regivan.
Numa lógica relevante a sua demonstração seria rejeitada. Idem numa lógica linear. Ou seja, a monotonicidade parece ser um requisito para aceitar a sua demonstração.
[]s
--
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/8BA61D98-8EB2-4E9C-8FE7-4AC343AD58C4%40gmail.com.
ORCID: https://orcid.org/0000-0002-1391-1175
ResearcherID: A-4670-2009
ResearcherID: A-4670-2009
Instituto de Matemática e Estatística,
Universidade de São Paulo
Rua do Matão, 1010 - CEP 05508-090 - São Paulo, SP
Regivan Hugo Nunes Santiago
Feb 10, 2022, 9:24:00 AM2/10/22
to Marcelo Finger, Lista acadêmica brasileira dos profissionais e estudantes da área de LOGICA
Obrigado Marcelo.
Eu não sei se captei o seu ponto.
Você está me dizendo que eu posso definir uma equivalência entre demonstrações apenas com a monotonicidade? É isso?
Eu não havia pensado nisso, mas parece razoável, pois significaria remover as hipóteses não utilizadas e chegar a mesma conclusão, o que livraria o apelo a Curry-Howard.
É isso?
Regivan
Eu não sei se captei o seu ponto.
Você está me dizendo que eu posso definir uma equivalência entre demonstrações apenas com a monotonicidade? É isso?
Eu não havia pensado nisso, mas parece razoável, pois significaria remover as hipóteses não utilizadas e chegar a mesma conclusão, o que livraria o apelo a Curry-Howard.
É isso?
Regivan
Elaine Pimentel
Feb 10, 2022, 9:30:45 AM2/10/22
to Regivan Hugo Nunes Santiago, Marcelo Finger, Lista acadêmica brasileira dos profissionais e estudantes da área de LOGICA
Oi, Regivan,
Do lado completamente "proof-theoretical", o que você está descrevendo se chama "weakening" -- você descarta uma hipótese (com uma leitura bottom-up). O que o Marcelo está dizendo é que nem todo sistema lógico permite esse procedimento (como as lógicas relevantes).
No caso de teoremas em Matemática, a gente usa a lógica clássica (ou intuicionista se você vai falar de CH para "programas"), onde weakening é perfeitamente admissível.
Abraços,
--
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/9D96C6DD-9EE4-437C-BAAC-A636384D3F1E%40gmail.com.
Elaine.
-----------------------------------
Elaine Pimentel
-----------------------------------
Marcelo Finger
Feb 10, 2022, 9:31:56 AM2/10/22
to Regivan Hugo Nunes Santiago, Lista acadêmica brasileira dos profissionais e estudantes da área de LOGICA
Oi Regivan,
O que eu quis dizer é que mudando-se a lógica subjacente, algumas provas deixam de ser aceitáveis. Ou seja, a sua demonstração poderia ser aceita numa lógica clássica ou intuicionista, que aceitam a regra da monotonicidade como uma regra de inferência válida. Desta forma pode-se adicionar premissas sem prejudicar a validade da inferência. O mesmo não ocorre com lógicas não monotônicas, como as lógicas relevantes e linear.
[]s
Regivan Hugo Nunes Santiago
Feb 10, 2022, 9:44:36 AM2/10/22
to Marcelo Finger, Lista acadêmica brasileira dos profissionais e estudantes da área de LOGICA
Eu entendi Marcelo e Elaine,
obrigado.
Regivan
obrigado.
Regivan
Reply all
Reply to author
Forward
0 new messages