sobre a "melhor forma" de apresentar a negação em lógicas construtivas
54 views
Skip to first unread message
Joao Marcos
May 17, 2018, 7:30:57 PM5/17/18
to Lista acadêmica brasileira dos profissionais e estudantes da área de LOGICA
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, mas não é inteiramente fora de propósito: se a bi-implicação é tomada como um conectivo primitivo, de fato, suas axiomatizações terão de dar conta de propriedades pouco intuitivas da bi-implicação clássica, tais como a associatividade deste conectivo (poder-se-ia argumentar neste caso que se trata de um mero "efeito colateral" do princípio da casa do pombo, tendo em vista a bivalência da lógica subjacente). Além disso, vale notar que tais definições alternativas não resistem ao enfraquecimento da lógica original, pois em fragmentos dedutivos da lógica clássica duas fórmulas classicamente equivalentes podem deixar de ser equivalentes, e passa assim a fazer diferença qual abreviatura é escolhida para introduzir o conectivo em questão.
Estendendo o exemplo propriamente para o domínio não-clássico, gostaria de colher reações dos especialistas aqui sobre o seguinte ponto.
Na lógica intuicionista a negação $\neg A$ de uma sentença $A$ é frequentemente introduzida *por definição* como a sentença $A\to\bot$, onde $\to$ é a "implicação intuicionista" e $\bot$ o "absurdo intuicionista", tomados como conectivos primitivos. Como consequência, ao enfraquecermos a implicação ou o absurdo, pela consideração de um fragmento dedutivo da lógica intuicionista, pode ocorrer que a interpretação de $\neg$ como algo que mereça o título de "negação" seja prejudicada.
Obviamente, para fragmentos da lógica intuicionista a abordagem supra-citada só faz sentido quando $\to$ e $\bot$ estão disponíveis. De todo modo, tendo em vista o fato de que os conectivos intuicionistas não são em geral interdefiníveis, não é inconcebível que a introdução de certos conectivos por meio de abreviaturas possa em certas situações ser conveniente, por alguma razão... embora isto possa também passar a impressão de que tais conectivos assim introduzidos "não existem de verdade".
A pergunta que lanço aqui é: ao trabalhar com *lógicas construtivas* (que sejam fragmentos da lógica clássica ou, digamos, de alguma extensão modal da lógica clássica), haverá alguma justificativa meta-lógica _razoável_ (em oposição a justificativas meramente ad hoc, formuladas convenientemente para "explicar" a teoria a posteriori) para considerarmos a negação como sendo preferencialmente introduzida por abreviatura, sempre que isto é possível? Situações em que tal abordagem pareceria não ser atraente, por exemplo, seriam aquelas em que a implicação e o bottom são suficientemente fortes para que a definição seja útil, mas a negação que se pretende introduzir é na realidade tanto paracompleta quanto paraconsistente (exemplo: lógica N4 de Nelson).
(A pergunta acima ---para a qual não há resposta certa ou errada--- é propositalmente vaga, de modo a tentar não tomar partido de nenhuma posição específica. Com alguma sorte, contudo, a pergunta estará suficientemente clara para que os colegas possam emitir suas *opiniões* a respeito do assunto!)
Abraços, JM
--
http://sequiturquodlibet.googlepages.com/
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, mas não é inteiramente fora de propósito: se a bi-implicação é tomada como um conectivo primitivo, de fato, suas axiomatizações terão de dar conta de propriedades pouco intuitivas da bi-implicação clássica, tais como a associatividade deste conectivo (poder-se-ia argumentar neste caso que se trata de um mero "efeito colateral" do princípio da casa do pombo, tendo em vista a bivalência da lógica subjacente). Além disso, vale notar que tais definições alternativas não resistem ao enfraquecimento da lógica original, pois em fragmentos dedutivos da lógica clássica duas fórmulas classicamente equivalentes podem deixar de ser equivalentes, e passa assim a fazer diferença qual abreviatura é escolhida para introduzir o conectivo em questão.
Estendendo o exemplo propriamente para o domínio não-clássico, gostaria de colher reações dos especialistas aqui sobre o seguinte ponto.
Na lógica intuicionista a negação $\neg A$ de uma sentença $A$ é frequentemente introduzida *por definição* como a sentença $A\to\bot$, onde $\to$ é a "implicação intuicionista" e $\bot$ o "absurdo intuicionista", tomados como conectivos primitivos. Como consequência, ao enfraquecermos a implicação ou o absurdo, pela consideração de um fragmento dedutivo da lógica intuicionista, pode ocorrer que a interpretação de $\neg$ como algo que mereça o título de "negação" seja prejudicada.
Obviamente, para fragmentos da lógica intuicionista a abordagem supra-citada só faz sentido quando $\to$ e $\bot$ estão disponíveis. De todo modo, tendo em vista o fato de que os conectivos intuicionistas não são em geral interdefiníveis, não é inconcebível que a introdução de certos conectivos por meio de abreviaturas possa em certas situações ser conveniente, por alguma razão... embora isto possa também passar a impressão de que tais conectivos assim introduzidos "não existem de verdade".
A pergunta que lanço aqui é: ao trabalhar com *lógicas construtivas* (que sejam fragmentos da lógica clássica ou, digamos, de alguma extensão modal da lógica clássica), haverá alguma justificativa meta-lógica _razoável_ (em oposição a justificativas meramente ad hoc, formuladas convenientemente para "explicar" a teoria a posteriori) para considerarmos a negação como sendo preferencialmente introduzida por abreviatura, sempre que isto é possível? Situações em que tal abordagem pareceria não ser atraente, por exemplo, seriam aquelas em que a implicação e o bottom são suficientemente fortes para que a definição seja útil, mas a negação que se pretende introduzir é na realidade tanto paracompleta quanto paraconsistente (exemplo: lógica N4 de Nelson).
(A pergunta acima ---para a qual não há resposta certa ou errada--- é propositalmente vaga, de modo a tentar não tomar partido de nenhuma posição específica. Com alguma sorte, contudo, a pergunta estará suficientemente clara para que os colegas possam emitir suas *opiniões* a respeito do assunto!)
Abraços, JM
--
http://sequiturquodlibet.googlepages.com/
Walter Carnielli
May 17, 2018, 8:48:57 PM5/17/18
to Lista dos Logicos Brasileiros
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, comutativa, tem elemento neutro (o top), etc. A
coisa se generaliza bem naturalmente para lógicas multivaloradas,
modais, etc. Tenho alguns artigos com diversos co-autores a esse
respeito, como vc talvez se lembre.
Essa é uma vantagem de se preferir anéis de polinômios em
detrimento de álgebras de Boole (ao menos acredito eu).
O resto da questão ainda não sei... e não sei se vou saber.
Abraços,
Walter
> --
> Você recebeu essa mensagem porque está inscrito 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 postar nesse grupo, envie um e-mail para logi...@dimap.ufrn.br.
> Acesse esse grupo em
> https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
> Para ver essa discussão na Web, acesse
> https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAO6j_LjFidFDHSaxFpJwYfhEf13gsoEG8g2YYi9iFtPVY2e9NQ%40mail.gmail.com.
--
-----------------------------------------------
Walter Carnielli
Centre for Logic, Epistemology and the History of Science and
Department of Philosophy
State University of Campinas –UNICAMP
13083-859 Campinas -SP, Brazil
http://www.cambridge.org/br/academic/subjects/philosophy/twentieth-century-philosophy/significance-new-logic?format=HB&isbn=9781107179028
Institutional e-mail: walter.c...@cle.unicamp.br
Website: http://www.cle.unicamp.br/prof/carnielli
CV Lattes : http://lattes.cnpq.br/1055555496835379
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, comutativa, tem elemento neutro (o top), etc. A
coisa se generaliza bem naturalmente para lógicas multivaloradas,
modais, etc. Tenho alguns artigos com diversos co-autores a esse
respeito, como vc talvez se lembre.
Essa é uma vantagem de se preferir anéis de polinômios em
detrimento de álgebras de Boole (ao menos acredito eu).
O resto da questão ainda não sei... e não sei se vou saber.
Abraços,
Walter
> Você recebeu essa mensagem porque está inscrito 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 postar nesse grupo, envie um e-mail para logi...@dimap.ufrn.br.
> Acesse esse grupo em
> https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
> Para ver essa discussão na Web, acesse
> https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAO6j_LjFidFDHSaxFpJwYfhEf13gsoEG8g2YYi9iFtPVY2e9NQ%40mail.gmail.com.
--
-----------------------------------------------
Walter Carnielli
Centre for Logic, Epistemology and the History of Science and
Department of Philosophy
State University of Campinas –UNICAMP
13083-859 Campinas -SP, Brazil
http://www.cambridge.org/br/academic/subjects/philosophy/twentieth-century-philosophy/significance-new-logic?format=HB&isbn=9781107179028
Institutional e-mail: walter.c...@cle.unicamp.br
Website: http://www.cle.unicamp.br/prof/carnielli
CV Lattes : http://lattes.cnpq.br/1055555496835379
Rodrigo Freire
May 17, 2018, 9:09:08 PM5/17/18
to logi...@dimap.ufrn.br
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”. Por exemplo, é
demonstrável que A\vee B sse é demonstrável que A ou é demonstrável que B.
Como se “é demonstrável que” fosse um morfismo da lógica na metalógica.
Isso não vale para a negação, claro. De modo mais geral, entender a negação em termos de condições de demonstrabilidade, como é tentado em contextos construtivos mainstream, é sempre complicado porque as condições de demonstrabilidade de \neg A não são as condições de não demonstrabilidade de A.
Abraço
Rodrigo
Enviado do meu iPhone
> --
> Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos Grupos do Google.
> 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/CA%2Bob58NkeY%3DvtCu5jHEeJnTaVNS7Z%2BQfvBZ2K1Jnw1n%3DpSLVMg%40mail.gmail.com.
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”. Por exemplo, é
demonstrável que A\vee B sse é demonstrável que A ou é demonstrável que B.
Como se “é demonstrável que” fosse um morfismo da lógica na metalógica.
Isso não vale para a negação, claro. De modo mais geral, entender a negação em termos de condições de demonstrabilidade, como é tentado em contextos construtivos mainstream, é sempre complicado porque as condições de demonstrabilidade de \neg A não são as condições de não demonstrabilidade de A.
Abraço
Rodrigo
Enviado do meu iPhone
> 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 postar neste grupo, envie um e-mail para logi...@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/CA%2Bob58NkeY%3DvtCu5jHEeJnTaVNS7Z%2BQfvBZ2K1Jnw1n%3DpSLVMg%40mail.gmail.com.
Valeria de Paiva
May 17, 2018, 9:24:38 PM5/17/18
to Lista acadêmica brasileira dos profissionais e estudantes da área de LOGICA
Otima pergunta, Joao Marcos!
uma que eu tb tenho carregado comigo ha algum tempo. Como voce disse, nao ha resposta certa, mas queria dar o meu palpite.
Eu acho, (e espero que isso seja junto com o Gentzen e o Prawitz ) que a gente quer pensar nos conectivos constructivos de forma que eles sejam tao independentes uns dos outros quanto possivel. a gente sabe que precisa ter conjuncao, disjuncao e implicacao independentes em logica intuitionista proposicional.
e me parece que isso 'e bom. a independencia dos conectivos mostra que eles correspondem a intuicoes diferentes, que devem ser modulares. e a gente sabe que a negacao *pode* ser definida em termos de implicacao no falso. em termos de que teoremas sao provados, a gente precisa de pelo menos esses ingredientes.
a gente tb sabe que pra logica classica, as bases sao menores, (e.g. negacao e disjuncao sao suficientes), bem como varias outras possibilidades.
ate' o famoso Scheffer stroke que faz tudo sozinho mesmo e ninguem entende nada.
mas a negacao que temos definida em termos de implicacao no falso, 'e muito ruim, na minha opiniao.
ela nao nos da' muita informacao.
ate mesmo na semantica categorica, ela colapsa todas as provas diferentes de uma mesma proposicao, jogando fora uma das razoes pra fazer semantica categorica.
>haverá alguma justificativa meta-lógica _razoável_ (em oposição a justificativas meramente ad hoc, formuladas convenientemente para "explicar" a teoria a posteriori) para considerarmos a negação como sendo preferencialmente introduzida por abreviatura, sempre que isto é possível?
acho que nao. acho que ao contrario, a negação introduzida por abreviatura 'e um problema, eu preferiria te-la como um conectivo independente.
mas nao sei como introduzi-la por si mesma num sistema construtivo, mantendo as propriedades que quero.
o que eu gostaria mesmo era de ter era uma versao de logica proposicional intuicionista onde a negacao das proposicoes basicas fosse atomica, e a gente comecasse sempre de uma versao onde as coisas fossem verdadeiras e falsas.
eu gostaria muito de uma versao da logica do Nelson N4 onde eu soubesse que substituicao de variaveis proposicionais funciona e onde eu conseguisse provar as coisas basicas tipo cut-elimination, propriedade de sub-formula, interpolacao, etc. mas eu nao sei fazer isso.
e sobre a bi-implicacao, eu nao me preocupo com ela. acho que a matematica de algebras de todos os tipos 'e legal, gosto de aneis, de espacos vetoriais, de corpos , de modulos, de espacos topologicos, de fiber bundles, de feixes, de homotopias, de variedades diferenciais, etc.. mas nao acho que bi-implicacao seja muito importante logicamente nao...
abracos
Valeria
--
Você recebeu essa mensagem porque está inscrito 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+unsubscribe@dimap.ufrn.br.
Para postar nesse grupo, envie um e-mail para logi...@dimap.ufrn.br.
Acesse esse grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAO6j_LjFidFDHSaxFpJwYfhEf13gsoEG8g2YYi9iFtPVY2e9NQ%40mail.gmail.com.
Hermógenes Oliveira
May 18, 2018, 8:47:56 AM5/18/18
to logi...@dimap.ufrn.br
Olá, João Marcos!
Joao Marcos <boto...@gmail.com> 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
*convicções* filosóficas se alinham com a "impressão de que tais
conectivos assim introduzidos não existem de verdade". Isto é, creio
que a negação, caso insistirmos seja mesmo um conectivo lógico, não está
no mesmo patamar dos outros conectivos, mas se relaciona primariamente
com restrições externas e/ou globais (trivialidade), mais do que com
restrições internas e/ou locais (contradição).
Contudo, não creio que seja pertinente expor meus sermões, ahã, quero
dizer, minhas *argumentações* filosóficas nesse sentido, embora esteja
tentado em fazê-lo. Duvido que possam ser consideradas "justificativas
meta-lógicas razoáveis".
Para aqueles que não compartilham das minhas opiniões esquisitas sobre a
negação, eu diria que as evidências metalógicas apontam na direção
oposta, isto é, *contra* a negação como abreviatura.
Uma ilustração interessante surgiu nas discussões do nosso grupo em
Tübingen algumas semanas atrás.
Nós examinávamos dois teoremas de Grigori Mints sobre regras admissíveis
em lógica intuicionista. Um dos teoremas afirma que regras admissíveis
que não figuram → são deriváveis (o outro teorema afirma o
correspondente sobre ∨). Aqui, regras admissíveis que figuram ¬ estão
incluídas, pois a negação é considerada primitiva. Alguém que
desenvolvesse investigação similar com base num sistema com a negação
definida, seria naturalmente conduzido a um resultado mais fraco.
As demonstrações de Mints são bem complicadas. Elas combinam
argumentações semânticas com argumentações sintáticas envolvendo
traduções entre lógica clássica e intuicionista. Em conversa com o Luca
alguns dias depois, eu tentava esboçar uma demonstração mais nominalista
do resultado considerando regras primitivas para a negação em dedução
natural. Por alguma razão, a conversa ficou girando em torno da
negação, e eu cheguei a mencionar a nossa discussão sobre ex
contradictione quodlibet algum tempo atrás aqui na lista. Eu apresentei
o que imagino ser a tua posição sobre o assunto. Fosse o que apresentei
a tua real posição ou um mero espantalho teu, eu acabei me encontrando
sozinho do outro lado do argumento...
Bem, de qualquer maneira, o Luca mencionou algumas coisas interessantes
(ele também estava interessado, por outros motivos, na questão da
negação como abreviatura): na axiomatização pioneira de Heyting (1930) a
negação era primitiva; Gentzen (1934) teria sido o primeiro a propor
explicitamente um sistema com a negação definida em termos da implicação
e do absurdo, embora a ideia já estivesse presente implicitamente em
escritos anteriores de Brouwer e outros precursores intuicionistas.
Eu penso que a proposta abreviativa Gentzeniana com respeito à negação
não é gratuita. Uma concepção primitiva de negação apresenta
dificuldades consideráveis com respeito à harmonia dedutiva e resultados
relacionados (normalização e etc.)[1][2], apesar do cálculo de sequentes
sugerir aqui uma saída sofisticada[3][4]. Contudo, embora de caráter
técnico, essa limitação pode ser relegada à uma mera questão pragmática
de métodos e resultados, e, para os que preferem, em todo caso, métodos
semânticos, talvez mesmo uma questão inócua. Ademais, como indico
acima, para os que não compartilham das minhas convicções religiosas,
digo, filosóficas, pode ser mesmo que razões metalógicas conduzam à
posição oposta. Por razões históricas, no entanto, as matérias técnicas
que preocupavam Gentzen ainda carregam um peso considerável nas
investigações em lógicas construtivas, de maneira que ainda é comum
encontrar a negação abreviada na literatura.
Referências:
[1] Dag Prawitz. Natural Deduction: A Proof-Theoretic Study, 1965,
Almqvist & Wiksell. Chapter II, § 1, Remark on pp. 34-35.
[2] Michael Dummett. The Logical Basis of Metaphysics, 1991, Harvard
University Press. Chapter 13, Negation, pp. 291-296.
[3] Ian Rumfitt. "Yes" and "No". Mind, 109, 781-823.
[4] Stepen Read. Harmony and Autonomy in Classical Logic. Journal of
Philosophical Logic, 29 (2), 123-154.
--
Hermógenes Oliveira
»Wir sind leicht bereit, uns selbst zu tadeln, unter der Bedingung, dass
niemand einstimmt.« -- Marie von Ebner-Eschenbach
Joao Marcos <boto...@gmail.com> 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 primitivos. Como consequência, ao enfraquecermos a
> implicação ou o absurdo, pela consideração de um fragmento dedutivo da
> lógica intuicionista, pode ocorrer que a interpretação de ¬ como algo
> implicação ou o absurdo, pela consideração de um fragmento dedutivo da
> que mereça o título de "negação" seja prejudicada.
>
> Obviamente, para fragmentos da lógica intuicionista a abordagem
> supra-citada só faz sentido quando → e ⊥ estão disponíveis. De todo
>
> Obviamente, para fragmentos da lógica intuicionista a abordagem
> modo, tendo em vista o fato de que os conectivos intuicionistas não
> são em geral interdefiníveis, não é inconcebível que a introdução de
> certos conectivos por meio de abreviaturas possa em certas situações
> ser conveniente, por alguma razão... embora isto possa também passar a
> impressão de que tais conectivos assim introduzidos "não existem de
> verdade".
>
> A pergunta que lanço aqui é: ao trabalhar com *lógicas construtivas*
> (que sejam fragmentos da lógica clássica ou, digamos, de alguma
> extensão modal da lógica clássica), haverá alguma justificativa
> meta-lógica _razoável_ (em oposição a justificativas meramente ad hoc,
> formuladas convenientemente para "explicar" a teoria a posteriori)
> para considerarmos a negação como sendo preferencialmente introduzida
> por abreviatura, sempre que isto é possível?
Antes de mais nada, devo avisar que os meus preconceitos, ahã, perdão,
> são em geral interdefiníveis, não é inconcebível que a introdução de
> certos conectivos por meio de abreviaturas possa em certas situações
> ser conveniente, por alguma razão... embora isto possa também passar a
> impressão de que tais conectivos assim introduzidos "não existem de
> verdade".
>
> A pergunta que lanço aqui é: ao trabalhar com *lógicas construtivas*
> (que sejam fragmentos da lógica clássica ou, digamos, de alguma
> extensão modal da lógica clássica), haverá alguma justificativa
> meta-lógica _razoável_ (em oposição a justificativas meramente ad hoc,
> formuladas convenientemente para "explicar" a teoria a posteriori)
> para considerarmos a negação como sendo preferencialmente introduzida
> por abreviatura, sempre que isto é possível?
*convicções* filosóficas se alinham com a "impressão de que tais
conectivos assim introduzidos não existem de verdade". Isto é, creio
que a negação, caso insistirmos seja mesmo um conectivo lógico, não está
no mesmo patamar dos outros conectivos, mas se relaciona primariamente
com restrições externas e/ou globais (trivialidade), mais do que com
restrições internas e/ou locais (contradição).
Contudo, não creio que seja pertinente expor meus sermões, ahã, quero
dizer, minhas *argumentações* filosóficas nesse sentido, embora esteja
tentado em fazê-lo. Duvido que possam ser consideradas "justificativas
meta-lógicas razoáveis".
Para aqueles que não compartilham das minhas opiniões esquisitas sobre a
negação, eu diria que as evidências metalógicas apontam na direção
oposta, isto é, *contra* a negação como abreviatura.
Uma ilustração interessante surgiu nas discussões do nosso grupo em
Tübingen algumas semanas atrás.
Nós examinávamos dois teoremas de Grigori Mints sobre regras admissíveis
em lógica intuicionista. Um dos teoremas afirma que regras admissíveis
que não figuram → são deriváveis (o outro teorema afirma o
correspondente sobre ∨). Aqui, regras admissíveis que figuram ¬ estão
incluídas, pois a negação é considerada primitiva. Alguém que
desenvolvesse investigação similar com base num sistema com a negação
definida, seria naturalmente conduzido a um resultado mais fraco.
As demonstrações de Mints são bem complicadas. Elas combinam
argumentações semânticas com argumentações sintáticas envolvendo
traduções entre lógica clássica e intuicionista. Em conversa com o Luca
alguns dias depois, eu tentava esboçar uma demonstração mais nominalista
do resultado considerando regras primitivas para a negação em dedução
natural. Por alguma razão, a conversa ficou girando em torno da
negação, e eu cheguei a mencionar a nossa discussão sobre ex
contradictione quodlibet algum tempo atrás aqui na lista. Eu apresentei
o que imagino ser a tua posição sobre o assunto. Fosse o que apresentei
a tua real posição ou um mero espantalho teu, eu acabei me encontrando
sozinho do outro lado do argumento...
Bem, de qualquer maneira, o Luca mencionou algumas coisas interessantes
(ele também estava interessado, por outros motivos, na questão da
negação como abreviatura): na axiomatização pioneira de Heyting (1930) a
negação era primitiva; Gentzen (1934) teria sido o primeiro a propor
explicitamente um sistema com a negação definida em termos da implicação
e do absurdo, embora a ideia já estivesse presente implicitamente em
escritos anteriores de Brouwer e outros precursores intuicionistas.
Eu penso que a proposta abreviativa Gentzeniana com respeito à negação
não é gratuita. Uma concepção primitiva de negação apresenta
dificuldades consideráveis com respeito à harmonia dedutiva e resultados
relacionados (normalização e etc.)[1][2], apesar do cálculo de sequentes
sugerir aqui uma saída sofisticada[3][4]. Contudo, embora de caráter
técnico, essa limitação pode ser relegada à uma mera questão pragmática
de métodos e resultados, e, para os que preferem, em todo caso, métodos
semânticos, talvez mesmo uma questão inócua. Ademais, como indico
acima, para os que não compartilham das minhas convicções religiosas,
digo, filosóficas, pode ser mesmo que razões metalógicas conduzam à
posição oposta. Por razões históricas, no entanto, as matérias técnicas
que preocupavam Gentzen ainda carregam um peso considerável nas
investigações em lógicas construtivas, de maneira que ainda é comum
encontrar a negação abreviada na literatura.
Referências:
[1] Dag Prawitz. Natural Deduction: A Proof-Theoretic Study, 1965,
Almqvist & Wiksell. Chapter II, § 1, Remark on pp. 34-35.
[2] Michael Dummett. The Logical Basis of Metaphysics, 1991, Harvard
University Press. Chapter 13, Negation, pp. 291-296.
[3] Ian Rumfitt. "Yes" and "No". Mind, 109, 781-823.
[4] Stepen Read. Harmony and Autonomy in Classical Logic. Journal of
Philosophical Logic, 29 (2), 123-154.
--
Hermógenes Oliveira
»Wir sind leicht bereit, uns selbst zu tadeln, unter der Bedingung, dass
niemand einstimmt.« -- Marie von Ebner-Eschenbach
Durante
May 18, 2018, 3:59:47 PM5/18/18
to LOGICA-L
Oi João e colegas,
Concordo com o Rodrigo. Usando outras palavras eu diria: ~A não faz sentido construtivo. Como apresentar a construção do que não se constrói? Não dá. A alternativa é, então, mostrar as consequências de uma suposta construção. Ao assumirmos como construído o que não se constrói, devemos ter como consequência algo ruim, catastrófico, negativo (trocadilho inevitável). Daí o A -> ⊥.
Saudações,
Daniel.
PS: só para registrar, como você sabe, o A -> ⊥ funciona também como definição da negação clássica. E há vários motivos, mas que eu saiba todos ad hoc, para usa-la.
Valeria de Paiva
May 18, 2018, 4:38:43 PM5/18/18
to Lista acadêmica brasileira dos profissionais e estudantes da área de LOGICA
oi Daniel,
obrigada pela sua explicacao. acho que eu entendo melhor a sua mensagem, do que a do Rodrigo.mas achei legal ver
>Ao assumirmos como construído o que não se constrói, devemos ter como consequência algo ruim, catastrófico, negativo (trocadilho inevitável).
e eu me pergunto, quais sao esses motivos hem?
>E há vários motivos, mas que eu saiba todos ad hoc, para usa-la.
abracos
Valeria--
Você recebeu essa mensagem porque está inscrito 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+unsubscribe@dimap.ufrn.br.
Para postar nesse grupo, envie um e-mail para logi...@dimap.ufrn.br.
Acesse esse grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/6f8a7ae5-4185-438a-9a5f-ddeac5da0105%40dimap.ufrn.br.
Abílio
May 18, 2018, 4:52:27 PM5/18/18
to logi...@dimap.ufrn.br
Colegas, vou tentar uns 'pitacos filosoficos' aqui.
1. De fato, ~A nao tem sentido construtivo, ao passo q A -> \bot parece ter.
2. Me parece q construtivamente nem o ex falso nem A -> (B ->A)
deveriam ser validos. Ha razoes para achar q uma 'logica de Brouwer'
deveria ser paraconsistente e relevante. Mas nao pq isso parece ser a
melhor interpretacao do q Brouwer diz, mas sim pq ~A -> (A -> B) e A
-> (B ->A) nao parecem validos do pto de vista construtivo (van Atten
fala sobre).
3. Sobre definir ~ com \bot. Dentre os conceitos de ~ e \bot, qual
parece ser intuitivamente mais plausivel? Me parece q o \bot. A ~ traz
todos aqueles velhos problemas filosoficos de nao ser etc. O \bot eh
algo ruim, inconcebivel, catastrofico, inaceitavel (ok Daniel?) - o
conceito, a ideia de algo ruim, inconcebivel, catastrofico,
inaceitavel me parece ser bastante clara.
Abracos
Abilio
1. De fato, ~A nao tem sentido construtivo, ao passo q A -> \bot parece ter.
2. Me parece q construtivamente nem o ex falso nem A -> (B ->A)
deveriam ser validos. Ha razoes para achar q uma 'logica de Brouwer'
deveria ser paraconsistente e relevante. Mas nao pq isso parece ser a
melhor interpretacao do q Brouwer diz, mas sim pq ~A -> (A -> B) e A
-> (B ->A) nao parecem validos do pto de vista construtivo (van Atten
fala sobre).
3. Sobre definir ~ com \bot. Dentre os conceitos de ~ e \bot, qual
parece ser intuitivamente mais plausivel? Me parece q o \bot. A ~ traz
todos aqueles velhos problemas filosoficos de nao ser etc. O \bot eh
algo ruim, inconcebivel, catastrofico, inaceitavel (ok Daniel?) - o
conceito, a ideia de algo ruim, inconcebivel, catastrofico,
inaceitavel me parece ser bastante clara.
Abracos
Abilio
> --
> Você recebeu essa mensagem porque está inscrito 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.
> Você recebeu essa mensagem porque está inscrito no grupo "LOGICA-L" dos
> Grupos do Google.
> Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie
Andrea Loparic
May 18, 2018, 8:08:34 PM5/18/18
to Lista_Lógica
Só uma pequena observação en passant, trivial, porém,
se for esquecida, pode levar a confusões. As definições
que costumam ser escritas por A -> bot nas lógicas
clássicas e intuicionista são de fato duas distintas,
uma vez que -> tem dois diferentes significados, ok?
Claro, todo mundo sabe disso, foi só um lembrete.
No mais, vou pensar quando der.
Bjs,
Andrea
> um e-mail para logica-l+unsubscribe@dimap.ufrn.br.
> Para postar nesse grupo, envie um e-mail para logi...@dimap.ufrn.br.
> Acesse esse grupo em
> https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
> Para ver essa discussão na Web, acesse
> https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/6f8a7ae5-4185-438a-9a5f-ddeac5da0105%40dimap.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+unsubscribe@dimap.ufrn.br.
Para postar neste grupo, envie um e-mail para logi...@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/CALtFD22m%2BhZdK6GgUZ1Egfuvq3w9Jrzx%3DNRbBPGk%2B16e8z2NWQ%40mail.gmail.com.
Andrea Loparic
May 18, 2018, 9:35:50 PM5/18/18
to Lista_Lógica
Ah, vi agora o post do Abilio. Para mim, nominalista
até onde for possível, a negação é de natureza essencialmente
linguística. Fora da linguagem, à negação só creio ter
sentido associar o gesto de rejeição-ou o ato de destruição
- seja lá do que for. Como alguns de vocês já insinuaram!
> um e-mail para logica-l+u...@dimap.ufrn.br.
> Para postar nesse grupo, envie um e-mail para logi...@dimap.ufrn.br.
> Acesse esse grupo em
> https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
> Para ver essa discussão na Web, acesse
> https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/6f8a7ae5-4185-438a-9a5f-ddeac5da0105%40dimap.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.
Valeria de Paiva
May 19, 2018, 2:51:44 PM5/19/18
to Lista acadêmica brasileira dos profissionais e estudantes da área de LOGICA
qual 'e a referencia, Abilio?
>(van Atten fala sobre).
>(van Atten fala sobre).
--
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 postar neste grupo, envie um e-mail para logi...@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/CALtFD22m%2BhZdK6GgUZ1Egfuvq3w9Jrzx%3DNRbBPGk%2B16e8z2NWQ%40mail.gmail.com.
Abílio
May 19, 2018, 5:03:47 PM5/19/18
to Lista acadêmica brasileira dos profissionais e estudantes da área de LOGICA
oi valeria
aqui
On the hypothetical judgement in the history of intuitionistic logic.
In: glymour, c.; wang, w.; westerstahl, d. (eds.) Logic, methodology,
and philosophy of science: proceedings of the thirteenth international
congress. London: king's college publications, 2009.
> https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAESt%3DXuTwxNo0vGqj%3DnzLaGhnTn%2By%2BQLhiOcAJtUgxVQ7UPuTQ%40mail.gmail.com.
aqui
On the hypothetical judgement in the history of intuitionistic logic.
In: glymour, c.; wang, w.; westerstahl, d. (eds.) Logic, methodology,
and philosophy of science: proceedings of the thirteenth international
congress. London: king's college publications, 2009.
Juan Carlos Agudelo Agudelo
May 19, 2018, 5:48:01 PM5/19/18
to Lista acadêmica brasileira dos profissionais e estudantes da área de LOGICA
Pensando na afirmação da Andrea Loparic:
"Fora da linguagem, à negação só creio ter
sentido associar o gesto de rejeição-ou o ato de destruição
- seja lá do que for. Como alguns de vocês já insinuaram! "
A fome não pode ser considerada evidencia (ou proba) de não ter comido (ou não ter comido o suficiente)?
Em matemáticas, o fato de que 6 = 3 x 2 é evidencia suficiente para deduzir que 6
não é primo.
Acho sim que a negação pode ser tratada de maneira construtiva, e acho que a negação intuicionista não é a melhor maneira de formalizar a negação desde um ponto de vista construcivista.
Abs,
Juan Carlos
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+unsubscribe@dimap.ufrn.br.
Para postar nesse grupo, envie um e-mail para logi...@dimap.ufrn.br.
Acesse esse grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CACHAqB%3DVRdQd5DOHA9f95bmc%3DhUcVjDeisN6tEg0cTCiW3Kijg%40mail.gmail.com.
Valeria de Paiva
May 19, 2018, 8:26:11 PM5/19/18
to Lista acadêmica brasileira dos profissionais e estudantes da área de LOGICA
obrigada, Abilio!
>> > um e-mail para logica-l+unsubscribe@dimap.ufrn.br.
>> > Para postar nesse grupo, envie um e-mail para logi...@dimap.ufrn.br.
>> > Acesse esse grupo em
>> > https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
>> > Para ver essa discussão na Web, acesse
>> >
>> > https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/6f8a7ae5-4185-438a-9a5f-ddeac5da0105%40dimap.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+unsubscribe@dimap.ufrn.br.
>> Para postar neste grupo, envie um e-mail para logi...@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/CALtFD22m%2BhZdK6GgUZ1Egfuvq3w9Jrzx%3DNRbBPGk%2B16e8z2NWQ%40mail.gmail.com.
>
>
>
>
> --
> Valeria de Paiva
> http://vcvpaiva.github.io/
> http://research.nuance.com/author/valeria-de-paiva/
> http://www.cs.bham.ac.uk/~vdp/
>
> --
> Você recebeu essa mensagem porque está inscrito 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+unsubscribe@dimap.ufrn.br.
> Para postar nesse grupo, envie um e-mail para logi...@dimap.ufrn.br.
> Acesse esse grupo em
> https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
> Para ver essa discussão na Web, acesse
--
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+unsubscribe@dimap.ufrn.br.
Para postar neste grupo, envie um e-mail para logi...@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/CALtFD23Rz94-C-ErVcUd2Ze2qM%2BqZxuPo1tcJ6ocVomM6Li%2Bqw%40mail.gmail.com.
Fernando Yamauti
May 22, 2018, 6:29:16 AM5/22/18
to logi...@dimap.ufrn.br
Só duas consideração provavelmente irrelevantes e que não interessam a ninguem. Na pratica matemática, se prova a negação de algo assumindo esse algo e chegando a uma contradição. Mas do ponto de vista do significado da proposição \neg A, ele é completamente determinado pela regra de introdução e, portanto, \neg A tem já algum significado independente de 0 e --> a priori (talvez seja isso que a Valéria tenha dito acima, não sei)
Como o Abilio mencionou acima, seria melhor (na verdade, seria a única maneira realmente construtiva) tomar um ponto de vista paraconsistente (igual originalmente o Brouwer e o Kolmogorov pensavam) quando se define a negação como A --> 0. Minha sugestao seria colocar termos em 0. Afinal, é assim que se pensa na matemática. Qualquer contradição deveria ser um termo canônico de 0.
Abs.,
Fernando
obrigada, Abilio!
>> > um e-mail para logica-l+u...@dimap.ufrn.br.
>> > Para postar nesse grupo, envie um e-mail para logi...@dimap.ufrn.br.
>> > Acesse esse grupo em
>> > https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
>> > Para ver essa discussão na Web, acesse
>> >
>> > https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/6f8a7ae5-4185-438a-9a5f-ddeac5da0105%40dimap.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 postar neste grupo, envie um e-mail para logi...@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/CALtFD22m%2BhZdK6GgUZ1Egfuvq3w9Jrzx%3DNRbBPGk%2B16e8z2NWQ%40mail.gmail.com.
>
>
>
>
> --
> Valeria de Paiva
> http://vcvpaiva.github.io/
> http://research.nuance.com/author/valeria-de-paiva/
> http://www.cs.bham.ac.uk/~vdp/
>
> --
> Você recebeu essa mensagem porque está inscrito 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 postar nesse grupo, envie um e-mail para logi...@dimap.ufrn.br.
> Acesse esse grupo em
> https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
> Para ver essa discussão na Web, acesse
--
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 postar neste grupo, envie um e-mail para logi...@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/CALtFD23Rz94-C-ErVcUd2Ze2qM%2BqZxuPo1tcJ6ocVomM6Li%2Bqw%40mail.gmail.com.
--
Você recebeu essa mensagem porque está inscrito 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+unsubscribe@dimap.ufrn.br.
Para postar nesse grupo, envie um e-mail para logi...@dimap.ufrn.br.
Acesse esse grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAESt%3DXtA1zye2PL4%2B6GhUeTQmbdaLH7_XP6_EPBK6RSfE6OW5A%40mail.gmail.com.
Joao Marcos
May 30, 2018, 7:40:25 AM5/30/18
to Lista acadêmica brasileira dos profissionais e estudantes da área de LOGICA
PessoALL:
Agradeço bastante as múltiplas e diversas respostas enviadas à minha
pergunta, tanto dentro quanto fora desta lista. Na falta de uma
"resposta certa", tudo que me compete fazer é comentar brevemente as
respostas dos colegas.
(Estou preparando slides para um curso de duas semanas que oferecerei
sobre lógica paraconsistente em Pequim agora em junho, e a minha
quarta aula está dedicada ao tema da dualidade, que é onde o
entendimento intuicionista do significado da negação pode ter algum
interesse. Não deixa de ser curioso que *do ponto de vista
construtivo* tanto a implicação quanto o absurdo tenham interpretações
não-problemáticas, mas que um conectivo definido pela composição
destes outros dois seja frequentemente tido como problemático...)
> 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, comutativa, tem elemento neutro (o top), etc. A
> coisa se generaliza bem naturalmente para lógicas multivaloradas,
> modais, etc.
Compreendo isto, Walter, mas esta é uma resposta que seria prontamente
classificada como aquilo que chamei de "a posteriori": ela apenas
explica porque as coisas são como são... Isto serve para fazer
continhas, claro, mas não contribui conceitualmente à pergunta que eu
fiz, ou tentei fazer!
> 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”. Por exemplo, é
>
> demonstrável que A\vee B sse é demonstrável que A ou é demonstrável que B.
>
> Como se “é demonstrável que” fosse um morfismo da lógica na metalógica.
>
> Isso não vale para a negação, claro. De modo mais geral, entender a negação em termos de condições de demonstrabilidade, como é tentado em contextos construtivos mainstream, é sempre complicado porque as condições de demonstrabilidade de \neg A não são as condições de não demonstrabilidade de A.
Não vou esconder que esta é a minha resposta favorita entre todas que
recebi, Rodrigo.
Uma interpretação verificacionista encontra dificuldades quando
encontra conectivos que expressam o conceito de falsificação, tais
como a negação intuicionista ou a co-implicação. Uma saída possível
seria pensar na negação como fazendo a ponte entre demonstrabilidade e
seu dual (chamemo-lo refutabilidade): \neg A é demonstrável sse A é
refutável, \neg A é refutável sse A é demonstrável. As propriedades
de demonstrabilidade obviamente se dualizam apropriadamente: é
refutável que A\wedge B sse é refutável que A ou é refutável que B.
Não por acaso, esta é a abordagem da lógica bi-intuicionista.
> Eu acho, (e espero que isso seja junto com o Gentzen e o Prawitz ) que a
> gente quer pensar nos conectivos constructivos de forma que eles sejam tao
> independentes uns dos outros quanto possivel. a gente sabe que precisa ter
> conjuncao, disjuncao e implicacao independentes em logica intuitionista
> proposicional.
> e me parece que isso 'e bom. a independencia dos conectivos mostra que eles
> correspondem a intuicoes diferentes, que devem ser modulares. e a gente
> sabe que a negacao *pode* ser definida em termos de implicacao no falso. em
> termos de que teoremas sao provados, a gente precisa de pelo menos esses
> ingredientes.
Mas e se a negação fosse outra, Valeria? Alternativamente, e se eu
quiser estudar um fragmento da lógica intuicionista em que a
implicação ou o falso não estejam presentes, mas a negação esteja?
> o que eu gostaria mesmo era de ter era uma versao de logica proposicional
> intuicionista onde a negacao das proposicoes basicas fosse atomica, e a
> gente comecasse sempre de uma versao onde as coisas fossem verdadeiras e
> falsas.
De acordo!
> eu gostaria muito de uma versao da logica do Nelson N4 onde eu soubesse que
> substituicao de variaveis proposicionais funciona e onde eu conseguisse
> provar as coisas basicas tipo cut-elimination, propriedade de sub-formula,
> interpolacao, etc. mas eu nao sei fazer isso.
Talvez não seja impossível?
> e sobre a bi-implicacao, eu nao me preocupo com ela. acho que a matematica
> de algebras de todos os tipos 'e legal, gosto de aneis, de espacos
> vetoriais, de corpos , de modulos, de espacos topologicos, de fiber bundles,
> de feixes, de homotopias, de variedades diferenciais, etc.. mas nao acho
> que bi-implicacao seja muito importante logicamente nao...
Bem, sem bi-implicação e suas generalizações não há relações de
equivalência... ou lógica algébrica!
> Antes de mais nada, devo avisar que os meus preconceitos, ahã, perdão,
> *convicções* filosóficas se alinham com a "impressão de que tais
> conectivos assim introduzidos não existem de verdade". Isto é, creio
> que a negação, caso insistirmos seja mesmo um conectivo lógico, não está
> no mesmo patamar dos outros conectivos, mas se relaciona primariamente
> com restrições externas e/ou globais (trivialidade), mais do que com
> restrições internas e/ou locais (contradição).
E como um inferencialista faria para estudar a negação intuicionista
se a implicação for extirpada da linguagem, Hermógenes? (o teorema de
Mints faz sentido neste contexto, né?)
> Bem, de qualquer maneira, o Luca mencionou algumas coisas interessantes
> (ele também estava interessado, por outros motivos, na questão da
> negação como abreviatura): na axiomatização pioneira de Heyting (1930) a
> negação era primitiva; Gentzen (1934) teria sido o primeiro a propor
> explicitamente um sistema com a negação definida em termos da implicação
> e do absurdo, embora a ideia já estivesse presente implicitamente em
> escritos anteriores de Brouwer e outros precursores intuicionistas.
Sem dúvida, Gentzen é o culpado! Se a lógica minimal de Johánsson
(1936) tivesse levado a melhor, contudo, era possível que a ideia da
negação como abreviatura tivesse logo caído em desuso...
> Eu penso que a proposta abreviativa Gentzeniana com respeito à negação
> não é gratuita. Uma concepção primitiva de negação apresenta
> dificuldades consideráveis com respeito à harmonia dedutiva e resultados
> relacionados (normalização e etc.)[1][2], apesar do cálculo de sequentes
> sugerir aqui uma saída sofisticada[3][4]. Contudo, embora de caráter
> técnico, essa limitação pode ser relegada à uma mera questão pragmática
> de métodos e resultados, e, para os que preferem, em todo caso, métodos
> semânticos, talvez mesmo uma questão inócua. Ademais, como indico
> acima, para os que não compartilham das minhas convicções religiosas,
> digo, filosóficas, pode ser mesmo que razões metalógicas conduzam à
> posição oposta. Por razões históricas, no entanto, as matérias técnicas
> que preocupavam Gentzen ainda carregam um peso considerável nas
> investigações em lógicas construtivas, de maneira que ainda é comum
> encontrar a negação abreviada na literatura.
Sim, "razões técnicas" são frequentemente ideologizadas...
> PS: só para registrar, como você sabe, o A -> ⊥ funciona também como
> definição da negação clássica. E há vários motivos, mas que eu saiba todos
> ad hoc, para usa-la.
Como você sabe, Daniel, também A <-> ⊥ poderia ser usado, e as
consequências (e inferências válidas) seriam outras...
> De fato, ~A nao tem sentido construtivo, ao passo q A -> \bot parece ter.
Só "parece", não é, Abílio?
> Só uma pequena observação en passant, trivial, porém,
> se for esquecida, pode levar a confusões. As definições
> que costumam ser escritas por A -> bot nas lógicas
> clássicas e intuicionista são de fato duas distintas,
> uma vez que -> tem dois diferentes significados, ok?
Corretíssimo, Andrea. E na lógica minimal, na qual o bot "não é
nenhum absurdo", a definição seria ainda outra...
> Pensando na afirmação da Andrea Loparic:
> "Fora da linguagem, à negação só creio ter
> sentido associar o gesto de rejeição-ou o ato de destruição
> - seja lá do que for. Como alguns de vocês já insinuaram! "
>
> A fome não pode ser considerada evidencia (ou proba) de não ter comido (ou
> não ter comido o suficiente)?
>
> Em matemáticas, o fato de que 6 = 3 x 2 é evidencia suficiente para deduzir
> que 6 não é primo.
Talvez por isso seja conveniente falar construtivamente em dois tipos
de "evidência" (para *verificação*, e para *refutação*)?
> Acho sim que a negação pode ser tratada de maneira construtiva, e acho que a
> negação intuicionista não é a melhor maneira de formalizar a negação desde
> um ponto de vista construcivista.
Isso. Você sugeriria alguma alternativa específica, Juan?
> Como o Abilio mencionou acima, seria melhor (na verdade, seria a única
> maneira realmente construtiva) tomar um ponto de vista paraconsistente
> (igual originalmente o Brouwer e o Kolmogorov pensavam) quando se define a
> negação como A --> 0. Minha sugestao seria colocar termos em 0. Afinal, é
> assim que se pensa na matemática. Qualquer contradição deveria ser um termo
> canônico de 0.
Quando você fala em tomar um ponto de vista paraconsistente, Fernando,
está querendo dizer que de A e A --> 0 não se seguiria uma fórmula
qualquer?
Abraços a todos,
Joao Marcos
--
http://sequiturquodlibet.googlepages.com/
Agradeço bastante as múltiplas e diversas respostas enviadas à minha
pergunta, tanto dentro quanto fora desta lista. Na falta de uma
"resposta certa", tudo que me compete fazer é comentar brevemente as
respostas dos colegas.
(Estou preparando slides para um curso de duas semanas que oferecerei
sobre lógica paraconsistente em Pequim agora em junho, e a minha
quarta aula está dedicada ao tema da dualidade, que é onde o
entendimento intuicionista do significado da negação pode ter algum
interesse. Não deixa de ser curioso que *do ponto de vista
construtivo* tanto a implicação quanto o absurdo tenham interpretações
não-problemáticas, mas que um conectivo definido pela composição
destes outros dois seja frequentemente tido como problemático...)
> 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, comutativa, tem elemento neutro (o top), etc. A
> coisa se generaliza bem naturalmente para lógicas multivaloradas,
> modais, etc.
classificada como aquilo que chamei de "a posteriori": ela apenas
explica porque as coisas são como são... Isto serve para fazer
continhas, claro, mas não contribui conceitualmente à pergunta que eu
fiz, ou tentei fazer!
> 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”. Por exemplo, é
>
> demonstrável que A\vee B sse é demonstrável que A ou é demonstrável que B.
>
> Como se “é demonstrável que” fosse um morfismo da lógica na metalógica.
>
> Isso não vale para a negação, claro. De modo mais geral, entender a negação em termos de condições de demonstrabilidade, como é tentado em contextos construtivos mainstream, é sempre complicado porque as condições de demonstrabilidade de \neg A não são as condições de não demonstrabilidade de A.
recebi, Rodrigo.
Uma interpretação verificacionista encontra dificuldades quando
encontra conectivos que expressam o conceito de falsificação, tais
como a negação intuicionista ou a co-implicação. Uma saída possível
seria pensar na negação como fazendo a ponte entre demonstrabilidade e
seu dual (chamemo-lo refutabilidade): \neg A é demonstrável sse A é
refutável, \neg A é refutável sse A é demonstrável. As propriedades
de demonstrabilidade obviamente se dualizam apropriadamente: é
refutável que A\wedge B sse é refutável que A ou é refutável que B.
Não por acaso, esta é a abordagem da lógica bi-intuicionista.
> Eu acho, (e espero que isso seja junto com o Gentzen e o Prawitz ) que a
> gente quer pensar nos conectivos constructivos de forma que eles sejam tao
> independentes uns dos outros quanto possivel. a gente sabe que precisa ter
> conjuncao, disjuncao e implicacao independentes em logica intuitionista
> proposicional.
> e me parece que isso 'e bom. a independencia dos conectivos mostra que eles
> correspondem a intuicoes diferentes, que devem ser modulares. e a gente
> sabe que a negacao *pode* ser definida em termos de implicacao no falso. em
> termos de que teoremas sao provados, a gente precisa de pelo menos esses
> ingredientes.
quiser estudar um fragmento da lógica intuicionista em que a
implicação ou o falso não estejam presentes, mas a negação esteja?
> o que eu gostaria mesmo era de ter era uma versao de logica proposicional
> intuicionista onde a negacao das proposicoes basicas fosse atomica, e a
> gente comecasse sempre de uma versao onde as coisas fossem verdadeiras e
> falsas.
> eu gostaria muito de uma versao da logica do Nelson N4 onde eu soubesse que
> substituicao de variaveis proposicionais funciona e onde eu conseguisse
> provar as coisas basicas tipo cut-elimination, propriedade de sub-formula,
> interpolacao, etc. mas eu nao sei fazer isso.
> e sobre a bi-implicacao, eu nao me preocupo com ela. acho que a matematica
> de algebras de todos os tipos 'e legal, gosto de aneis, de espacos
> vetoriais, de corpos , de modulos, de espacos topologicos, de fiber bundles,
> de feixes, de homotopias, de variedades diferenciais, etc.. mas nao acho
> que bi-implicacao seja muito importante logicamente nao...
equivalência... ou lógica algébrica!
> Antes de mais nada, devo avisar que os meus preconceitos, ahã, perdão,
> *convicções* filosóficas se alinham com a "impressão de que tais
> conectivos assim introduzidos não existem de verdade". Isto é, creio
> que a negação, caso insistirmos seja mesmo um conectivo lógico, não está
> no mesmo patamar dos outros conectivos, mas se relaciona primariamente
> com restrições externas e/ou globais (trivialidade), mais do que com
> restrições internas e/ou locais (contradição).
se a implicação for extirpada da linguagem, Hermógenes? (o teorema de
Mints faz sentido neste contexto, né?)
> Bem, de qualquer maneira, o Luca mencionou algumas coisas interessantes
> (ele também estava interessado, por outros motivos, na questão da
> negação como abreviatura): na axiomatização pioneira de Heyting (1930) a
> negação era primitiva; Gentzen (1934) teria sido o primeiro a propor
> explicitamente um sistema com a negação definida em termos da implicação
> e do absurdo, embora a ideia já estivesse presente implicitamente em
> escritos anteriores de Brouwer e outros precursores intuicionistas.
(1936) tivesse levado a melhor, contudo, era possível que a ideia da
negação como abreviatura tivesse logo caído em desuso...
> Eu penso que a proposta abreviativa Gentzeniana com respeito à negação
> não é gratuita. Uma concepção primitiva de negação apresenta
> dificuldades consideráveis com respeito à harmonia dedutiva e resultados
> relacionados (normalização e etc.)[1][2], apesar do cálculo de sequentes
> sugerir aqui uma saída sofisticada[3][4]. Contudo, embora de caráter
> técnico, essa limitação pode ser relegada à uma mera questão pragmática
> de métodos e resultados, e, para os que preferem, em todo caso, métodos
> semânticos, talvez mesmo uma questão inócua. Ademais, como indico
> acima, para os que não compartilham das minhas convicções religiosas,
> digo, filosóficas, pode ser mesmo que razões metalógicas conduzam à
> posição oposta. Por razões históricas, no entanto, as matérias técnicas
> que preocupavam Gentzen ainda carregam um peso considerável nas
> investigações em lógicas construtivas, de maneira que ainda é comum
> encontrar a negação abreviada na literatura.
> PS: só para registrar, como você sabe, o A -> ⊥ funciona também como
> definição da negação clássica. E há vários motivos, mas que eu saiba todos
> ad hoc, para usa-la.
consequências (e inferências válidas) seriam outras...
> De fato, ~A nao tem sentido construtivo, ao passo q A -> \bot parece ter.
> Só uma pequena observação en passant, trivial, porém,
> se for esquecida, pode levar a confusões. As definições
> que costumam ser escritas por A -> bot nas lógicas
> clássicas e intuicionista são de fato duas distintas,
> uma vez que -> tem dois diferentes significados, ok?
nenhum absurdo", a definição seria ainda outra...
> Pensando na afirmação da Andrea Loparic:
> "Fora da linguagem, à negação só creio ter
> sentido associar o gesto de rejeição-ou o ato de destruição
> - seja lá do que for. Como alguns de vocês já insinuaram! "
>
> A fome não pode ser considerada evidencia (ou proba) de não ter comido (ou
> não ter comido o suficiente)?
>
> Em matemáticas, o fato de que 6 = 3 x 2 é evidencia suficiente para deduzir
> que 6 não é primo.
de "evidência" (para *verificação*, e para *refutação*)?
> Acho sim que a negação pode ser tratada de maneira construtiva, e acho que a
> negação intuicionista não é a melhor maneira de formalizar a negação desde
> um ponto de vista construcivista.
> Como o Abilio mencionou acima, seria melhor (na verdade, seria a única
> maneira realmente construtiva) tomar um ponto de vista paraconsistente
> (igual originalmente o Brouwer e o Kolmogorov pensavam) quando se define a
> negação como A --> 0. Minha sugestao seria colocar termos em 0. Afinal, é
> assim que se pensa na matemática. Qualquer contradição deveria ser um termo
> canônico de 0.
está querendo dizer que de A e A --> 0 não se seguiria uma fórmula
qualquer?
Abraços a todos,
Joao Marcos
--
http://sequiturquodlibet.googlepages.com/
Juan Carlos Agudelo Agudelo
May 30, 2018, 10:50:30 AM5/30/18
to Lista acadêmica brasileira dos profissionais e estudantes da área de LOGICA
Olá João,
Vou ampliar um pouquinho mais minha ideia:
Acho que tanto na vida cotidiana, quanto na matemática, razonamos sobre afirmações e negações da mesma maneira. Assim como algumas "evidencias" permitem deduzir afirmações, outras evidencias permitem deduzir negações. Também acho que se pode pensar em "refutações" e "demostrações" como conceitos duais: una demonstração de uma proposição A é uma refutação da proposição ~A, e uma refutação de uma proposição A é uma demostração de ~A.
O exemplo que dei da vida cotidiana talvez não foi o melhor. Talvez um melhor exemplo seja: a rua seca é evidencia para deduzir que não choveu, ou para refutar que choveu (assim como a rua molhada é evidencia para deduzir que choveu, ou para refutar que não choveu).
O exemplo dos números primos acho que é melhor. Alias, se no lugar de considerar a definição de "número primo", se considera a definição de "número composto", é obvio que o que serve para demostrar que um número N é primo, também serve para refutar que N é composto, e o que serve para refutar que N é um número primo, também serve para demostrar que N é composto. ¿por que então exigir um razonamento hipotético que leve a contradições para demostrar negações? (acho que essa pode ser uma maneira de provar negações -- e também afirmações-- mas não é unica maneira).
Confesso que atualmente tenho um projeto de pesquisa (com o Andrés Sicard, a quem você conhece) no qual estou trabalhando nessas ideias, já temos alguns resultados e esperamos poder someter a publicacao esses resultados de aqui a pouco.
Um abraço,
Juan Carlos
--
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+unsubscribe@dimap.ufrn.br.
Para postar neste grupo, envie um e-mail para logi...@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/CAO6j_Li9hiQJqGbi%2BYPutno6JN0O35T1AWN0oU8cUhfrp8uxOg%40mail.gmail.com.
Fernando Yamauti
May 31, 2018, 12:57:34 AM5/31/18
to logi...@dimap.ufrn.br
Oi João,
Sim. O 0 deixaria de ser objeto inicial (o Brouwer antes de afrouxar concordava com isso e o Kolmogorov sempre concordou). E, caso a negação seja definida de maneira primitiva, o 0 teria uma regra de introdução do tipo
a :A, b : \neg A
------------------------
c (a, b) : 0
Então, a priori, 0 poderia ter pontos 1 --> 0 que corresponderiam às contradições. Isso não muda muita coisa, mas, pelo menos, tira algumas heresias não construtivas (ausência de provas geram provas!?) e a bizarrice de que todo A = 0 quando ocorre uma contradição (o que implicaria que todas as contradições são iguais).
Só repetindo o óbvio. Definir a negação de maneira primitiva é equivalente a definir o que significa uma prova canônica de \neg A (a condição de demonstrabilidade de \neg A). Quando se concorda que uma prova canônica de \neg A é necessariamente uma regra que leva uma prova canônica de A até uma contradição, inevitavelmente se chega a \neg A = A --> 0. Existiria outra definição de prova canônica de \neg A tal que \neg A ainda mereça ser chamada de "negação de A"? Se a resposta for negativa, então construtivamente não existe outra definição de \neg A.
Também chamo atenção, talvez discordando um pouco do Juan, que, mesmo em casos onde não parece que uma evidencia da negação é da forma A --> 0 (ou seja, uma regra que leva uma prova de A em uma contradição), tem-se que, depois de despir a evidencia, ela é, na verdade, da forma A --> 0 e essa é a única maneira construtiva de provar uma negação.
Por exemplo, A := \forall x : N B(x) e B(x) := x =_N 0. Como A não é algo do tipo existencial, parece que dá para provar \neg A exibindo um natural n tal que n \neq 0. Mas aí estão escondidas duas etapas: achar um n : N e provar que \neg (n =_N 0). Mas o que significa uma prova de \neg (n =_N 0)? Aí voltamos as provas do tipo A --> 0 de novo.
O caso do A := "6 é primo" é um pouco diferente. Seja A = \neg B(6), onde B(x) := "x é divisivel por n \neq 1, 0". Então uma prova de 6 =_N 2.3 gera uma prova de B(6) e, portanto, uma prova de \neg \neg B(6) = \neg A. Ou seja, foi encontrada uma prova de B(6) e não de \neg \neg B(6) *diretamente*. Depois essa prova foi transformada em uma regra que leva uma prova de \neg B(6) em uma contradição (usando a regra de introdução que eu escrevi acima). Ou seja, no final, a prova de \neg A é necessariamente do tipo A --> 0. É claro que alguém poderia pensar que uma prova de B(6) *é* uma prova de \neg \neg B(6) (que é o que o Juan mencionou, acho), mas, na minha opinião, ela somente *pode ser vista* como uma prova de \neg \neg B(6).
Caso alguém realmente queira considerar uma prova de B(6) como uma prova de \neg \neg B(6), uma alternativa trivial seria definir a negação de maneira menos uniforme. Uma prova canônica de \neg A seria uma regra que leva uma prova canônica de A em uma contradição ou, caso A = \neg B, uma prova canônica de B. Mas isso fica muito feio...
Abs.,
Fernando
--
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 postar neste grupo, envie um e-mail para logi...@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/CAO6j_Li9hiQJqGbi%2BYPutno6JN0O35T1AWN0oU8cUhfrp8uxOg%40mail.gmail.com.
Reply all
Reply to author
Forward
0 new messages