Anderson Nakano <andersonnak...@gmail.com> 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.
