Re: [Logica-l] sobre a "melhor forma" de apresentar a negação em lógicas construtivas

Olá, João Marcos! Joao Marcos escreveu: > > [...] > > Na lógica intuicionista a negação ¬A de uma sentença A é > frequentemente introduzida *por definição* como a sentença A→⊥, onde → > é a "implicação intuicionista" e ⊥ o "absurdo intuicionista", tomados > como conectivos

Re: [Logica-l] sobre a "melhor forma" de apresentar a negação em lógicas construtivas

Oi João Aqui vai uma opinião talvez muito simplista de um não-especialista. A propriedade meta-logica que me parece relevante para sua questão é a comutatividade com “é demonstrável que”. Em um contexto construtivo usual, conjunção, disjunção e implicação comutam com “é demonstrável que”.

Re: [Logica-l] sobre a "melhor forma" de apresentar a negação em lógicas construtivas

Oi João, respondendo só metade da sua pergunta, a metade mais fácil: na verdade, a bi-implicação na lógica clássica (e em varias outras) corresponde à soma no anel Booleano onde a conjunção é o produto. Dessa forma, fica claro porque a bi-implicação, sendo soma, é associativa,

[Logica-l] sobre a "melhor forma" de apresentar a negação em lógicas construtivas

PessoALL: Em axiomatizações da lógica clássica, a *bi-implicação* frequentemente é introduzida como uma mera abreviatura a partir, digamos, de fórmulas contendo conjunções e implicações, ou contendo conjunções, disjunções e negações, apropriadamente combinadas. Tal situação nem sempre é ideal,