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

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

2017-10-27 Por tôpico Bruno Bentzen

Caros,

Antes tarde do que nunca, talvez caibam aqui duas breves observações históricas 
interessantes sobre os pontos (3) e (4) da primeira mensagem do Chico: 

>3) Estou insistindo em incluir o nome do Arend pois afinal nem sempre nos 
>lembramos que o Brower tinha a firme opinião que a sua visão da Lógica era 
>impossível (por definição, já que envolvia a "prática quotidiana dos 
>matemáticos") de ser axiomatizada. 

Ao contrário do que possa parecer inicialmente, a recepção do Brouwer da 
formalização da lógica intuicionística de seu estudante Heyting (1928) foi 
extremamente positiva! Inclusive, foi através de seu encorajamento que o 
Heyting viria a publicar a versão revisada do manuscrito (1930). A entrada a 
seguir da SEP contém mais detalhes a respeito.

https://plato.stanford.edu/entries/intuitionistic-logic-development/#4

>4) Interessante observar que posições filosóficas não se materializam na 
>"prática quotidiana dos matemáticos": um dos resultados mais conhecidos de 
>Brower (toda função contínua do disco de dimensão n em   
sí mesmo possui ponto fixo) é estabelecido pelo próprio por contradição! O 
primeiro passo da contradição já é de ordem grande: não há retração 
contínua do disco em sua borda (em qualquer dimensão n maior ou igual a 1), o 
que exige métodos homológicos ou homotópicos); exibir o ponto   
fixo: "para com isso"

Recordo de haver lido em algum lugar, mas não me lembro exatamente onde (talvez 
os colegas possam nos informar?), que as contribuições clássicas do Brouwer, 
como o teorema do ponto fixo (1910) e da invariancia do domínio (1912) nunca 
foram consideradas por ele como resultados válidos matematicamente, mas apenas 
como publicações estratégicas com o fim de ser bem aceito pela comunidade 
matemática antes de lançar o seu programa intuicionista (oficialmente 
apresentado tambem em 1912, mas já muito bem esboçado em 1907 na sua 
dissertação).

Abraços lógicos,
Bruno

--
Bruno Bentzen
https://sites.google.com/site/bbentzena/

-- 
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/d3e1aad8-4cde-48fe-9fcb-b603e2e2e8cb%40dimap.ufrn.br.

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

2017-10-27 Por tôpico Bruno Bentzen

Oi Valéria,

Não tem problema :)

>acho que seria legal se a gente unisse os esforcos pra fazer todos os 
>lambda-termos pros teoremas intuicionistas do Kleene em (S. C. Kleene. 
>Introduction to metamathematics, volume 1 of Bibliotheca mathematica. 
>NorthHolland Publishing Co., 1952.). 

Essa me parece uma ótima ideia! Atualmente o Cubo prova todos os teoremas da 
lógica proposicional intuicionística (e clássica, via e.g. a inclusão da lei do 
terceiro excluído no contexto de premissas) e também realiza quaisquer 
operações aritméticas e booleanas que não envolvem tipos dependentes.

Para provar o resto dos teoremas do Kleene, no entanto, precisariamos de 
dependência de tipos e tipos de identidade - o que é bom, pois esse é o 
objetivo a longo prazo. Tenho algumas ideias de como estender o sistema, mas no 
momento me falta tempo livre para sentar e me preparar para a inevitável dor de 
cabeça :)

Abraços lógicos,
Bruno

--
Bruno Bentzen
https://sites.google.com/site/bbentzena/

-- 
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/d021bed4-6cde-4494-a331-b79a95e04678%40dimap.ufrn.br.

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

2017-10-25 Por tôpico Fernando Yamauti

 Oi Valéria,

 Obrigado pelas referências. O Chico respondeu sim. Pelas suas referencias
ficou mais claro: são só (bi)hiperdoutrinas de categorias bicartesianas
fechadas e cocartesianamente cofechadas (nome muito grande!). Nem sabia que
isso tinha utilidade. O caso monoidal parece ser mais interessante, mas
mesmo o caso (co)cartesiano parece que não implica ser uma algebra Booleana
nessas referencias. Portanto algum axioma da diferença simétrica que o
Chico usa não deve valer nessas categorias.

 Abs.

Em 25 de outubro de 2017 20:51, Valeria de Paiva 
escreveu:

> oi Fernando,
> provavelmente o Chico ja respondeu, mas se nao, de uma olhada em
> https://arxiv.org/abs/1708.05896
> A Cointuitionistic Adjoint Logic
>
> ou Crolard's papers:
>
>
>-
>
>“A formulae-as-types interpretation of Subtractive Logic
>”. T. Crolard. 
> *Journal
>of Logic and Computation. Special issue on Intuitionistic Modal Logic and
>Application.* Volume 14, Issue 4, August 2004. pp 529-570.
>
>*Abstract.* We present a formulae-as-types interpretation of
>Subtractive Logic (*i.e.* bi-intuitionistic logic). This presentation
>is two-fold: we first define a very natural restriction of the λμ-calculus
>which is closed under reduction and whose type system is a constructive
>restriction of the Classical Natural Deduction. Then we extend this
>deduction system conservatively to Subtractive Logic. From a computational
>standpoint, the resulting calculus provides a type system for first-class
>coroutines (a restricted form of first-class continuations).
>-
>
>“Subtractive logic
>”. T. Crolard. 
> *Theoretical
>Computer Science* 254:1–2(2001):151-185.*Abstract.* This paper is the
>first part of a work whose purpose is to investigate duality in some
>related frameworks (cartesian closed categories, lambda-calculi,
>intuitionistic and classical logics) from syntactic, semantical and
>computational viewpoints. We start with category theory and we show that
>any bicartesian closed category with coexponents is degenerated (i.e. there
>is at most one arrow between two objects). The remainder of the paper is
>devoted to logical issues. We examine the propositional calculus underlying
>the type system of bicartesian closed categories with coexponents and we
>show that this calculus corresponds to subtractive logic: a conservative
>extension of intuitionistic logic with a new connector (subtraction) dual
>to implication. Eventually, we consider first order subtractive logic and
>we present an embedding of classical logic into subtractive logic.
>
> abs
> Valeria
>
> 2017-10-25 3:21 GMT-07:00 Fernando Yamauti :
>
>>  Oi Chico,
>>
>>  Só uma pergunta idiota. Que adjunção entre a diferença simétrica e a
>> disjunção (que voce havia citado) é essa? Suponho que deva ser algo que
>> vale em qualquer topos Booleano, mas mesmo em Set algo do tipo  (-) \vee A
>> -| (-)  \Delta A  (ou o contrario), onde ambos endofuntores são entre o
>> reticulado dos subobjetos,  não parece ser verdade. Portanto acho que voce
>> esta pensando em algo menos obvio que isso, mas não consegui descobrir o
>> que é...
>>
>>  Abs.
>>
>>
>> Em 24 de outubro de 2017 04:08, Francisco Miraglia 
>> escreveu:
>>
>>> Cara Valéria,
>>>
>>> Observações que talvez possam ser úteis:
>>>
>>> 1) O esquema (A --> B) --> (Ng A --> Ng B) é válido no Intucionismo,
>>> (versão Heyting); as álgebras de Heyting fornecem uma semântica completa
>>> para a versão do Intuicionismo do Arend;
>>>
>>> 2) Adicionar o esquema recíproco à axiomatização de Heyting da Lógica
>>> Intucionista imediatamente fornece a Lógica Clássica; é semelhante ao
>>> que acontece com a equivalência no sistema Intuicionista: se for
>>> distributiva, a Lógica é clássica.
>>>
>>> 3) Estou insistindo em incluir o nome do Arend pois afinal nem sempre
>>> nos lembramos que o Brower tinha a firme opinião que a sua visão da
>>> Lógica era impossível (por definição, já que envolvia a "prática
>>> quotidiana dos matemáticos") de ser axiomatizada.
>>>
>>> 4) Interessante observar que posições filosóficas não se materializam
>>> na "prática quotidiana dos matemáticos": um dos resultados mais conhecidos
>>> de Brower (toda função contínua do disco de dimensão n em sí mesmo possui
>>> ponto fixo) é estabelecido pelo próprio por contradição!
>>> O primeiro passo da contradição já é de ordem grande: não há retração
>>> contínua do disco em sua borda (em qualquer dimensão n maior ou igual a
>>> 1), o que exige métodos homológicos ou homotópicos); exibir o ponto fixo:
>>> "para com isso"
>>>
>>> 5) Quanto à nomenclatura, tanto Heyting, quanto Kleene (e Vesley)  dão o
>>> nome de contraposição ao esquema em (1), sempre chamando a atenção de que ,
>>> no

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

2017-10-25 Por tôpico Valeria de Paiva

oi Bruno,
desculpe a demora. (quarta-feira 'e um dia complicado por aqui, sua
mensagem foi overlooked...)

mas sim, achei muito BOM ver o seu Cubo e os lambda-termos pra essas 40
derivacoes:

>Uma lista razoável com provas de mais de 40 proposições válidas
intuicionisticamente (incluindo grande parte dos teoremas listados na
entrada citada da Wikipedia) pode ser achada nesta mini biblioteca
 do Cubo. A sintaxe
do sistema é brevemente explicada aqui
. Quaisquer
comentários são bem-vindos. :)

acho que seria legal se a gente unisse os esforcos pra fazer todos os
lambda-termos pros teoremas intuicionistas do Kleene em (S. C. Kleene.
Introduction to metamathematics, volume 1 of Bibliotheca mathematica.
NorthHolland Publishing Co., 1952.).

Eu e a Sara Kalvala usamos esses teoremas intuicionistas faceizinhos do
Kleeene em
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.97.3475=rep1=pdf
pra comecar a pensar numa testsuite de teoremas de Logica Linear.

o que 'e mais interessante aqui 'e pensar nas varias maneiras de adicionar
!'s que fazem os teoremas de IL verdadeiros em LL, isso foi a tese do
Harold Schellinx (
The noble art of linear decorating ) que 'e super interessante!!
abs
Valeria

2017-10-25 15:51 GMT-07:00 Valeria de Paiva :

> oi Fernando,
> provavelmente o Chico ja respondeu, mas se nao, de uma olhada em
> https://arxiv.org/abs/1708.05896
> A Cointuitionistic Adjoint Logic
>
> ou Crolard's papers:
>
>
>-
>
>“A formulae-as-types interpretation of Subtractive Logic
>”. T. Crolard. 
> *Journal
>of Logic and Computation. Special issue on Intuitionistic Modal Logic and
>Application.* Volume 14, Issue 4, August 2004. pp 529-570.
>
>*Abstract.* We present a formulae-as-types interpretation of
>Subtractive Logic (*i.e.* bi-intuitionistic logic). This presentation
>is two-fold: we first define a very natural restriction of the λμ-calculus
>which is closed under reduction and whose type system is a constructive
>restriction of the Classical Natural Deduction. Then we extend this
>deduction system conservatively to Subtractive Logic. From a computational
>standpoint, the resulting calculus provides a type system for first-class
>coroutines (a restricted form of first-class continuations).
>-
>
>“Subtractive logic
>”. T. Crolard. 
> *Theoretical
>Computer Science* 254:1–2(2001):151-185.*Abstract.* This paper is the
>first part of a work whose purpose is to investigate duality in some
>related frameworks (cartesian closed categories, lambda-calculi,
>intuitionistic and classical logics) from syntactic, semantical and
>computational viewpoints. We start with category theory and we show that
>any bicartesian closed category with coexponents is degenerated (i.e. there
>is at most one arrow between two objects). The remainder of the paper is
>devoted to logical issues. We examine the propositional calculus underlying
>the type system of bicartesian closed categories with coexponents and we
>show that this calculus corresponds to subtractive logic: a conservative
>extension of intuitionistic logic with a new connector (subtraction) dual
>to implication. Eventually, we consider first order subtractive logic and
>we present an embedding of classical logic into subtractive logic.
>
> abs
> Valeria
>
> 2017-10-25 3:21 GMT-07:00 Fernando Yamauti :
>
>>  Oi Chico,
>>
>>  Só uma pergunta idiota. Que adjunção entre a diferença simétrica e a
>> disjunção (que voce havia citado) é essa? Suponho que deva ser algo que
>> vale em qualquer topos Booleano, mas mesmo em Set algo do tipo  (-) \vee A
>> -| (-)  \Delta A  (ou o contrario), onde ambos endofuntores são entre o
>> reticulado dos subobjetos,  não parece ser verdade. Portanto acho que voce
>> esta pensando em algo menos obvio que isso, mas não consegui descobrir o
>> que é...
>>
>>  Abs.
>>
>>
>> Em 24 de outubro de 2017 04:08, Francisco Miraglia 
>> escreveu:
>>
>>> Cara Valéria,
>>>
>>> Observações que talvez possam ser úteis:
>>>
>>> 1) O esquema (A --> B) --> (Ng A --> Ng B) é válido no Intucionismo,
>>> (versão Heyting); as álgebras de Heyting fornecem uma semântica completa
>>> para a versão do Intuicionismo do Arend;
>>>
>>> 2) Adicionar o esquema recíproco à axiomatização de Heyting da Lógica
>>> Intucionista imediatamente fornece a Lógica Clássica; é semelhante ao
>>> que acontece com a equivalência no sistema Intuicionista: se for
>>> distributiva, a Lógica é clássica.
>>>
>>> 3) Estou insistindo em incluir o nome do Arend pois afinal nem sempre
>>> nos lembramos que o Brower tinha a firme opinião que a sua visão da
>>> Lógica era impossível (por

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

2017-10-25 Por tôpico Valeria de Paiva

oi Fernando,
provavelmente o Chico ja respondeu, mas se nao, de uma olhada em
https://arxiv.org/abs/1708.05896
A Cointuitionistic Adjoint Logic

ou Crolard's papers:


   -

   “A formulae-as-types interpretation of Subtractive Logic
   ”. T.
Crolard. *Journal
   of Logic and Computation. Special issue on Intuitionistic Modal Logic and
   Application.* Volume 14, Issue 4, August 2004. pp 529-570.

   *Abstract.* We present a formulae-as-types interpretation of Subtractive
   Logic (*i.e.* bi-intuitionistic logic). This presentation is two-fold:
   we first define a very natural restriction of the λμ-calculus which is
   closed under reduction and whose type system is a constructive restriction
   of the Classical Natural Deduction. Then we extend this deduction system
   conservatively to Subtractive Logic. From a computational standpoint, the
   resulting calculus provides a type system for first-class coroutines (a
   restricted form of first-class continuations).
   -

   “Subtractive logic
   ”. T.
Crolard. *Theoretical
   Computer Science* 254:1–2(2001):151-185.*Abstract.* This paper is the
   first part of a work whose purpose is to investigate duality in some
   related frameworks (cartesian closed categories, lambda-calculi,
   intuitionistic and classical logics) from syntactic, semantical and
   computational viewpoints. We start with category theory and we show that
   any bicartesian closed category with coexponents is degenerated (i.e. there
   is at most one arrow between two objects). The remainder of the paper is
   devoted to logical issues. We examine the propositional calculus underlying
   the type system of bicartesian closed categories with coexponents and we
   show that this calculus corresponds to subtractive logic: a conservative
   extension of intuitionistic logic with a new connector (subtraction) dual
   to implication. Eventually, we consider first order subtractive logic and
   we present an embedding of classical logic into subtractive logic.

abs
Valeria

2017-10-25 3:21 GMT-07:00 Fernando Yamauti :

>  Oi Chico,
>
>  Só uma pergunta idiota. Que adjunção entre a diferença simétrica e a
> disjunção (que voce havia citado) é essa? Suponho que deva ser algo que
> vale em qualquer topos Booleano, mas mesmo em Set algo do tipo  (-) \vee A
> -| (-)  \Delta A  (ou o contrario), onde ambos endofuntores são entre o
> reticulado dos subobjetos,  não parece ser verdade. Portanto acho que voce
> esta pensando em algo menos obvio que isso, mas não consegui descobrir o
> que é...
>
>  Abs.
>
>
> Em 24 de outubro de 2017 04:08, Francisco Miraglia 
> escreveu:
>
>> Cara Valéria,
>>
>> Observações que talvez possam ser úteis:
>>
>> 1) O esquema (A --> B) --> (Ng A --> Ng B) é válido no Intucionismo,
>> (versão Heyting); as álgebras de Heyting fornecem uma semântica completa
>> para a versão do Intuicionismo do Arend;
>>
>> 2) Adicionar o esquema recíproco à axiomatização de Heyting da Lógica
>> Intucionista imediatamente fornece a Lógica Clássica; é semelhante ao que
>> acontece com a equivalência no sistema Intuicionista: se for distributiva,
>> a Lógica é clássica.
>>
>> 3) Estou insistindo em incluir o nome do Arend pois afinal nem sempre nos
>> lembramos que o Brower tinha a firme opinião que a sua visão da
>> Lógica era impossível (por definição, já que envolvia a "prática
>> quotidiana dos matemáticos") de ser axiomatizada.
>>
>> 4) Interessante observar que posições filosóficas não se materializam  na
>> "prática quotidiana dos matemáticos": um dos resultados mais conhecidos de
>> Brower (toda função contínua do disco de dimensão n em sí mesmo possui
>> ponto fixo) é estabelecido pelo próprio por contradição!
>> O primeiro passo da contradição já é de ordem grande: não há retração
>> contínua do disco em sua borda (em qualquer dimensão n maior ou igual a
>> 1), o que exige métodos homológicos ou homotópicos); exibir o ponto fixo:
>> "para com isso"
>>
>> 5) Quanto à nomenclatura, tanto Heyting, quanto Kleene (e Vesley)  dão o
>> nome de contraposição ao esquema em (1), sempre chamando a atenção de que ,
>> no Intuicionismo segundo Arend, difere da regra de contraposição clássica,
>> que, em geral, é  enunciada como o esquema "contrapositivo", mencionado em
>> (2).
>>
>> (6) Não me lembro de ler acerca dessas coisas no livro do Dummet (mas
>> também não foi lá que aprendi a lidar com o intuicionismo do Arend), porém
>> sabes como é: a memória não é mais o que era, sendo substituída pela
>> "prática quotidiana" de utilizar metateoria intuicionista para fazer
>> Matemática. Exemplo: anéis de Gelfand (aqueles comutativos com unidade tais
>> que que por cima de todo ideal há apenas um maximal) são,
>> intuicionisticamente, fielmente quadráticos (possuem uma teoria de formas
>> quadráticas "bem comportada" e satisfazem a conjectura

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

2017-10-25 Por tôpico Fernando Yamauti

 Oi Chico,

 Só uma pergunta idiota. Que adjunção entre a diferença simétrica e a
disjunção (que voce havia citado) é essa? Suponho que deva ser algo que
vale em qualquer topos Booleano, mas mesmo em Set algo do tipo  (-) \vee A
-| (-)  \Delta A  (ou o contrario), onde ambos endofuntores são entre o
reticulado dos subobjetos,  não parece ser verdade. Portanto acho que voce
esta pensando em algo menos obvio que isso, mas não consegui descobrir o
que é...

 Abs.


Em 24 de outubro de 2017 04:08, Francisco Miraglia 
escreveu:

> Cara Valéria,
>
> Observações que talvez possam ser úteis:
>
> 1) O esquema (A --> B) --> (Ng A --> Ng B) é válido no Intucionismo,
> (versão Heyting); as álgebras de Heyting fornecem uma semântica completa
> para a versão do Intuicionismo do Arend;
>
> 2) Adicionar o esquema recíproco à axiomatização de Heyting da Lógica
> Intucionista imediatamente fornece a Lógica Clássica; é semelhante ao que
> acontece com a equivalência no sistema Intuicionista: se for distributiva,
> a Lógica é clássica.
>
> 3) Estou insistindo em incluir o nome do Arend pois afinal nem sempre nos
> lembramos que o Brower tinha a firme opinião que a sua visão da
> Lógica era impossível (por definição, já que envolvia a "prática
> quotidiana dos matemáticos") de ser axiomatizada.
>
> 4) Interessante observar que posições filosóficas não se materializam  na
> "prática quotidiana dos matemáticos": um dos resultados mais conhecidos de
> Brower (toda função contínua do disco de dimensão n em sí mesmo possui
> ponto fixo) é estabelecido pelo próprio por contradição!
> O primeiro passo da contradição já é de ordem grande: não há retração
> contínua do disco em sua borda (em qualquer dimensão n maior ou igual a
> 1), o que exige métodos homológicos ou homotópicos); exibir o ponto fixo:
> "para com isso"
>
> 5) Quanto à nomenclatura, tanto Heyting, quanto Kleene (e Vesley)  dão o
> nome de contraposição ao esquema em (1), sempre chamando a atenção de que ,
> no Intuicionismo segundo Arend, difere da regra de contraposição clássica,
> que, em geral, é  enunciada como o esquema "contrapositivo", mencionado em
> (2).
>
> (6) Não me lembro de ler acerca dessas coisas no livro do Dummet (mas
> também não foi lá que aprendi a lidar com o intuicionismo do Arend), porém
> sabes como é: a memória não é mais o que era, sendo substituída pela
> "prática quotidiana" de utilizar metateoria intuicionista para fazer
> Matemática. Exemplo: anéis de Gelfand (aqueles comutativos com unidade tais
> que que por cima de todo ideal há apenas um maximal) são,
> intuicionisticamente, fielmente quadráticos (possuem uma teoria de formas
> quadráticas "bem comportada" e satisfazem a conjectura de Milnor). Isto já
> é meio complicado; o caso clássico (que penso também ser verdadeiro) parece
> ser ainda mais complicado. Interessante que os meus colegas de formas
> quadráticas e K-teoria não dão a menor importância para a informação
> intuicionista...
>
> (7) A relação intucionista da disjunção com a implicação resume-se ao
> óbvio; qualquer outra relação é FALSA (experimente nos abertos da reta
> real). Ou seja, na minha opinião, "barking up the wrong tree".
>
> Como voce sabe muito bem, o modo mais adequado de tratar estes conceitos é
> via adjunções: a implicação é  adjunta da conjunção, enquanto que a
> disjunção é, classicamente, adjunta da diferença simétrica (o complementar
> clássico da equivalência); porém esta última adjunção está longe de ser
> intuicionisticamente válida. Aliás, se um reticulado distribitivo possui
> uma operação parecida com a diferença simétrica, tem que ser uma álgebra de
> Boole. Aqui começam a aparecer diferenças conceituais importantes e a
> necessidade de empregar
> outras noções, mais gerais (e.g., functores adjuntos), para construir
> Lógicas. Já escrevi demais
>
>
> Um grande abraço,
>
> Chico Miraglia
>
>
>
>
>
>
>> 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
>>> >> logic=edit=9>
>>> ]
>>>
>>> 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

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

2017-10-24 Por tôpico Francisco Miraglia


Cara Valéria,

Infelizmente, não há atalhos para os anéis de Gelfand; entretanto,  
exemplares importantes são os anéis (ou álgebras) de funções reais  
contínuas sobre um espaço compacto Hausdorff. Só aí já da para ter uma  
idéia da complexidade. Por sinal, para estes a resposta à pergunta
que mencionei  é verdade e a longa prova consta do novo Memoirs meu e  
do Max  que saiu recentemente (nov/16) sobre a teoria abstrata de  
formas quadráticas e aplicações à Teoria de Anéis.


Em relação ao Cálculo Proposicional de 2ª ordem, a escola polonesa dos  
anos 20 considerava quantificação universal sobre proposições como  
completamente natural (veja a tese de doutorado de A. Tarski;  
orientador: Leśniewski). Há muita informação acerca do assunto no meu  
livro com o Ken López Escobar: "Definitions the primitive concepts of  
Logics the Leśniewski-Tarski legacy",  Dissertationes Math. 401,  
Polish Academy of Science, 2002.


Outro abraço,

Chico


Quoting Valeria de Paiva :


Concordo completamente com o Marcelo: Chico, por favor  escreva mais!

(gostaria de entender o exemplo " anéis de Gelfand (aqueles comutativos com
unidade tais que que por cima de todo ideal há apenas um maximal) são,
intuicionisticamente, fielmente quadráticos (possuem uma teoria de formas
quadráticas "bem comportada" e satisfazem a conjectura de Milnor)", esta'
explicado em algum lugar facil?)


e obrigada Hermogenes  pela mensagem clara e pelo plug pra palestra da
Elaine.

e sim, Hermogenes  eu tb gosto muito dessa traducao que o Peter Aczel
chamou de "Russell-Prawitz" em
*The Russell–Prawitz modality*
(Author: Peter Aczel

Departments
of Mathematics and Computer Science, Manchester University, Manchester M13
9PL, England

tem uma versao prepint no site do Aczel,
The Russell-Prawitz Modality - School of Computer Science - The ...

www.cs.man.ac.uk/~petera/russ-praw.ps.gz)

mas e' bem mais complicada ne? voce precisa achar facil falar de
quantificacao sobre todas as proposicoes,
o que eu nao acho muito facil nao.

finalmente obrigada Elaine pela discussao. estamos todos de acordo sobre o
que e' provavel
na logica propositional intuicionista do Heyting. so estamos discordando de
nomes,
(bom e eu estou reclamando pois sistemas de axiomas sempre confundem as
coisas colocando muitas ideias numa
formulinha so') e pelo menos o Hermogenes concorda comigo!

abs e obrigada,
Valeria

2017-10-24 6:24 GMT-07:00 Valeria de Paiva :


oi Chico,

"typo" na primeira linha da sua mensagem
>O esquema (A --> B) --> (Ng A --> Ng B) é válido no Intucionismo, (versão
Heyting);
voce quiz dizer
(A --> B) --> (Ng B --> Ng A),
certo?

e sim, gosto bastante das algebras de Heyting e claro que concordo
totalmente com:

>Como voce sabe muito bem, o modo mais adequado de tratar estes conceitos
é via adjunções: a implicação é  adjunta da conjunção, enquanto que a
disjunção é, classicamente, adjunta da diferença simétrica (o complementar
clássico da equivalência); porém esta última adjunção está longe de ser
intuicionisticamente válida.

mas e', a discussao sobre o adjunto da disjuncao 'e grande e dificil. e
pra mim nao faz parte dessa conversa menorzinha, do que 'e valido pro
Heyting e de que nomes devem ser usados pra que.

obrigada tb por
>A relação intucionista da disjunção com a implicação resume-se ao óbvio;
qualquer outra relação é FALSA
era isso mesmo que eu queria verificar.

abracos,
Valeria

2017-10-23 23:08 GMT-07:00 Francisco Miraglia :


Cara Valéria,

Observações que talvez possam ser úteis:

1) O esquema (A --> B) --> (Ng A --> Ng B) é válido no Intucionismo,
(versão Heyting); as álgebras de Heyting fornecem uma semântica completa
para a versão do Intuicionismo do Arend;

2) Adicionar o esquema recíproco à axiomatização de Heyting da Lógica
Intucionista imediatamente fornece a Lógica Clássica; é semelhante ao que
acontece com a equivalência no sistema Intuicionista: se for distributiva,
a Lógica é clássica.

3) Estou insistindo em incluir o nome do Arend pois afinal nem sempre nos
lembramos que o Brower tinha a firme opinião que a sua visão da
Lógica era impossível (por definição, já que envolvia a "prática
quotidiana dos matemáticos") de ser axiomatizada.

4) Interessante observar que posições filosóficas não se materializam  na
"prática quotidiana dos matemáticos": um dos resultados mais conhecidos de
Brower (toda função contínua do disco de dimensão n em sí mesmo possui
ponto fixo) é estabelecido pelo próprio por contradição!
O primeiro passo da contradição já é de ordem grande: não há retração
contínua do disco em sua borda (em qualquer dimensão n maior ou

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

2017-10-24 Por tôpico Francisco Miraglia


Cara Valéria,

Voce tem razão acerca do "typo". Quanto à adjunção associada à  
disjunção, esta é a razão de ter te enviado o texto...


Um abraço,

Chico Miraglia


Quoting Valeria de Paiva :


oi Chico,

"typo" na primeira linha da sua mensagem

O esquema (A --> B) --> (Ng A --> Ng B) é válido no Intucionismo, (versão

Heyting);
voce quiz dizer
(A --> B) --> (Ng B --> Ng A),
certo?

e sim, gosto bastante das algebras de Heyting e claro que concordo
totalmente com:


Como voce sabe muito bem, o modo mais adequado de tratar estes conceitos é

via adjunções: a implicação é  adjunta da conjunção, enquanto que a
disjunção é, classicamente, adjunta da diferença simétrica (o complementar
clássico da equivalência); porém esta última adjunção está longe de ser
intuicionisticamente válida.

mas e', a discussao sobre o adjunto da disjuncao 'e grande e dificil. e pra
mim nao faz parte dessa conversa menorzinha, do que 'e valido pro Heyting e
de que nomes devem ser usados pra que.

obrigada tb por

A relação intucionista da disjunção com a implicação resume-se ao óbvio;

qualquer outra relação é FALSA
era isso mesmo que eu queria verificar.

abracos,
Valeria

2017-10-23 23:08 GMT-07:00 Francisco Miraglia :


Cara Valéria,

Observações que talvez possam ser úteis:

1) O esquema (A --> B) --> (Ng A --> Ng B) é válido no Intucionismo,
(versão Heyting); as álgebras de Heyting fornecem uma semântica completa
para a versão do Intuicionismo do Arend;

2) Adicionar o esquema recíproco à axiomatização de Heyting da Lógica
Intucionista imediatamente fornece a Lógica Clássica; é semelhante ao que
acontece com a equivalência no sistema Intuicionista: se for distributiva,
a Lógica é clássica.

3) Estou insistindo em incluir o nome do Arend pois afinal nem sempre nos
lembramos que o Brower tinha a firme opinião que a sua visão da
Lógica era impossível (por definição, já que envolvia a "prática
quotidiana dos matemáticos") de ser axiomatizada.

4) Interessante observar que posições filosóficas não se materializam  na
"prática quotidiana dos matemáticos": um dos resultados mais conhecidos de
Brower (toda função contínua do disco de dimensão n em sí mesmo possui
ponto fixo) é estabelecido pelo próprio por contradição!
O primeiro passo da contradição já é de ordem grande: não há retração
contínua do disco em sua borda (em qualquer dimensão n maior ou igual a
1), o que exige métodos homológicos ou homotópicos); exibir o ponto fixo:
"para com isso"

5) Quanto à nomenclatura, tanto Heyting, quanto Kleene (e Vesley)  dão o
nome de contraposição ao esquema em (1), sempre chamando a atenção de que ,
no Intuicionismo segundo Arend, difere da regra de contraposição clássica,
que, em geral, é  enunciada como o esquema "contrapositivo", mencionado em
(2).

(6) Não me lembro de ler acerca dessas coisas no livro do Dummet (mas
também não foi lá que aprendi a lidar com o intuicionismo do Arend), porém
sabes como é: a memória não é mais o que era, sendo substituída pela
"prática quotidiana" de utilizar metateoria intuicionista para fazer
Matemática. Exemplo: anéis de Gelfand (aqueles comutativos com unidade tais
que que por cima de todo ideal há apenas um maximal) são,
intuicionisticamente, fielmente quadráticos (possuem uma teoria de formas
quadráticas "bem comportada" e satisfazem a conjectura de Milnor). Isto já
é meio complicado; o caso clássico (que penso também ser verdadeiro) parece
ser ainda mais complicado. Interessante que os meus colegas de formas
quadráticas e K-teoria não dão a menor importância para a informação
intuicionista...

(7) A relação intucionista da disjunção com a implicação resume-se ao
óbvio; qualquer outra relação é FALSA (experimente nos abertos da reta
real). Ou seja, na minha opinião, "barking up the wrong tree".

Como voce sabe muito bem, o modo mais adequado de tratar estes conceitos é
via adjunções: a implicação é  adjunta da conjunção, enquanto que a
disjunção é, classicamente, adjunta da diferença simétrica (o complementar
clássico da equivalência); porém esta última adjunção está longe de ser
intuicionisticamente válida. Aliás, se um reticulado distribitivo possui
uma operação parecida com a diferença simétrica, tem que ser uma álgebra de
Boole. Aqui começam a aparecer diferenças conceituais importantes e a
necessidade de empregar
outras noções, mais gerais (e.g., functores adjuntos), para construir
Lógicas. Já escrevi demais


Um grande abraço,

Chico Miraglia







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

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

2017-10-24 Por tôpico Valeria de Paiva

 Concordo completamente com o Marcelo: Chico, por favor  escreva mais!

(gostaria de entender o exemplo " anéis de Gelfand (aqueles comutativos com
unidade tais que que por cima de todo ideal há apenas um maximal) são,
intuicionisticamente, fielmente quadráticos (possuem uma teoria de formas
quadráticas "bem comportada" e satisfazem a conjectura de Milnor)", esta'
explicado em algum lugar facil?)


e obrigada Hermogenes  pela mensagem clara e pelo plug pra palestra da
Elaine.

e sim, Hermogenes  eu tb gosto muito dessa traducao que o Peter Aczel
chamou de "Russell-Prawitz" em
*The Russell–Prawitz modality*
(Author: Peter Aczel

Departments
of Mathematics and Computer Science, Manchester University, Manchester M13
9PL, England

tem uma versao prepint no site do Aczel,
The Russell-Prawitz Modality - School of Computer Science - The ...

www.cs.man.ac.uk/~petera/russ-praw.ps.gz)

mas e' bem mais complicada ne? voce precisa achar facil falar de
quantificacao sobre todas as proposicoes,
o que eu nao acho muito facil nao.

finalmente obrigada Elaine pela discussao. estamos todos de acordo sobre o
que e' provavel
na logica propositional intuicionista do Heyting. so estamos discordando de
nomes,
(bom e eu estou reclamando pois sistemas de axiomas sempre confundem as
coisas colocando muitas ideias numa
formulinha so') e pelo menos o Hermogenes concorda comigo!

abs e obrigada,
Valeria

2017-10-24 6:24 GMT-07:00 Valeria de Paiva :

> oi Chico,
>
> "typo" na primeira linha da sua mensagem
> >O esquema (A --> B) --> (Ng A --> Ng B) é válido no Intucionismo, (versão
> Heyting);
> voce quiz dizer
> (A --> B) --> (Ng B --> Ng A),
> certo?
>
> e sim, gosto bastante das algebras de Heyting e claro que concordo
> totalmente com:
>
> >Como voce sabe muito bem, o modo mais adequado de tratar estes conceitos
> é via adjunções: a implicação é  adjunta da conjunção, enquanto que a
> disjunção é, classicamente, adjunta da diferença simétrica (o complementar
> clássico da equivalência); porém esta última adjunção está longe de ser
> intuicionisticamente válida.
>
> mas e', a discussao sobre o adjunto da disjuncao 'e grande e dificil. e
> pra mim nao faz parte dessa conversa menorzinha, do que 'e valido pro
> Heyting e de que nomes devem ser usados pra que.
>
> obrigada tb por
> >A relação intucionista da disjunção com a implicação resume-se ao óbvio;
> qualquer outra relação é FALSA
> era isso mesmo que eu queria verificar.
>
> abracos,
> Valeria
>
> 2017-10-23 23:08 GMT-07:00 Francisco Miraglia :
>
>> Cara Valéria,
>>
>> Observações que talvez possam ser úteis:
>>
>> 1) O esquema (A --> B) --> (Ng A --> Ng B) é válido no Intucionismo,
>> (versão Heyting); as álgebras de Heyting fornecem uma semântica completa
>> para a versão do Intuicionismo do Arend;
>>
>> 2) Adicionar o esquema recíproco à axiomatização de Heyting da Lógica
>> Intucionista imediatamente fornece a Lógica Clássica; é semelhante ao que
>> acontece com a equivalência no sistema Intuicionista: se for distributiva,
>> a Lógica é clássica.
>>
>> 3) Estou insistindo em incluir o nome do Arend pois afinal nem sempre nos
>> lembramos que o Brower tinha a firme opinião que a sua visão da
>> Lógica era impossível (por definição, já que envolvia a "prática
>> quotidiana dos matemáticos") de ser axiomatizada.
>>
>> 4) Interessante observar que posições filosóficas não se materializam  na
>> "prática quotidiana dos matemáticos": um dos resultados mais conhecidos de
>> Brower (toda função contínua do disco de dimensão n em sí mesmo possui
>> ponto fixo) é estabelecido pelo próprio por contradição!
>> O primeiro passo da contradição já é de ordem grande: não há retração
>> contínua do disco em sua borda (em qualquer dimensão n maior ou igual a
>> 1), o que exige métodos homológicos ou homotópicos); exibir o ponto fixo:
>> "para com isso"
>>
>> 5) Quanto à nomenclatura, tanto Heyting, quanto Kleene (e Vesley)  dão o
>> nome de contraposição ao esquema em (1), sempre chamando a atenção de que ,
>> no Intuicionismo segundo Arend, difere da regra de contraposição clássica,
>> que, em geral, é  enunciada como o esquema "contrapositivo", mencionado em
>> (2).
>>
>> (6) Não me lembro de ler acerca dessas coisas no livro do Dummet (mas
>> também não foi lá que aprendi a lidar com o intuicionismo do Arend), porém
>> sabes como é: a memória não é mais o que era, sendo substituída pela
>> "prática quotidiana" de utilizar metateoria intuicionista para fazer
>> Matemática. Exemplo: anéis de Gelfand (aqueles comutativos com unidade tais
>> que que por cima de todo ideal há apenas um maximal) são,
>> intuicionisticamente,

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

2017-10-24 Por tôpico Valeria de Paiva

oi Chico,

"typo" na primeira linha da sua mensagem
>O esquema (A --> B) --> (Ng A --> Ng B) é válido no Intucionismo, (versão
Heyting);
voce quiz dizer
(A --> B) --> (Ng B --> Ng A),
certo?

e sim, gosto bastante das algebras de Heyting e claro que concordo
totalmente com:

>Como voce sabe muito bem, o modo mais adequado de tratar estes conceitos é
via adjunções: a implicação é  adjunta da conjunção, enquanto que a
disjunção é, classicamente, adjunta da diferença simétrica (o complementar
clássico da equivalência); porém esta última adjunção está longe de ser
intuicionisticamente válida.

mas e', a discussao sobre o adjunto da disjuncao 'e grande e dificil. e pra
mim nao faz parte dessa conversa menorzinha, do que 'e valido pro Heyting e
de que nomes devem ser usados pra que.

obrigada tb por
>A relação intucionista da disjunção com a implicação resume-se ao óbvio;
qualquer outra relação é FALSA
era isso mesmo que eu queria verificar.

abracos,
Valeria

2017-10-23 23:08 GMT-07:00 Francisco Miraglia :

> Cara Valéria,
>
> Observações que talvez possam ser úteis:
>
> 1) O esquema (A --> B) --> (Ng A --> Ng B) é válido no Intucionismo,
> (versão Heyting); as álgebras de Heyting fornecem uma semântica completa
> para a versão do Intuicionismo do Arend;
>
> 2) Adicionar o esquema recíproco à axiomatização de Heyting da Lógica
> Intucionista imediatamente fornece a Lógica Clássica; é semelhante ao que
> acontece com a equivalência no sistema Intuicionista: se for distributiva,
> a Lógica é clássica.
>
> 3) Estou insistindo em incluir o nome do Arend pois afinal nem sempre nos
> lembramos que o Brower tinha a firme opinião que a sua visão da
> Lógica era impossível (por definição, já que envolvia a "prática
> quotidiana dos matemáticos") de ser axiomatizada.
>
> 4) Interessante observar que posições filosóficas não se materializam  na
> "prática quotidiana dos matemáticos": um dos resultados mais conhecidos de
> Brower (toda função contínua do disco de dimensão n em sí mesmo possui
> ponto fixo) é estabelecido pelo próprio por contradição!
> O primeiro passo da contradição já é de ordem grande: não há retração
> contínua do disco em sua borda (em qualquer dimensão n maior ou igual a
> 1), o que exige métodos homológicos ou homotópicos); exibir o ponto fixo:
> "para com isso"
>
> 5) Quanto à nomenclatura, tanto Heyting, quanto Kleene (e Vesley)  dão o
> nome de contraposição ao esquema em (1), sempre chamando a atenção de que ,
> no Intuicionismo segundo Arend, difere da regra de contraposição clássica,
> que, em geral, é  enunciada como o esquema "contrapositivo", mencionado em
> (2).
>
> (6) Não me lembro de ler acerca dessas coisas no livro do Dummet (mas
> também não foi lá que aprendi a lidar com o intuicionismo do Arend), porém
> sabes como é: a memória não é mais o que era, sendo substituída pela
> "prática quotidiana" de utilizar metateoria intuicionista para fazer
> Matemática. Exemplo: anéis de Gelfand (aqueles comutativos com unidade tais
> que que por cima de todo ideal há apenas um maximal) são,
> intuicionisticamente, fielmente quadráticos (possuem uma teoria de formas
> quadráticas "bem comportada" e satisfazem a conjectura de Milnor). Isto já
> é meio complicado; o caso clássico (que penso também ser verdadeiro) parece
> ser ainda mais complicado. Interessante que os meus colegas de formas
> quadráticas e K-teoria não dão a menor importância para a informação
> intuicionista...
>
> (7) A relação intucionista da disjunção com a implicação resume-se ao
> óbvio; qualquer outra relação é FALSA (experimente nos abertos da reta
> real). Ou seja, na minha opinião, "barking up the wrong tree".
>
> Como voce sabe muito bem, o modo mais adequado de tratar estes conceitos é
> via adjunções: a implicação é  adjunta da conjunção, enquanto que a
> disjunção é, classicamente, adjunta da diferença simétrica (o complementar
> clássico da equivalência); porém esta última adjunção está longe de ser
> intuicionisticamente válida. Aliás, se um reticulado distribitivo possui
> uma operação parecida com a diferença simétrica, tem que ser uma álgebra de
> Boole. Aqui começam a aparecer diferenças conceituais importantes e a
> necessidade de empregar
> outras noções, mais gerais (e.g., functores adjuntos), para construir
> Lógicas. Já escrevi demais
>
>
> Um grande abraço,
>
> Chico Miraglia
>
>
>
>
>
>
>> 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
>>> >> logic=edit=9>
>>> ]
>>>
>>> The system of classical logic is obtained by adding any one

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

2017-10-24 Por tôpico Francisco Miraglia


Caro Marcelo,

Obrigado!!

Abraços,

Chico


Quoting Marcelo Finger :


Chico.

Adorei seu post.  Apenas 2 comentários rápidos


4) Interessante observar que posições filosóficas não se materializam  na

"prática quotidiana dos matemáticos":

Isso é um fenômeno humano, não apenas matemático.  O mundo das ideias e
práticas humanas é um campo fértil para a prática paraconsistente.


Já escrevi demais


Pelo contrário, escreva mais (vezes)!

[]s


2017-10-24 4:08 GMT-02:00 Francisco Miraglia :


Cara Valéria,

Observações que talvez possam ser úteis:

1) O esquema (A --> B) --> (Ng A --> Ng B) é válido no Intucionismo,
(versão Heyting); as álgebras de Heyting fornecem uma semântica completa
para a versão do Intuicionismo do Arend;

2) Adicionar o esquema recíproco à axiomatização de Heyting da Lógica
Intucionista imediatamente fornece a Lógica Clássica; é semelhante ao que
acontece com a equivalência no sistema Intuicionista: se for distributiva,
a Lógica é clássica.

3) Estou insistindo em incluir o nome do Arend pois afinal nem sempre nos
lembramos que o Brower tinha a firme opinião que a sua visão da
Lógica era impossível (por definição, já que envolvia a "prática
quotidiana dos matemáticos") de ser axiomatizada.

4) Interessante observar que posições filosóficas não se materializam  na
"prática quotidiana dos matemáticos": um dos resultados mais conhecidos de
Brower (toda função contínua do disco de dimensão n em sí mesmo possui
ponto fixo) é estabelecido pelo próprio por contradição!
O primeiro passo da contradição já é de ordem grande: não há retração
contínua do disco em sua borda (em qualquer dimensão n maior ou igual a
1), o que exige métodos homológicos ou homotópicos); exibir o ponto fixo:
"para com isso"

5) Quanto à nomenclatura, tanto Heyting, quanto Kleene (e Vesley)  dão o
nome de contraposição ao esquema em (1), sempre chamando a atenção de que ,
no Intuicionismo segundo Arend, difere da regra de contraposição clássica,
que, em geral, é  enunciada como o esquema "contrapositivo", mencionado em
(2).

(6) Não me lembro de ler acerca dessas coisas no livro do Dummet (mas
também não foi lá que aprendi a lidar com o intuicionismo do Arend), porém
sabes como é: a memória não é mais o que era, sendo substituída pela
"prática quotidiana" de utilizar metateoria intuicionista para fazer
Matemática. Exemplo: anéis de Gelfand (aqueles comutativos com unidade tais
que que por cima de todo ideal há apenas um maximal) são,
intuicionisticamente, fielmente quadráticos (possuem uma teoria de formas
quadráticas "bem comportada" e satisfazem a conjectura de Milnor). Isto já
é meio complicado; o caso clássico (que penso também ser verdadeiro) parece
ser ainda mais complicado. Interessante que os meus colegas de formas
quadráticas e K-teoria não dão a menor importância para a informação
intuicionista...

(7) A relação intucionista da disjunção com a implicação resume-se ao
óbvio; qualquer outra relação é FALSA (experimente nos abertos da reta
real). Ou seja, na minha opinião, "barking up the wrong tree".

Como voce sabe muito bem, o modo mais adequado de tratar estes conceitos é
via adjunções: a implicação é  adjunta da conjunção, enquanto que a
disjunção é, classicamente, adjunta da diferença simétrica (o complementar
clássico da equivalência); porém esta última adjunção está longe de ser
intuicionisticamente válida. Aliás, se um reticulado distribitivo possui
uma operação parecida com a diferença simétrica, tem que ser uma álgebra de
Boole. Aqui começam a aparecer diferenças conceituais importantes e a
necessidade de empregar
outras noções, mais gerais (e.g., functores adjuntos), para construir
Lógicas. Já escrevi demais


Um grande abraço,

Chico Miraglia







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 )}]

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

2017-10-24 Por tôpico Marcelo Finger

Chico.

Adorei seu post.  Apenas 2 comentários rápidos

> 4) Interessante observar que posições filosóficas não se materializam  na
"prática quotidiana dos matemáticos":

Isso é um fenômeno humano, não apenas matemático.  O mundo das ideias e
práticas humanas é um campo fértil para a prática paraconsistente.

> Já escrevi demais

Pelo contrário, escreva mais (vezes)!

[]s


2017-10-24 4:08 GMT-02:00 Francisco Miraglia :

> Cara Valéria,
>
> Observações que talvez possam ser úteis:
>
> 1) O esquema (A --> B) --> (Ng A --> Ng B) é válido no Intucionismo,
> (versão Heyting); as álgebras de Heyting fornecem uma semântica completa
> para a versão do Intuicionismo do Arend;
>
> 2) Adicionar o esquema recíproco à axiomatização de Heyting da Lógica
> Intucionista imediatamente fornece a Lógica Clássica; é semelhante ao que
> acontece com a equivalência no sistema Intuicionista: se for distributiva,
> a Lógica é clássica.
>
> 3) Estou insistindo em incluir o nome do Arend pois afinal nem sempre nos
> lembramos que o Brower tinha a firme opinião que a sua visão da
> Lógica era impossível (por definição, já que envolvia a "prática
> quotidiana dos matemáticos") de ser axiomatizada.
>
> 4) Interessante observar que posições filosóficas não se materializam  na
> "prática quotidiana dos matemáticos": um dos resultados mais conhecidos de
> Brower (toda função contínua do disco de dimensão n em sí mesmo possui
> ponto fixo) é estabelecido pelo próprio por contradição!
> O primeiro passo da contradição já é de ordem grande: não há retração
> contínua do disco em sua borda (em qualquer dimensão n maior ou igual a
> 1), o que exige métodos homológicos ou homotópicos); exibir o ponto fixo:
> "para com isso"
>
> 5) Quanto à nomenclatura, tanto Heyting, quanto Kleene (e Vesley)  dão o
> nome de contraposição ao esquema em (1), sempre chamando a atenção de que ,
> no Intuicionismo segundo Arend, difere da regra de contraposição clássica,
> que, em geral, é  enunciada como o esquema "contrapositivo", mencionado em
> (2).
>
> (6) Não me lembro de ler acerca dessas coisas no livro do Dummet (mas
> também não foi lá que aprendi a lidar com o intuicionismo do Arend), porém
> sabes como é: a memória não é mais o que era, sendo substituída pela
> "prática quotidiana" de utilizar metateoria intuicionista para fazer
> Matemática. Exemplo: anéis de Gelfand (aqueles comutativos com unidade tais
> que que por cima de todo ideal há apenas um maximal) são,
> intuicionisticamente, fielmente quadráticos (possuem uma teoria de formas
> quadráticas "bem comportada" e satisfazem a conjectura de Milnor). Isto já
> é meio complicado; o caso clássico (que penso também ser verdadeiro) parece
> ser ainda mais complicado. Interessante que os meus colegas de formas
> quadráticas e K-teoria não dão a menor importância para a informação
> intuicionista...
>
> (7) A relação intucionista da disjunção com a implicação resume-se ao
> óbvio; qualquer outra relação é FALSA (experimente nos abertos da reta
> real). Ou seja, na minha opinião, "barking up the wrong tree".
>
> Como voce sabe muito bem, o modo mais adequado de tratar estes conceitos é
> via adjunções: a implicação é  adjunta da conjunção, enquanto que a
> disjunção é, classicamente, adjunta da diferença simétrica (o complementar
> clássico da equivalência); porém esta última adjunção está longe de ser
> intuicionisticamente válida. Aliás, se um reticulado distribitivo possui
> uma operação parecida com a diferença simétrica, tem que ser uma álgebra de
> Boole. Aqui começam a aparecer diferenças conceituais importantes e a
> necessidade de empregar
> outras noções, mais gerais (e.g., functores adjuntos), para construir
> Lógicas. Já escrevi demais
>
>
> Um grande abraço,
>
> Chico Miraglia
>
>
>
>
>
>
>> 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
>>> >> logic=edit=9>
>>> ]
>>>
>>> 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)
>>>-

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

2017-10-24 Por tôpico Elaine Pimentel

Prezados Hermógenes e Valéria,

Em matemática, quando você quer provar A => B por "contrapositivo", você
prova \neg B => \neg A. Ou seja, você usa que

\neg B => \neg A => (A => B)

é válida. Isso é equivalente a adicionar a dupla negação ao seu sistema
lógico. Eu aprendi assim: que a "lei do contrapositivo" era

\neg B => \neg A \equiv (A => B)

sendo que a recíproca é obviamente válida em lógica intuicionista.

Nunca, entretanto, pensei a respeito da terminologia. Longe de mim querer
"make a point" ou etc. Não tenho problema em deixar de usar o termo na
próxima palestra :) Obrigada por assistir, btw.

Abraços,

Elaine.

2017-10-24 5:39 GMT-03:00 Hermógenes Oliveira <
hermogenes.olive...@student.uni-tuebingen.de>:

> Valeria de Paiva  escreveu:
>
>
>> [... ]
>>
>> (¬φ → ¬χ) → (χ → φ) (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) → (¬B → ¬A)
>>
>> mas quem escreveu o artigo em vez de dizer
>>
>> (¬A → ¬B) → (¬¬B → ¬¬A),
>> removeu a dupla negacao, ficando com
>> (¬A → ¬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?
>>
>
> Eu concordo contigo, Valéria.  Tradicionalmente, "contraposição" é o
> nome dado à (A → B) → (¬B → ¬A).
>
> Curiosamente, a primeira vez que eu vi a "contraposição" apresentada
> como divisora de águas entre lógica clássica e intuicionista foi no
> vídeo da palestra da Elaine Pimentel, "A semantical view of proof
> systems", no Filomena 2017 (divulgado recentemente nesta lista).  Na
> ocasião, pensei "Peraí...", pausei o vídeo e raciocinei basicamente o
> que você apresentou acima.  A Elaine apresentou o negócio como uma
> regra de inferência que permitiria estabelecer A → B por meio de
> derivação de ¬A a partir de ¬B.  Devo admitir, contudo, que
> apresentado assim, como regra de inferência, o nome "contraposição"
> não me parece *tão* estranho.
>
> Eu não sei porque (¬A → ¬B) → (B → A), com o nome "contraposição", tem
> sido usado como diferenciador entre lógica clássica e intuicionista,
> mas isso parece ser um desenvolvimento recente (a palestra da Elaine e
> o artigo da Wikipédia sendo os únicos casos que me lembro até agora).
> Talvez tenha aparecido em algum livro ou artigo e as pessoas passaram
> a adotar essa caracterização.  Eu não gosto muito, pois tem grande
> potencial para causar confusão.
>
> tem mais alguma coisa errada no artigo?  eu estou querendo me
>> lembrar da relacao entre implicacao e disjuncao.  essas estao
>> certas?
>>
>> Disjunction versus implication:
>>
>>(φ ∨ ψ) → (¬φ → ψ)
>>
>
> Esta está correta.  Basta aplicar ∨E com premissa menor ψ, obtida,
> respectivamente, (1, [φ]) por ECQ a partir de φ (descartado) e ¬φ, e
> (2, [ψ]) ψ (descartado).  Daí é só introdizir as implicações.
>
>(¬φ ∨ ψ) → (φ → ψ)
>>
>
> Esta tambeḿ está correta.  Basta substituir φ por ¬φ na justificativa
> acima.
>
> Mas talvez a relação mais interessante entre disjunção e implicação
> seja dada por
>
> φ ∨ ψ ⇔ ∀χ (φ → χ) → ((ψ → χ) → χ))
>
> que é, basicamente, uma tradução da regra de eliminação em segunda
> ordem (com quantificação sobre sentenças), também chamado de sistema
> Fₐₜ na literatura recente. Essa relacão é inclusive usada no artigo da
> Wikipédia que você mencionou para oferecer um *esquema* axiomático
> alternativo para a lei do terceiro excluído (φ ∨ ¬φ):
>
> (φ → χ) → ((¬φ →χ) → χ).
>
>
> --
> 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/di
> map.ufrn.br/group/logica-l/.
> Para ver esta discussão na web, acesse https://groups.google.com/a/di
> map.ufrn.br/d/msgid/logica-l/20171024103907.Horde.StcBDM_NG
> GFij6cUvk478_N%40webmail.uni-tuebingen.de.
>



-- 
Elaine.
-
Elaine Pimentel  - DMAT/UFRN

Address: Departamento de Matemática
Universidade Federal do Rio Grande do Norte
Campus Universitário - Av. Senador Salgado Filho, s/nº
Lagoa Nova, CEP: 59.078-970 - Natal - RN

Phone: +55 84 3215-3820

http://sites.google.com/site/elainepimentel/
Lattes: http://lattes.cnpq.br/3298246411086415


-- 
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,

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

2017-10-24 Por tôpico Hermógenes Oliveira


Valeria de Paiva  escreveu:



[... ]

(¬φ → ¬χ) → (χ → φ) (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) → (¬B → ¬A)

mas quem escreveu o artigo em vez de dizer

(¬A → ¬B) → (¬¬B → ¬¬A),
removeu a dupla negacao, ficando com
(¬A → ¬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?


Eu concordo contigo, Valéria.  Tradicionalmente, "contraposição" é o
nome dado à (A → B) → (¬B → ¬A).

Curiosamente, a primeira vez que eu vi a "contraposição" apresentada
como divisora de águas entre lógica clássica e intuicionista foi no
vídeo da palestra da Elaine Pimentel, "A semantical view of proof
systems", no Filomena 2017 (divulgado recentemente nesta lista).  Na
ocasião, pensei "Peraí...", pausei o vídeo e raciocinei basicamente o
que você apresentou acima.  A Elaine apresentou o negócio como uma
regra de inferência que permitiria estabelecer A → B por meio de
derivação de ¬A a partir de ¬B.  Devo admitir, contudo, que
apresentado assim, como regra de inferência, o nome "contraposição"
não me parece *tão* estranho.

Eu não sei porque (¬A → ¬B) → (B → A), com o nome "contraposição", tem
sido usado como diferenciador entre lógica clássica e intuicionista,
mas isso parece ser um desenvolvimento recente (a palestra da Elaine e
o artigo da Wikipédia sendo os únicos casos que me lembro até agora).
Talvez tenha aparecido em algum livro ou artigo e as pessoas passaram
a adotar essa caracterização.  Eu não gosto muito, pois tem grande
potencial para causar confusão.


tem mais alguma coisa errada no artigo?  eu estou querendo me
lembrar da relacao entre implicacao e disjuncao.  essas estao
certas?

Disjunction versus implication:

   (φ ∨ ψ) → (¬φ → ψ)


Esta está correta.  Basta aplicar ∨E com premissa menor ψ, obtida,
respectivamente, (1, [φ]) por ECQ a partir de φ (descartado) e ¬φ, e
(2, [ψ]) ψ (descartado).  Daí é só introdizir as implicações.


   (¬φ ∨ ψ) → (φ → ψ)


Esta tambeḿ está correta.  Basta substituir φ por ¬φ na justificativa
acima.

Mas talvez a relação mais interessante entre disjunção e implicação
seja dada por

φ ∨ ψ ⇔ ∀χ (φ → χ) → ((ψ → χ) → χ))

que é, basicamente, uma tradução da regra de eliminação em segunda
ordem (com quantificação sobre sentenças), também chamado de sistema
Fₐₜ na literatura recente. Essa relacão é inclusive usada no artigo da
Wikipédia que você mencionou para oferecer um *esquema* axiomático
alternativo para a lei do terceiro excluído (φ ∨ ¬φ):

(φ → χ) → ((¬φ →χ) → χ).


--
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/20171024103907.Horde.StcBDM_NGGFij6cUvk478_N%40webmail.uni-tuebingen.de.

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

2017-10-24 Por tôpico Francisco Miraglia


Cara Valéria,

Observações que talvez possam ser úteis:

1) O esquema (A --> B) --> (Ng A --> Ng B) é válido no Intucionismo,  
(versão Heyting); as álgebras de Heyting fornecem uma semântica  
completa para a versão do Intuicionismo do Arend;


2) Adicionar o esquema recíproco à axiomatização de Heyting da Lógica
Intucionista imediatamente fornece a Lógica Clássica; é semelhante ao  
que acontece com a equivalência no sistema Intuicionista: se for  
distributiva, a Lógica é clássica.


3) Estou insistindo em incluir o nome do Arend pois afinal nem sempre  
nos lembramos que o Brower tinha a firme opinião que a sua visão da

Lógica era impossível (por definição, já que envolvia a "prática
quotidiana dos matemáticos") de ser axiomatizada.

4) Interessante observar que posições filosóficas não se materializam   
na "prática quotidiana dos matemáticos": um dos resultados mais  
conhecidos de Brower (toda função contínua do disco de dimensão n em  
sí mesmo possui ponto fixo) é estabelecido pelo próprio por contradição!

O primeiro passo da contradição já é de ordem grande: não há retração
contínua do disco em sua borda (em qualquer dimensão n maior ou igual  
a 1), o que exige métodos homológicos ou homotópicos); exibir o ponto  
fixo: "para com isso"


5) Quanto à nomenclatura, tanto Heyting, quanto Kleene (e Vesley)  dão  
o nome de contraposição ao esquema em (1), sempre chamando a atenção  
de que , no Intuicionismo segundo Arend, difere da regra de  
contraposição clássica, que, em geral, é  enunciada como o esquema  
"contrapositivo", mencionado em (2).


(6) Não me lembro de ler acerca dessas coisas no livro do Dummet (mas  
também não foi lá que aprendi a lidar com o intuicionismo do Arend),  
porém sabes como é: a memória não é mais o que era, sendo substituída  
pela "prática quotidiana" de utilizar metateoria intuicionista para  
fazer Matemática. Exemplo: anéis de Gelfand (aqueles comutativos com  
unidade tais que que por cima de todo ideal há apenas um maximal) são,  
intuicionisticamente, fielmente quadráticos (possuem uma teoria de  
formas quadráticas "bem comportada" e satisfazem a conjectura de  
Milnor). Isto já é meio complicado; o caso clássico (que penso também  
ser verdadeiro) parece ser ainda mais complicado. Interessante que os  
meus colegas de formas quadráticas e K-teoria não dão a menor  
importância para a informação  intuicionista...


(7) A relação intucionista da disjunção com a implicação resume-se ao  
óbvio; qualquer outra relação é FALSA (experimente nos abertos da reta  
real). Ou seja, na minha opinião, "barking up the wrong tree".


Como voce sabe muito bem, o modo mais adequado de tratar estes  
conceitos é via adjunções: a implicação é  adjunta da conjunção,  
enquanto que a disjunção é, classicamente, adjunta da diferença  
simétrica (o complementar clássico da equivalência); porém esta última  
adjunção está longe de ser intuicionisticamente válida. Aliás, se um  
reticulado distribitivo possui uma operação parecida com a diferença  
simétrica, tem que ser uma álgebra de Boole. Aqui começam a aparecer  
diferenças conceituais importantes e a necessidade de empregar
outras noções, mais gerais (e.g., functores adjuntos), para construir  
Lógicas. Já escrevi demais



Um grande abraço,

Chico Miraglia







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)

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

2017-10-23 Por tôpico 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...

2017-10-23 Por tôpico 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...

2017-10-23 Por tôpico 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.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

18 matches

Site Navigation

Mail list logo

Footer information