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 Em qui., 10 de fev. de 2022 às 11:23, Regivan Hugo Nunes Santiago < regivan.santi...@gmail.com> escreveu: > 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 -- Marcelo Finger Departament of Computer Science, IME-USP http://www.ime.usp.br/~mfinger ORCID: https://orcid.org/0000-0002-1391-1175 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 -- 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/CAGG7Aw1-OSN3c4_QVtHZ5XgqxjBfv7MFWtec9UCA05A_3LEqWw%40mail.gmail.com.
