um probleminha com logica intuicionista...

[Valeria de Paiva]

prezados colegas,

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

Acho que  tem um "erro" em https://en.wikipedia.org/wiki/Intuitionistic_logic

onde  na secao 9 alguem diz que:

Relation to classical logic[edit]

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

• {\displaystyle \phi \lor \lnot \phi } (Law of the excluded middle. May also be formulated as {\displaystyle (\phi \to \chi )\to ((\lnot \phi \to \chi )\to \chi )}.)
• {\displaystyle \lnot \lnot \phi \to \phi } (Double negation elimination)
• {\displaystyle ((\phi \to \chi )\to \phi )\to \phi } (Peirce's law)
• {\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 )}
• {\displaystyle (\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/

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

--
Você recebeu essa mensagem porque está inscrito no grupo "LOGICA-L" dos Grupos do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+unsubscribe@dimap.ufrn.br.
Para postar nesse grupo, envie um e-mail para logi...@dimap.ufrn.br.
Acesse esse grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAESt%3DXtQF5fvc8xt%2BaKJ2A5d6bw33taeFkFv0j_PCGJQ6UCSGg%40mail.gmail.com.

--

Thiago Nascimento, Mestrando PPgSC - UFRN.

[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

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/CAESt%3DXtQF5fvc8xt%2BaKJ2A5d6bw33taeFkFv0j_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+unsubscribe@dimap.ufrn.br.
Para postar nesse grupo, envie um e-mail para logi...@dimap.ufrn.br.
Acesse esse grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.

Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAOHRVBVYL6xH5E%3D7ni-_sH0pMxwEdwQD-Q265E_KxeLZJM%2B-sw%40mail.gmail.com.

[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

--
Você recebeu essa mensagem porque está inscrito no grupo "LOGICA-L" dos Grupos do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+unsubscribe@dimap.ufrn.br.
Para postar nesse grupo, envie um e-mail para logi...@dimap.ufrn.br.
Acesse esse grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.

Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAESt%3DXtQF5fvc8xt%2BaKJ2A5d6bw33taeFkFv0j_PCGJQ6UCSGg%40mail.gmail.com.

[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" <valeria...@gmail.com>
> 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

>> <https://en.wikipedia.org/w/index.php?title=Intuitionistic_logic&action=edit&section=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)

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

>> <https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAESt%3DXtQF5fvc8xt%2BaKJ2A5d6bw33taeFkFv0j_PCGJQ6UCSGg%40mail.gmail.com?utm_medium=email&utm_source=footer>
>> .
>>
>
> --
> Você está recebendo esta mensagem porque se inscreveu no grupo

> "LOGICA-L" dos Grupos do Google.
> Para cancelar inscrição nesse grupo e parar de receber e-mails dele,

> envie um e-mail para logica-l+u...@dimap.ufrn.br.
> Para postar neste grupo, envie um e-mail para logi...@dimap.ufrn.br.
> Visite este grupo em
> https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
> Para ver esta discussão na web, acesse
> https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAAPnweACzeBQqKjVR5jth2Y%3DzmqGmA_Pm4ssOPg5D6vGp%2B3AOA%40mail.gmail.com.

[Hermógenes Oliveira]

Valeria de Paiva <valeria...@gmail.com> 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

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

--
Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos Grupos do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+u...@dimap.ufrn.br.
Para postar neste grupo, envie um e-mail para logi...@dimap.ufrn.br.
Visite este grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.

Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/20171024103907.Horde.StcBDM_NGGFij6cUvk478_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

-------------------------------------------------------- 

[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

Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/20171024040835.Horde.FIpwwQ6QoRzTHzQgYuI6dQ3%40webmail.ime.usp.br.

--

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

[Francisco Miraglia]

Caro Marcelo,

Obrigado!!

Abraços,

Chico

>> map.ufrn.br/d/msgid/logica-l/20171024040835.Horde.FIpwwQ6Qo
>> RzTHzQgYuI6dQ3%40webmail.ime.usp.br.

>>
>
>
>
> --
> 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+u...@dimap.ufrn.br.
> Para postar neste grupo, envie um e-mail para logi...@dimap.ufrn.br.
> Visite este grupo em
> https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
> Para ver esta discussão na web, acesse

> https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CABqmzx0yU7rgAoaOJBZwdg%2BC42C5qeqeViZqULXspOyszaD1-A%40mail.gmail.com.

[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

[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

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

[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

> https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAESt%3DXvrHUGvEJqCDVZBX4tjgHwDOAM41H2C2h3vgdBbG9F9qw%40mail.gmail.com.

[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 <valeria...@gmail.com>:

> 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
> <https://dl.acm.org/author_page.cfm?id=81100285875&coll=DL&dl=ACM&trk=0&cfid=822206738&cftoken=84188042>

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

> <https://dl.acm.org/inst_page.cfm?id=60003771&CFID=822206738&CFTOKEN=84188042>

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

> <https://www.google.com/url?sa=t&rct=j&q=&esrc=s&source=web&cd=5&ved=0ahUKEwiXrPfPsInXAhUjiVQKHYixAesQFghAMAQ&url=http%3A%2F%2Fwww.cs.man.ac.uk%2F~petera%2Fruss-praw.ps.gz&usg=AOvVaw0R-2D-kiwKnCxmYNQ0bPtJ>

> https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAESt%3DXvzGrB1gFLDJ9%3DeUibbaPWmx-FkAfVBzSZ8qJcuE1aQJA%40mail.gmail.com.

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

[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

[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

--

Você recebeu essa mensagem porque está inscrito no grupo "LOGICA-L" dos Grupos do Google.

Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+unsubscribe@dimap.ufrn.br.

Para postar nesse grupo, envie um e-mail para logi...@dimap.ufrn.br.
Acesse esse grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.

Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CACHAqBmf%2BtauDjypWfOL%2B5jg0Eg%3D%3D9F5oFHZ2HHbmxJRJ9Xkqw%40mail.gmail.com.

[Andrea Loparic]

Marcelo, caro, é por essas e outras que crianças e velhinhas,

especialmente as inteligentes, se dão tão bem!

 

--

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/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ê recebeu essa mensagem porque está inscrito no grupo "LOGICA-L" dos Grupos do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+unsubscribe@dimap.ufrn.br.
Para postar nesse grupo, envie um e-mail para logi...@dimap.ufrn.br.
Acesse esse grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.

Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CABqmzx0agJUPdhoUH8gb3qyTb0CHUFZqq6VD%2BPA6MBGLBnnt_g%40mail.gmail.com.

[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

Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CABqmzx0agJUPdhoUH8gb3qyTb0CHUFZqq6VD%2BPA6MBGLBnnt_g%40mail.gmail.com.

--
Você recebeu essa mensagem porque está inscrito no grupo "LOGICA-L" dos Grupos do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+unsubscribe@dimap.ufrn.br.
Para postar nesse grupo, envie um e-mail para logi...@dimap.ufrn.br.
Acesse esse grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.

Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CACHAqBmsn3kz_z%3DRS1S%2BVhPm6Mf_bcUzUpJ13yMJ%2BNon4oC%3DBA%40mail.gmail.com.

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

 

Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/20171024040835.Horde.FIpwwQ6QoRzTHzQgYuI6dQ3%40webmail.ime.usp.br.

[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

Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+unsubscribe@dimap.ufrn.br.

Para postar nesse grupo, envie um e-mail para logi...@dimap.ufrn.br.
Acesse esse grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.

Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAJGvw-3rtaS6%2B45LRrLi9J-eefupmA9LRJO95ZHcxHFaZ7Mi6g%40mail.gmail.com.

[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&rep=rep1&type=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

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/CAJGvw-3rtaS6%2B45LRrLi9J-eefupmA9LRJO95ZHcxHFaZ7Mi6g%40mail.gmail.com.

--

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

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

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/CAJGvw-3rtaS6%2B45LRrLi9J-eefupmA9LRJO95ZHcxHFaZ7Mi6g%40mail.gmail.com.

--

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

--
Você recebeu essa mensagem porque está inscrito no grupo "LOGICA-L" dos Grupos do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+unsubscribe@dimap.ufrn.br.
Para postar nesse grupo, envie um e-mail para logi...@dimap.ufrn.br.
Acesse esse grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.

Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAESt%3DXuqsrVGenCd0Mq2P7xmUzosbx%2BTXweGo69xfb6vp%3D8F7A%40mail.gmail.com.

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

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