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

[Valeria de Paiva]

oi Andrea!

bom ler voce!!! e bom lembrar que o seus sistemas funcionam. ajuda bastante
mesmo!
pra ajudar mais, o que o Google me contou sobre os seus papers (que nao
custava nada colocar no website do sistema tb, ne?)

mas os links abaixo nao estao todos funcionando, dai que o requerido pra
ler sobre o calculo intuicionista 'e

https://periodicos.ufsc.br/index.php/principia/article/view/1808-1711.2010v14n1p125/17985

PARABENS pelos bolos e papers e sistemas!

e PARABENS ao Decio por manter Principia no ar.

Abracos logicos,
Valeria

segunda-feira, 12 de março de 2012
Palestras Professora Andrea Loparic

Olá para todos.

O grupo de estudos de lógica da FAFICH, com o apoio do Programa de
Pós-graduação em Filosofia, retoma suas atividades neste semestre com duas
palestras da professora *Andrea Loparic* (USP):

*Teoria das valorações*
Dia 22 de março, 15h, sala 3019.

*Identidade, negação e universos de discurso*
Dia 23 de março, 15h, sala 3019.


Referências:


*Teoria das valorações:*
LOPARIC, A. M. A. C. ; da COSTA, N.C.A. Paraconsistency,
paracompleteness and valuations. Logique et Analyse, v. 106, p.
119-131, 1984
Disponível em http://dl.dropbox.com/u/5959592/al/loparic.parac.pdf
LOPARIC, A. M. A. C. . A semantical study of some propositional
calculi. THE JOURNAL OF NON-CLASSICAL LOGIC, v. III, p. 74-95, 1986.
LOPARIC, A. M. A. C. . The method of valuations in modal logic. In:
First Brazilian Conference, 1977, New York. Proceedings First
Brazilian Conference. New York : Marcel Dekker Inc., 1977.
Disponível em http://dl.dropbox.com/u/5959592/al/met.valuations.pdf
LOPARIC, A. M. A. C. 'Valuation semantics for intuitionistic
propositional calculus and some of its subcalculi' in Principia,
http://www.cfh.ufsc.br/~principi/p141-8.pdf

*Identidade, negação e universos de discurso*

LOPARIC, A. M. A. C.. 'Lacan avec les Philosophes' in "Bibliotheque du
College International de Philosophie" ed. Alban Michel,
Disponível em
http://dl.dropbox.com/u/5959592/al/A.Loparic.Identite.negation.pdf


2017-10-24 16:34 GMT-07:00 Andrea Loparic :

> Marcelo, caro, é por essas e outras que crianças e velhinhas,
> especialmente as inteligentes, se dão tão bem!
>
>
> Em 24 de outubro de 2017 20:59, Marcelo Finger 
> escreveu:
>
>> Andreia.
>>
>> Demorou um pouquinho mas acho que entendi seus jogos de palavras. É o
>> tipo de trocadilho que meu filho de 12 anos faz :)
>>
>> Pequins
>>
>> Marcelo
>>
>> 2017-10-24 20:48 GMT-02:00 Andrea Loparic :
>>
>>> Caros,
>>>
>>> Aproveitando o trend legal sobre o intuicionismo, venho lembrar,
>>> para os mais novos especialmente, que, com base em semânticas
>>> de valorações bivalentes corretas e completas que obtive outrora,
>>> para os cálculos proposicionais minimal (Johanssen-Kolmogoroff)
>>> e intucionista (Heyting), meu filho computeiro Marko Loparic e eu
>>> fizemos juntos um programinha em Python que constroi e exibe
>>> tabelas de verdade generalizadas para testar a validade de
>>> fórmulas em cada um desses dois cálculos. O artigo com a semântica
>>> foi publicado pelo Décio, a quem peço a gentileza de me mandar
>>> novamente a referência, pois, aos 76, acho-me somezeimerada ( por
>>> enquanto, pelo menos, não é All) . O programinha, desde 2009, está
>>> disponivel para uso de quem quiser na URL
>>>
>>> http://www.paralogics.net/tableaux/minimal_intuitionism/
>>>
>>> Obs: O programa só reconhece como fórmulas as que vêm na notação
>>> especificada na introdução, a saber, aquelas cujo vocabulário é composto
>>> por minúsculas, ~, &, | , > = e parêntesis (para os conectivos
>>> binários).
>>>
>>> No mais, reitero o convite para saborearem meu bolo de rolo,
>>> garantindo que, nessa modalidade, estou ainda nozeimerada.
>>>
>>> Beijins ( ou seriam pequins?)
>>>
>>> Andrea
>>>
>>> --
>>> 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/CACHAqBmf%2BtauDjypWfOL%2B5jg0E
>>> g%3D%3D9F5oFHZ2HHbmxJRJ9Xkqw%40mail.gmail.com
>>> 
>>> .
>>>
>>
>>
>>
>> --
>>  Marcelo Finger
>>  Departament of Computer Science, IME
>>  University of Sao Paulo
>>  http://www.ime.usp.br/~mfinger
>>
>> --
>> 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 

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

[Andrea Loparic]

Marcelo, caro, é por essas e outras que crianças e velhinhas,
especialmente as inteligentes, se dão tão bem!


Em 24 de outubro de 2017 20:59, Marcelo Finger 
escreveu:

> Andreia.
>
> Demorou um pouquinho mas acho que entendi seus jogos de palavras. É o tipo
> de trocadilho que meu filho de 12 anos faz :)
>
> Pequins
>
> Marcelo
>
> 2017-10-24 20:48 GMT-02:00 Andrea Loparic :
>
>> Caros,
>>
>> Aproveitando o trend legal sobre o intuicionismo, venho lembrar,
>> para os mais novos especialmente, que, com base em semânticas
>> de valorações bivalentes corretas e completas que obtive outrora,
>> para os cálculos proposicionais minimal (Johanssen-Kolmogoroff)
>> e intucionista (Heyting), meu filho computeiro Marko Loparic e eu
>> fizemos juntos um programinha em Python que constroi e exibe
>> tabelas de verdade generalizadas para testar a validade de
>> fórmulas em cada um desses dois cálculos. O artigo com a semântica
>> foi publicado pelo Décio, a quem peço a gentileza de me mandar
>> novamente a referência, pois, aos 76, acho-me somezeimerada ( por
>> enquanto, pelo menos, não é All) . O programinha, desde 2009, está
>> disponivel para uso de quem quiser na URL
>>
>> http://www.paralogics.net/tableaux/minimal_intuitionism/
>>
>> Obs: O programa só reconhece como fórmulas as que vêm na notação
>> especificada na introdução, a saber, aquelas cujo vocabulário é composto
>> por minúsculas, ~, &, | , > = e parêntesis (para os conectivos binários).
>>
>> No mais, reitero o convite para saborearem meu bolo de rolo,
>> garantindo que, nessa modalidade, estou ainda nozeimerada.
>>
>> Beijins ( ou seriam pequins?)
>>
>> Andrea
>>
>> --
>> 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/CACHAqBmf%2BtauDjypWfOL%2B5jg0
>> Eg%3D%3D9F5oFHZ2HHbmxJRJ9Xkqw%40mail.gmail.com
>> 
>> .
>>
>
>
>
> --
>  Marcelo Finger
>  Departament of Computer Science, IME
>  University of Sao Paulo
>  http://www.ime.usp.br/~mfinger
>
> --
> 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/CABqmzx0agJUPdhoUH8gb3qyTb0CHU
> FZqq6VD%2BPA6MBGLBnnt_g%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/CACHAqBmsn3kz_z%3DRS1S%2BVhPm6Mf_bcUzUpJ13yMJ%2BNon4oC%3DBA%40mail.gmail.com.

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

[Marcelo Finger]

Andreia.

Demorou um pouquinho mas acho que entendi seus jogos de palavras. É o tipo
de trocadilho que meu filho de 12 anos faz :)

Pequins

Marcelo

2017-10-24 20:48 GMT-02:00 Andrea Loparic :

> Caros,
>
> Aproveitando o trend legal sobre o intuicionismo, venho lembrar,
> para os mais novos especialmente, que, com base em semânticas
> de valorações bivalentes corretas e completas que obtive outrora,
> para os cálculos proposicionais minimal (Johanssen-Kolmogoroff)
> e intucionista (Heyting), meu filho computeiro Marko Loparic e eu
> fizemos juntos um programinha em Python que constroi e exibe
> tabelas de verdade generalizadas para testar a validade de
> fórmulas em cada um desses dois cálculos. O artigo com a semântica
> foi publicado pelo Décio, a quem peço a gentileza de me mandar
> novamente a referência, pois, aos 76, acho-me somezeimerada ( por
> enquanto, pelo menos, não é All) . O programinha, desde 2009, está
> disponivel para uso de quem quiser na URL
>
> http://www.paralogics.net/tableaux/minimal_intuitionism/
>
> Obs: O programa só reconhece como fórmulas as que vêm na notação
> especificada na introdução, a saber, aquelas cujo vocabulário é composto
> por minúsculas, ~, &, | , > = e parêntesis (para os conectivos binários).
>
> No mais, reitero o convite para saborearem meu bolo de rolo,
> garantindo que, nessa modalidade, estou ainda nozeimerada.
>
> Beijins ( ou seriam pequins?)
>
> Andrea
>
> --
> 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/CACHAqBmf%2BtauDjypWfOL%2B5jg0Eg%3D%
> 3D9F5oFHZ2HHbmxJRJ9Xkqw%40mail.gmail.com
> 
> .
>



-- 
 Marcelo Finger
 Departament of Computer Science, IME
 University of Sao Paulo
 http://www.ime.usp.br/~mfinger

-- 
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/CABqmzx0agJUPdhoUH8gb3qyTb0CHUFZqq6VD%2BPA6MBGLBnnt_g%40mail.gmail.com.

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

[Andrea Loparic]

Caros,

Aproveitando o trend legal sobre o intuicionismo, venho lembrar,
para os mais novos especialmente, que, com base em semânticas
de valorações bivalentes corretas e completas que obtive outrora,
para os cálculos proposicionais minimal (Johanssen-Kolmogoroff)
e intucionista (Heyting), meu filho computeiro Marko Loparic e eu
fizemos juntos um programinha em Python que constroi e exibe
tabelas de verdade generalizadas para testar a validade de
fórmulas em cada um desses dois cálculos. O artigo com a semântica
foi publicado pelo Décio, a quem peço a gentileza de me mandar
novamente a referência, pois, aos 76, acho-me somezeimerada ( por
enquanto, pelo menos, não é All) . O programinha, desde 2009, está
disponivel para uso de quem quiser na URL

http://www.paralogics.net/tableaux/minimal_intuitionism/

Obs: O programa só reconhece como fórmulas as que vêm na notação
especificada na introdução, a saber, aquelas cujo vocabulário é composto
por minúsculas, ~, &, | , > = e parêntesis (para os conectivos binários).

No mais, reitero o convite para saborearem meu bolo de rolo,
garantindo que, nessa modalidade, estou ainda nozeimerada.

Beijins ( ou seriam pequins?)

Andrea

-- 
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/CACHAqBmf%2BtauDjypWfOL%2B5jg0Eg%3D%3D9F5oFHZ2HHbmxJRJ9Xkqw%40mail.gmail.com.

[Logica-l] Fwd: Concurso Docente - UnB (Lógica Computacional e Inteligência Artificial)

[Joao Marcos]

-- Forwarded message --

Prezada(o)s,

Solicitamos ajuda na divulgação (desculpem-nos pelas eventuais duplicatas):

Estão abertas as inscrições do concurso público para professor Adjunto
"A", Classe 1, da Universidade de Brasilia (UnB), Faculdade do Gama
(FGA), para o Baracharelado em Engenharia de Software, na área de
conhecimento "Lógica Computacional e Inteligência Artificial".

- Período de inscrição e solicitação de isenção da taxa de Inscrição:
23/10/2017 a 24/11/2017
- Divulgação da relação dos candidatos que tiveram o pedido de isenção
deferido: 01/12/201
- Período para contestar o indeferimento do pedido de isenção:
04/12/2017 a 05/12/2017
- Divulgação do resultado da contestação: 13/12/2017
- Data limite para o pagamento da taxa de inscrição: 14/12/2017

A expectativa é que as provas sejam realizadas no terço final do mês
de janeiro/2018. O Edital e demais informações estão publicadas em
http://concursos.unb.br/index.php/efetivos-2017/972-edital-de-abertura-n-220-2017

Sobre a UnB Gama
---

A Faculdade UnB Gama (FGA) é a extensão da Universidade de Brasília na
região administrativa do Gama. É o maior entre os três campi da
universidade situados fora do Plano Piloto de Brasília, abrigando
cinco cursos da área de engenharia: Engenharia Aeroespacial,
Engenharia Automotiva, Engenharia Eletrônica, Engenharia de Energia e
Engenharia de Software. O novo campus faz parte de um projeto de
expansão das universidades federais, o Reuni. Entrou em funcionamento
no segundo semestre de 2008. Em 2011 foi inaugurada a sede definitiva.

- Para mais informações sobre a UnB Gama, acesse: https://fga.unb.br
- Para conhecer o Bacharelado em Engenharia de Software, veja:
https://fga.unb.br/software/
- Para ter mais detalhes sobre o Projeto Pedagógico do Curso, leia:
https://fga.unb.br/articles/0001/6971/PPC_-_Projeto_Pol_tico_do_Curso_-_Software.pdf

atenciosamente,

Prof. Paulo Meirelles

-- 
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/CAO6j_LghJ%2BuydD10Ng9mF5bhJWeAZidTKfx3_hxg0AXqK2smUw%40mail.gmail.com.

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

[Bruno Bentzen]

>
> A sintaxe do sistema é brevemente explicada aqui 
> . 


Uma pequena correção: o link acima está quebrado (obrigado por me avisar, 
Eduardo!), o endereço correto do README é este aqui 
.

On Tuesday, October 24, 2017 at 9:51:51 PM UTC+8, Bruno Bentzen wrote:
>
> Oi Valéria,
>
> Acrescentando meus dois centavos:
>
> Nos últimos anos comecei a brincar um pouco com uma implementação de um 
> checador de tipos em C, o resultado foi um mini checador de tipos "for fun" 
> para uma versão extendida do Cálculo lambda simplesmente tipado. Batizei o 
> pequeno sistema de "Cubo".
>
> 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. :)
>
> Claro, o Cubo (mal-programado, mas consistente!) é apenas uma criança, mas 
> no futuro pretendo incluir suporte para tipos dependentes e universos 
> também. Bem, quem sabe um dia ele não se tornará um adulto que possa servir 
> como checador de tipos para uma teoria de tipos cúbica? (Daí a origem do 
> nome)
>
> Abraços lógicos,
> Bruno
>
> --
> Bruno Bentzen
> https://sites.google.com/site/bbentzena/
>
> On Tuesday, October 24, 2017 at 7:00:02 AM UTC+8, valeria.depaiva 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ê 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/85d1a3e4-24c6-4bfb-b88d-af01c5556bd1%40dimap.ufrn.br.

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

[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...

[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 

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

[Bruno Bentzen]

Oi Valéria,

Acrescentando meus dois centavos:

Nos últimos anos comecei a brincar um pouco com uma implementação de um 
checador de tipos em C, o resultado foi um mini checador de tipos "for fun" 
para uma versão extendida do Cálculo lambda simplesmente tipado. Batizei o 
pequeno sistema de "Cubo".

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. :)

Claro, o Cubo (mal-programado, mas consistente!) é apenas uma criança, mas 
no futuro pretendo incluir suporte para tipos dependentes e universos 
também. Bem, quem sabe um dia ele não se tornará um adulto que possa servir 
como checador de tipos para uma teoria de tipos cúbica? (Daí a origem do 
nome)

Abraços lógicos,
Bruno

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

On Tuesday, October 24, 2017 at 7:00:02 AM UTC+8, valeria.depaiva 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ê 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/883c0ec9-edf9-488c-82fd-38d098bbd678%40dimap.ufrn.br.

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

[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...

[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] Re: Collected Works by Charles S. Peirce

[Antonio Marmo]

Muito obrigado, caríssimo Jean-Yves!
Aliás, uma vez mais muito obrigado a todos que atenciosamente me responderam em 
particular.

Só para explicar: eu tinha um problema com autores que citam o Peirce, mas não 
dizem de que trabalho vem esta ou aquela citação. Às vezes indicam só o ano do 
trabalho e não o incluem na bibliografia ao final. Como num mesmo por vezes há 
mais de um trabalho, fica difícil localizar a passagem. E a coleção do Peirce 
que eu já tinha não facilitava muito.

Porém, todas as ajudas que recebi deram condições de achar essas passagens e 
agora sigo em frente.

E nunca é demais reconhecer a atenção generosa dos demais!

Quanto ao fato do Peirce em muitos aspectos já antecipar o que hoje se faz 
rotineiramente no meio da pluralidade das lógicas, isso já é um assunto quente 
para outros debates. Outra contribuição importante, mas pouco lembrada, são as 
reflexões de Husserl, que também podem inaugurar outras discussões.

Abraços!

Dize à sabedoria: Tu és minha irmã...
Provérbios 7:4

> On 24 Oct 2017, at 07:23, jyb  wrote:
> 
> Ola Tony
> 
> Na pagina do tutorial sobre Peirce no UNILOG'2018 que vai ser apresentado por 
> William James McCurdy 
> voce vai encontrar links para os escritos do Peirce que estão on-line e muito 
> mais
> http://www.uni-log.org/ULS6-peirce.html
> 
> A ideia do nosso site do  UNILOG 
> http://www.uni-log.org/
> é que não seja so um site para eventos, mas um boa base para a pesquisa, uma 
> bússola
> uma vez que uma edicao do UNILOG acabou, o site desta edicao conitnua a ser 
> util
> veja por exemplo a pagina do tutorial sobre Lewis Carroll do UNILOG'2015, em 
> Istanbul apresentado por Amirouche Moktefi, com mutios links uteis
> http://www.uni-log.org/t5-lewiscarroll.html
> 
> JYB
> 
> 
> 
> Le vendredi 20 octobre 2017 19:09:49 UTC+2, marmo.tony a écrit :
>> 
>> Caríssimos,
>> 
>> Estou precisando encontrar em PDF a coleção de trabalhos de Peirce.
>> Achei um PDF que na verdade fala dos vários trabalhos de editoração de 
>> manuscritos dele, não traz os artigos em si numa ordem cronológica.
>> 
>> Quem, por favor, tiver esse PDF, mande-o para mim como e-mail particular. 
>> Muito obrigado!
>> 
>> Dize à sabedoria: Tu és minha irmã...
>> Provérbios 7:4
>> 
>>> On 20 Oct 2017, at 06:17, jean-yves beziau  wrote:
>>> 
>>> Acabou de ser publicado um numero especial do prestigioso jornal
>>> Sophia - Logic and Philosophy of Religion
>>> Volume 56, Issue 2, June 2017
>>> Issue Editors: Ricardo Sousa Silvestre, Jean-Yvez Beziau
>>> https://link.springer.com/journal/11841/56/2?wt_mc=alerts.TOCjournals
>>> 
>>> Artigos publicados aqui são relacionados ao 
>>> 1st World Congress on Logic and Religion
>>> organizado em João Pessoa de 1 a 5 de abril de 2015
>>> http://www.uni-log.org/logos2015.html
>>> 
>>> Outros artigos apresentados neste evento ja foram publicados num numero 
>>> especial de 
>>> Logica Universalis - Logic and Religion
>>> Volume 11, Issue 1, March de 2017
>>> Issue Editors: Jean-Yves Beziau, Ricardo Silvestre
>>> https://link.springer.com/journal/11787/11/1/page/1
>>> 
>>> Relacionado a este evento vai ser ainda publicado um livro na serie
>>> Sophia Studies in Cross-cultural Philosophy of Traditions and Cultures
>>> http://www.springer.com/series/8880
>>> 
>>> E estamos também ja trabalhando na publicação dos artigos relacionados ao
>>> 2nd  World Congress on Logic and Religion
>>> http://logicandreligion.uw.edu.pl/
>>> organizado na Polonia de 18 a 22 de junho de 2017
>>> 
>>> assim que na preparação do
>>> 3rd  World Congress on Logic and Religion
>>> projetado em Varanasi na India em 2019
>>> http://www.uni-log.org/logos2019.html
>>> 
>>> 
>>> -- 
>>> Você recebeu essa mensagem porque está inscrito no grupo "LOGICA-L" dos 
>>> Grupos do Google.
>>> Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie 
>>> um e-mail para logica-l+u...@dimap.ufrn.br.
>>> Para postar nesse grupo, envie um e-mail para logi...@dimap.ufrn.br.
>>> Acesse esse grupo em 
>>> https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
>>> Para ver essa discussão na Web, acesse 
>>> https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAF2zFLB7YduqAvLLHEf8TM7WH0-bAM%2BBCJ1j%3DSEgJuAAaNMsqA%40mail.gmail.com.
> 
> -- 
> Você recebeu essa mensagem porque está inscrito no grupo "LOGICA-L" dos 
> Grupos do Google.
> Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um 
> e-mail para logica-l+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/20f515f2-d482-49d0-ad96-1de8e10ccd40%40dimap.ufrn.br.

-- 
Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos 
Grupos do Google.
Para cancelar inscrição nesse grupo e parar de receber 

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

[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...

[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)
>>>- 

[Logica-l] Why Priest’s Attack on Classical Negation Can’t Succeed

[jean-yves beziau]

Publicado há  pouco na Logica Universalis:
Classical Negation Strikes Back: Why Priest’s Attack on Classical Negation
Can’t Succeed
Jonas R. Becker Arenhart amd Ederson Safra Melo
https://link.springer.com/article/10.1007/s11787-017-0178-z

-- 
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/CAF2zFLAaLkx4CoQn7X5jN8R1FsYH-%2BeLi5s7oEikC0PEiV48cw%40mail.gmail.com.

[Logica-l] Re: Collected Works by Charles S. Peirce

[jyb]

Ola Tony

Na pagina do tutorial sobre Peirce no UNILOG'2018 que vai ser apresentado 
por William James McCurdy 
voce vai encontrar links para os escritos do Peirce que estão on-line e 
muito mais
http://www.uni-log.org/ULS6-peirce.html

A ideia do nosso site do  UNILOG 
http://www.uni-log.org/
é que não seja so um site para eventos, mas um boa base para a pesquisa, 
uma bússola
uma vez que uma edicao do UNILOG acabou, o site desta edicao conitnua a ser 
util
veja por exemplo a pagina do tutorial sobre Lewis Carroll do UNILOG'2015, 
em Istanbul apresentado por Amirouche Moktefi, com mutios links uteis
http://www.uni-log.org/t5-lewiscarroll.html

JYB



Le vendredi 20 octobre 2017 19:09:49 UTC+2, marmo.tony a écrit :
>
> Caríssimos,
>
> Estou precisando encontrar em PDF a coleção de trabalhos de Peirce.
> Achei um PDF que na verdade fala dos vários trabalhos de editoração de 
> manuscritos dele, não traz os artigos em si numa ordem cronológica.
>
> Quem, por favor, tiver esse PDF, mande-o para mim como e-mail particular. 
> Muito obrigado!
>
> *Dize à sabedoria: Tu és minha irmã...*
>
> Provérbios 7:4 
>
> On 20 Oct 2017, at 06:17, jean-yves beziau  > wrote:
>
> Acabou de ser publicado um numero especial do prestigioso jornal
> Sophia - Logic and Philosophy of Religion
> Volume 56, Issue 2, June 2017
> Issue Editors: Ricardo Sousa Silvestre, Jean-Yvez Beziau
> https://link.springer.com/journal/11841/56/2?wt_mc=alerts.TOCjournals
>
> Artigos publicados aqui são relacionados ao 
> 1st World Congress on Logic and Religion
> organizado em João Pessoa de 1 a 5 de abril de 2015
> http://www.uni-log.org/logos2015.html
>
> Outros artigos apresentados neste evento ja foram publicados num numero 
> especial de 
> Logica Universalis - Logic and Religion
> Volume 11, Issue 1, March de 2017
> Issue Editors: Jean-Yves Beziau, Ricardo Silvestre
> https://link.springer.com/journal/11787/11/1/page/1
>
> Relacionado a este evento vai ser ainda publicado um livro na serie
> Sophia Studies in Cross-cultural Philosophy of Traditions and Cultures
> http://www.springer.com/series/8880
>
> E estamos também ja trabalhando na publicação dos artigos relacionados ao
> 2nd  World Congress on Logic and Religion
> http://logicandreligion.uw.edu.pl/
> organizado na Polonia de 18 a 22 de junho de 2017
>
> assim que na preparação do
> 3rd  World Congress on Logic and Religion
> projetado em Varanasi na India em 2019
> http://www.uni-log.org/logos2019.html
>
>
> -- 
> Você recebeu essa mensagem porque está inscrito no grupo "LOGICA-L" dos 
> Grupos do Google.
> Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie 
> um e-mail para logica-l+u...@dimap.ufrn.br .
> Para postar nesse grupo, envie um e-mail para logi...@dimap.ufrn.br 
> .
> Acesse esse grupo em 
> https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
> Para ver essa discussão na Web, acesse 
> https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAF2zFLB7YduqAvLLHEf8TM7WH0-bAM%2BBCJ1j%3DSEgJuAAaNMsqA%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/20f515f2-d482-49d0-ad96-1de8e10ccd40%40dimap.ufrn.br.

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

[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, "contraposição" é o
> nome dado à (A → B) → (¬B → ¬A).
>
> Curiosamente, a primeira vez que eu vi a "contraposiçã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 você apresentou acima.  A Elaine apresentou o negócio como uma
> regra de inferência que permitiria estabelecer A → B por meio de
> derivação de ¬A a partir de ¬B.  Devo admitir, contudo, que
> apresentado assim, como regra de inferência, o nome "contraposição"
> não me parece *tão* estranho.
>
> Eu não sei porque (¬A → ¬B) → (B → A), com o nome "contraposiçã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 únicos casos que me lembro até agora).
> Talvez tenha aparecido em algum livro ou artigo e as pessoas passaram
> a adotar essa caracterizaçã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 implicações.
>
>(¬φ ∨ ψ) → (φ → ψ)
>>
>
> Esta tambeḿ está correta.  Basta substituir φ por ¬φ na justificativa
> acima.
>
> Mas talvez a relação mais interessante entre disjunção e implicação
> seja dada por
>
> φ ∨ ψ ⇔ ∀χ (φ → χ) → ((ψ → χ) → χ))
>
> que é, basicamente, uma tradução da regra de eliminação em segunda
> ordem (com quantificação sobre sentenças), também chamado de sistema
> Fₐₜ na literatura recente. Essa relacão é inclusive usada no artigo da
> Wikipédia que você 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...

[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, "contraposição" é o
nome dado à (A → B) → (¬B → ¬A).

Curiosamente, a primeira vez que eu vi a "contraposiçã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 você apresentou acima.  A Elaine apresentou o negócio como uma
regra de inferência que permitiria estabelecer A → B por meio de
derivação de ¬A a partir de ¬B.  Devo admitir, contudo, que
apresentado assim, como regra de inferência, o nome "contraposição"
não me parece *tão* estranho.

Eu não sei porque (¬A → ¬B) → (B → A), com o nome "contraposiçã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 únicos casos que me lembro até agora).
Talvez tenha aparecido em algum livro ou artigo e as pessoas passaram
a adotar essa caracterizaçã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 implicações.


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


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

Mas talvez a relação mais interessante entre disjunção e implicação
seja dada por

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

que é, basicamente, uma tradução da regra de eliminação em segunda
ordem (com quantificação sobre sentenças), também chamado de sistema
Fₐₜ na literatura recente. Essa relacão é inclusive usada no artigo da
Wikipédia que você 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...

[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)