Re: [Logica-l] um probleminha com logica intuicionista...

[Abner de Mattos Brito]

Prezada Valeria,

Eu não posso fornecer uma resposta completa à sua pergunta por falta de
conhecimento em lógica intuicionista, mas sei que, considerando a
terminologia utilizada no artigo da Wikipedia em questão, duo acostumado a
usar o termo "contra-positiva" desde o primeiro semestre de graduação em
matemática, então a menos que haja, na lógica intuicionista, distinção
entre a tal "contra-positiva" e a contraposição, eu não veria motivo algum
para estranhar o termo empregado.

Curiosamente, o esquema de fórmula em questão,

(\neg B → \neg A) → (A → B)

é o axioma do cálculo proposicional de primeira ordem envolvendo negação,
utilizado por Angelo Margaris em "First Order Matemática Logic", que
estudei em minha iniciação científica.

Atenciosamente,
Abner Brito

On Oct 23, 2017 9:00 PM, "Valeria de Paiva" 
wrote:

> prezados colegas,
>
> estou com um probleminha na wikipedia e em vez de gastar o tempo que
> precisaria pra achar minha copia do Dummett em casa, resolvi apelar pros
> amigos.
>
> Acho que  tem um "erro" em https://en.wikipedia.org/
> wiki/Intuitionistic_logic
> onde  na secao 9 alguem diz que:
>
> Relation to classical logic[edit
> 
> ]
>
> The system of classical logic is obtained by adding any one of the
> following axioms:
>
>- {\displaystyle \phi \lor \lnot \phi }[image: \phi \lor \lnot \phi] (Law
>of the excluded middle. May also be formulated as {\displaystyle (\phi
>\to \chi )\to ((\lnot \phi \to \chi )\to \chi )}[image: (\phi \to \chi
>) \to ((\lnot \phi \to \chi ) \to \chi )].)
>- {\displaystyle \lnot \lnot \phi \to \phi }[image: \lnot \lnot \phi
>\to \phi] (Double negation elimination)
>- {\displaystyle ((\phi \to \chi )\to \phi )\to \phi }[image: ((\phi
>\to \chi ) \to \phi ) \to \phi] (Peirce's law)
>- {\displaystyle (\lnot \phi \to \lnot \chi )\to (\chi \to \phi )}[image:
>{\displaystyle (\lnot \phi \to \lnot \chi )\to (\chi \to \phi )}] (Law
>of contraposition)
>
>
> mas essa ultima assercao nao 'e o que eu chamaria de contraposicao.
> Contraposicao  usual 'e valida em logical intuicionista.
>
> o que acontece e' que essa assercao combina contraposicao com eliminacao
> da negacao dupla, ou seja:
>
> contraposicao devia ser
>
> (A--> B) -->  (\neg B --> neg A)
>
> mas quem escreveu o artigo em vez de dizer
>
> (\neg A-->\neg B) --> (\neg\neg B --> \neg\neg A),
> removeu a dupla negacao, ficando com
> (\neg A-->\neg B) --> ( B -->  A)
>
>  dai que isso 'e  mesmo nao-derivavel em IL, pois inclui double negation
> elimination, junto com a contraposicao.
>
> voces concordam? ou eu estou "esquecendo" alguma coisa importante?
> tem mais alguma coisa errada no artigo?
> eu estou querendo me lembrar da relacao entre implicacao e disjuncao.
> essas estao certas?
>
> Disjunction versus implication:
>
>- {\displaystyle (\phi \vee \psi )\to (\neg \phi \to \psi )}[image:
>(\phi \vee \psi) \to (\neg \phi \to \psi)]
>- {\displaystyle (\neg \phi \vee \psi )\to (\phi \to \psi )}[image:
>(\neg \phi \vee \psi) \to (\phi \to \psi)]
>
>
> obrigada pela ajuda,
> Valeria
> --
> 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+unsubscr...@dimap.ufrn.br.
> Para postar nesse grupo, envie um e-mail para logica-l@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%3DXtQF5fvc8xt%
> 2BaKJ2A5d6bw33taeFkFv0j_PCGJQ6UCSGg%40mail.gmail.com
> 
> .
>

-- 
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/CAAPnweACzeBQqKjVR5jth2Y%3DzmqGmA_Pm4ssOPg5D6vGp%2B3AOA%40mail.gmail.com.

Re: [Logica-l] um probleminha com logica intuicionista...

[Valeria de Paiva]

Alo Thiago,

obrigada por confirmar o que eu disse, isto 'e que

>(A--> B) -->  (\neg B --> neg A)
e' valido em IL e e' o que eu chamo de "contraposition."

e que
>(\neg A-->\neg B) --> ( B -->  A)
não pode ser provado em IL e de fato é equivalente à dupla negação.
e portanto a formula nao deveria ser chamada de Contraposition no artigo na
Wikipedia.
('e um nome ruim, pois essa formula mistura contraposition e eliminacao da
dupla negacao).

mas 'e, eu nao usaria a tripla negacao pra mostrar nada disso nao, pois a
tripla negacao 'e logicamente mais complicada, ne?

obrigada,
Valeria




2017-10-23 16:32 GMT-07:00 Thiago Nascimento da Silva <
thiagnascsi...@gmail.com>:

>  Essa contraposição aqui pode ser provada em IL (A--> B) -->  (\neg B -->
> neg A). Sai basicamente do fato que tu elimina a primeira implicação e
> depois elimina a negação e usa explosão. Essa contraposição aqui (\neg
> A-->\neg B) --> ( B -->  A) não pode ser provada em IL e de fato é
> equivalente à dupla negação. Demonstração: Primeiro note que ¬A -> ¬¬¬A é
> um teorema de IL, agora instancie essa forma de contraposição da seguinte
> maneira (¬A -> ¬¬¬A) ->  (¬¬A -> A), como a primeira parte é axioma, nós
> temos que (¬¬A -> A) é teorema.
>
> Em 23 de outubro de 2017 22:59, Valeria de Paiva <
> valeria.depa...@gmail.com> escreveu:
>
>> prezados colegas,
>>
>> estou com um probleminha na wikipedia e em vez de gastar o tempo que
>> precisaria pra achar minha copia do Dummett em casa, resolvi apelar pros
>> amigos.
>>
>> Acho que  tem um "erro" em https://en.wikipedia.org/wi
>> ki/Intuitionistic_logic
>> onde  na secao 9 alguem diz que:
>>
>> Relation to classical logic[edit
>> 
>> ]
>>
>> The system of classical logic is obtained by adding any one of the
>> following axioms:
>>
>>- {\displaystyle \phi \lor \lnot \phi }[image: \phi \lor \lnot \phi] (Law
>>of the excluded middle. May also be formulated as {\displaystyle
>>(\phi \to \chi )\to ((\lnot \phi \to \chi )\to \chi )}[image: (\phi
>>\to \chi ) \to ((\lnot \phi \to \chi ) \to \chi )].)
>>- {\displaystyle \lnot \lnot \phi \to \phi }[image: \lnot \lnot \phi
>>\to \phi] (Double negation elimination)
>>- {\displaystyle ((\phi \to \chi )\to \phi )\to \phi }[image: ((\phi
>>\to \chi ) \to \phi ) \to \phi] (Peirce's law)
>>- {\displaystyle (\lnot \phi \to \lnot \chi )\to (\chi \to \phi )}[image:
>>{\displaystyle (\lnot \phi \to \lnot \chi )\to (\chi \to \phi )}] (Law
>>of contraposition)
>>
>>
>> mas essa ultima assercao nao 'e o que eu chamaria de contraposicao.
>> Contraposicao  usual 'e valida em logical intuicionista.
>>
>> o que acontece e' que essa assercao combina contraposicao com eliminacao
>> da negacao dupla, ou seja:
>>
>> contraposicao devia ser
>>
>> (A--> B) -->  (\neg B --> neg A)
>>
>> mas quem escreveu o artigo em vez de dizer
>>
>> (\neg A-->\neg B) --> (\neg\neg B --> \neg\neg A),
>> removeu a dupla negacao, ficando com
>> (\neg A-->\neg B) --> ( B -->  A)
>>
>>  dai que isso 'e  mesmo nao-derivavel em IL, pois inclui double negation
>> elimination, junto com a contraposicao.
>>
>> voces concordam? ou eu estou "esquecendo" alguma coisa importante?
>> tem mais alguma coisa errada no artigo?
>> eu estou querendo me lembrar da relacao entre implicacao e disjuncao.
>> essas estao certas?
>>
>> Disjunction versus implication:
>>
>>- {\displaystyle (\phi \vee \psi )\to (\neg \phi \to \psi )}[image:
>>(\phi \vee \psi) \to (\neg \phi \to \psi)]
>>- {\displaystyle (\neg \phi \vee \psi )\to (\phi \to \psi )}[image:
>>(\neg \phi \vee \psi) \to (\phi \to \psi)]
>>
>>
>> obrigada pela ajuda,
>> Valeria
>> --
>> 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+unsubscr...@dimap.ufrn.br.
>> Para postar nesse grupo, envie um e-mail para logica-l@dimap.ufrn.br.
>> Acesse esse grupo em https://groups.google.com/a/di
>> map.ufrn.br/group/logica-l/.
>> Para ver essa discussão na Web, acesse https://groups.google.com/a/di
>> map.ufrn.br/d/msgid/logica-l/CAESt%3DXtQF5fvc8xt%2BaKJ2A5d6
>> bw33taeFkFv0j_PCGJQ6UCSGg%40mail.gmail.com
>> 
>> .
>>
>
>
>
> --
> Thiago Nascimento, Mestrando PPgSC - UFRN.
>
> --
> 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+unsubscr...@dimap.ufrn.br.
> Para postar nesse grupo, envie um e-mail para logica-l@dimap.ufrn.br.
> Acesse esse 

Re: [Logica-l] um probleminha com logica intuicionista...

[Thiago Nascimento da Silva]

 Essa contraposição aqui pode ser provada em IL (A--> B) -->  (\neg B -->
neg A). Sai basicamente do fato que tu elimina a primeira implicação e
depois elimina a negação e usa explosão. Essa contraposição aqui (\neg
A-->\neg B) --> ( B -->  A) não pode ser provada em IL e de fato é
equivalente à dupla negação. Demonstração: Primeiro note que ¬A -> ¬¬¬A é
um teorema de IL, agora instancie essa forma de contraposição da seguinte
maneira (¬A -> ¬¬¬A) ->  (¬¬A -> A), como a primeira parte é axioma, nós
temos que (¬¬A -> A) é teorema.

Em 23 de outubro de 2017 22:59, Valeria de Paiva 
escreveu:

> prezados colegas,
>
> estou com um probleminha na wikipedia e em vez de gastar o tempo que
> precisaria pra achar minha copia do Dummett em casa, resolvi apelar pros
> amigos.
>
> Acho que  tem um "erro" em https://en.wikipedia.org/
> wiki/Intuitionistic_logic
> onde  na secao 9 alguem diz que:
>
> Relation to classical logic[edit
> 
> ]
>
> The system of classical logic is obtained by adding any one of the
> following axioms:
>
>- {\displaystyle \phi \lor \lnot \phi }[image: \phi \lor \lnot \phi] (Law
>of the excluded middle. May also be formulated as {\displaystyle (\phi
>\to \chi )\to ((\lnot \phi \to \chi )\to \chi )}[image: (\phi \to \chi
>) \to ((\lnot \phi \to \chi ) \to \chi )].)
>- {\displaystyle \lnot \lnot \phi \to \phi }[image: \lnot \lnot \phi
>\to \phi] (Double negation elimination)
>- {\displaystyle ((\phi \to \chi )\to \phi )\to \phi }[image: ((\phi
>\to \chi ) \to \phi ) \to \phi] (Peirce's law)
>- {\displaystyle (\lnot \phi \to \lnot \chi )\to (\chi \to \phi )}[image:
>{\displaystyle (\lnot \phi \to \lnot \chi )\to (\chi \to \phi )}] (Law
>of contraposition)
>
>
> mas essa ultima assercao nao 'e o que eu chamaria de contraposicao.
> Contraposicao  usual 'e valida em logical intuicionista.
>
> o que acontece e' que essa assercao combina contraposicao com eliminacao
> da negacao dupla, ou seja:
>
> contraposicao devia ser
>
> (A--> B) -->  (\neg B --> neg A)
>
> mas quem escreveu o artigo em vez de dizer
>
> (\neg A-->\neg B) --> (\neg\neg B --> \neg\neg A),
> removeu a dupla negacao, ficando com
> (\neg A-->\neg B) --> ( B -->  A)
>
>  dai que isso 'e  mesmo nao-derivavel em IL, pois inclui double negation
> elimination, junto com a contraposicao.
>
> voces concordam? ou eu estou "esquecendo" alguma coisa importante?
> tem mais alguma coisa errada no artigo?
> eu estou querendo me lembrar da relacao entre implicacao e disjuncao.
> essas estao certas?
>
> Disjunction versus implication:
>
>- {\displaystyle (\phi \vee \psi )\to (\neg \phi \to \psi )}[image:
>(\phi \vee \psi) \to (\neg \phi \to \psi)]
>- {\displaystyle (\neg \phi \vee \psi )\to (\phi \to \psi )}[image:
>(\neg \phi \vee \psi) \to (\phi \to \psi)]
>
>
> obrigada pela ajuda,
> Valeria
> --
> 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+unsubscr...@dimap.ufrn.br.
> Para postar nesse grupo, envie um e-mail para logica-l@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%3DXtQF5fvc8xt%
> 2BaKJ2A5d6bw33taeFkFv0j_PCGJQ6UCSGg%40mail.gmail.com
> 
> .
>



-- 
Thiago Nascimento, Mestrando PPgSC - UFRN.

-- 
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/CAOHRVBVYL6xH5E%3D7ni-_sH0pMxwEdwQD-Q265E_KxeLZJM%2B-sw%40mail.gmail.com.

[Logica-l] um probleminha com logica intuicionista...

[Valeria de Paiva]

prezados colegas,

estou com um probleminha na wikipedia e em vez de gastar o tempo que
precisaria pra achar minha copia do Dummett em casa, resolvi apelar pros
amigos.

Acho que  tem um "erro" em
https://en.wikipedia.org/wiki/Intuitionistic_logic
onde  na secao 9 alguem diz que:

Relation to classical logic[edit

]

The system of classical logic is obtained by adding any one of the
following axioms:

   - {\displaystyle \phi \lor \lnot \phi }[image: \phi \lor \lnot \phi] (Law
   of the excluded middle. May also be formulated as {\displaystyle (\phi
   \to \chi )\to ((\lnot \phi \to \chi )\to \chi )}[image: (\phi \to \chi )
   \to ((\lnot \phi \to \chi ) \to \chi )].)
   - {\displaystyle \lnot \lnot \phi \to \phi }[image: \lnot \lnot \phi \to
   \phi] (Double negation elimination)
   - {\displaystyle ((\phi \to \chi )\to \phi )\to \phi }[image: ((\phi \to
   \chi ) \to \phi ) \to \phi] (Peirce's law)
   - {\displaystyle (\lnot \phi \to \lnot \chi )\to (\chi \to \phi )}[image:
   {\displaystyle (\lnot \phi \to \lnot \chi )\to (\chi \to \phi )}] (Law
   of contraposition)


mas essa ultima assercao nao 'e o que eu chamaria de contraposicao.
Contraposicao  usual 'e valida em logical intuicionista.

o que acontece e' que essa assercao combina contraposicao com eliminacao da
negacao dupla, ou seja:

contraposicao devia ser

(A--> B) -->  (\neg B --> neg A)

mas quem escreveu o artigo em vez de dizer

(\neg A-->\neg B) --> (\neg\neg B --> \neg\neg A),
removeu a dupla negacao, ficando com
(\neg A-->\neg B) --> ( B -->  A)

 dai que isso 'e  mesmo nao-derivavel em IL, pois inclui double negation
elimination, junto com a contraposicao.

voces concordam? ou eu estou "esquecendo" alguma coisa importante?
tem mais alguma coisa errada no artigo?
eu estou querendo me lembrar da relacao entre implicacao e disjuncao.
essas estao certas?

Disjunction versus implication:

   - {\displaystyle (\phi \vee \psi )\to (\neg \phi \to \psi )}[image:
   (\phi \vee \psi) \to (\neg \phi \to \psi)]
   - {\displaystyle (\neg \phi \vee \psi )\to (\phi \to \psi )}[image:
   (\neg \phi \vee \psi) \to (\phi \to \psi)]


obrigada pela ajuda,
Valeria
-- 
Valeria de Paiva
http://vcvpaiva.github.io/
http://research.nuance.com/author/valeria-de-paiva/
http://www.cs.bham.ac.uk/~vdp/

-- 
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/CAESt%3DXtQF5fvc8xt%2BaKJ2A5d6bw33taeFkFv0j_PCGJQ6UCSGg%40mail.gmail.com.