Planar Heyting Algebras for Children

[Eduardo Ochs]

Gente, deixa eu divulgar uma coisa aqui apesar dela ser um

"work in progress" e 90% dela ser sobre didática...

Aqui tem um artigo no qual eu tou trabalhando,

  http://angg.twu.net/LATEX/2016planar-has.pdf

que é parte de um projeto de apresentar varios assuntos "pra

crianças", onde esse "crianças" quer dizer "pessoas com bem

pouca maturidade matemática"... boa parte do que tá nesse

(proto-)artigo eu expus, com montes de exercícios, pros alunos de

uma optativa de que tou dando, e o modo de expor foi se ajustando a

eles...

Esses alunos são do curso de Ciência da Computação daqui

de Rio das Ostras, e todos eles já fizeram Matemática Discreta e

DEVERIAM ter uma certa prática com teoremas e demonstrações,

mas o que eu fui vendo é que metade da turma dessa minha optativa

pensa e escreve besteiras incríveis quando é obrigada a lidar

com teoremas gerais - eles são "crianças" no sentido acima,

afinal! - então eu puxei o foco para "calcular coisas"; por

exemplo, num dia eles não conseguiam ter certeza se a função

  f = {(1,10), (2,20)}

era função de um certo conjunto A num certo conjunto B, e como

as discussões deles não pareciam estar indo a lugar nenhum eu

lembrei a eles que

  f:A→B   ↔   (f⊂A×B) & (∀a∈A. ∃!b∈B. (a,b)∈f)

botei todo mundo pra calcular

  (f⊂A×B) & (∀a∈A. ∃!b∈B. (a,b)∈f)

para vários valores de A e B...

Parêntese pra quem achar o proto-paper irritante demais por a) ter

exemplos em todo lugar e b) não ir muito longe: as seções finais dele

mostram/vão mostrar (algumas já estão escritas) como visualizar

"closure operators" em "planar heyting algebras"; aí depois disso

vem - mas provavelmente em papers separados - uma parte que ainda não

existe sobre como usar diagramas parecidos com os do proto-paper pra

falar de categorias e funtores, e depois uma parte co-autorada com o

Peter Arndt sobre feixes e feixificação em toposes; a gente conseguiu

encontrar uma tradução "pra crianças" pra boa parte dos teoremas de

uma seção do livro do Johnstone (o "Sketches of an Elephant - A Topos

Theory Compendium"), mas isso foi no ano passado, quando a gente ainda

não tinha idéia de que linguagem usar pra escrever os nossos

resultados... e a gente tem um _pouquinho_ de material sobre S4 e S5

pra crianças guardado também, mas lembrem que as crianças ainda estão

na fase de aprender a calcular e visualizar coisas, então esse

material cobre pouquíssimos teoremas...

Se alguém aqui tiver idéias sobre como visualizar lógicas

paraconsistentes eu ADORARIA discutir isso... a única lógica

paraconsistente que eu já entendi até hoje é uma que o Jean-Yves

Beziau montou em cima de S5 ("S5 is a paraconsistent logic and so is

first-order classical logic", 2002), eu sou péssimo nessas coisas.

De novo: desculpem eu estar divulgando algo que está incompleto, mas

um monte de gente (5 < n < 20) já tinha me pedido pra escrever direito

porque é que as tais ZHAs (secão 4 do artigo) eram Heyting Algebras (o

porquê tá na seção 13), e porque é que a implicação em ZHAs podia ser

calculada usando um certo algoritmo olhométrico rapidíssimo (seções 6

e 7), e essas partes já estão prontas.

  [[]] =),

    Eduardo Ochs

[Joao Marcos]

> Se alguém aqui tiver idéias sobre como visualizar lógicas
> paraconsistentes eu ADORARIA discutir isso... a única lógica
> paraconsistente que eu já entendi até hoje é uma que o Jean-Yves
> Beziau montou em cima de S5 ("S5 is a paraconsistent logic and so is
> first-order classical logic", 2002), eu sou péssimo nessas coisas.

Vale notar que a mesma estratégia pode ser aplicada a qualquer lógica
modal normal ("Nearly every normal modal logic is paranormal", Logique
et Analyse 2005). Não me parece que as crianças achariam mais difícil
entender estes outros sistemas mais fracos do que entender S5. Tome ◡
para a negação paraconsistente modal que funciona como um "diamante
negativo" (negation as unnecessity). Algumas classes de
enquadramentos modais usuais são então facilmente caracterizáveis, por
exemplo:
[reflexividade] p∨◡p
[simetria] ◡◡p => p
[euclidianidade] ◡p∧◡◡p => q
Observe que nem todo paraconsistentista ficará contente com o axioma
característico da euclidianidade, o qual mostra que a lógica em
questão é "parcialmente explosiva em contato com ◡".

Sobre a "visualização de lógicas", talvez você curta ver a negação ◡
como *dual* da negação ◠, uma negação paracompleta modal que funciona
como um "box negativo" (negation as impossibility). Isto é similar,
claro, à interpretação intuicionista da negação. Do ponto de vista
algébrico você poderia trabalhar com álgebras duais à álgebra de
Heyting ou, melhor ainda, com álgebras bi-Heyting, bem estudadas na
literatura (e também na literatura categorial). Se você tiver
interesse em trabalhar nisto, fique à vontade para entrar em contato
direto comigo!

No paper que segue você encontrará um estudo em que as duas negações,
◡ e ◠, são postas na mesma linguagem. Várias situações interessantes
de interação têm lugar.
https://dl.dropboxusercontent.com/u/9291912/papers/16-LMZ-SeqNegMod.pdf
São também oferecidos no paper cálculos de sequentes com a propriedade
de analiticidade para várias lógicas nesta linguagem, estendida por
conectivos de restauração para internalizar consistência e
determinação.

Abraços,
Joao Marcos

--
http://sequiturquodlibet.googlepages.com/

[Eduardo Ochs]

Oi João & outros,

acho que tou precisando de uma ajuda em algo preliminar antes de eu

tentar fazer as figuras para as negações paraconsistentes...

No p.149 do "Modal Logic - An Introduction" do Chellas tem uma figura

que dá a ordem parcial das 7 modalidades sem negação em S4; ele diz

que a gente consegue provar que

  ◻P → P → ⋄P

  ◻P → ◻⋄◻P → ⋄◻P → ⋄◻⋄P → ⋄P

  ◻P → ◻⋄◻P → ◻⋄P → ⋄◻⋄P → ⋄P,

e que cada uma dessas implicações é "estrita" no sentido de que para

cada uma delas a gente consegue um "relational model" M=(W,R,v) no

qual a implicação reversa não é verdade.

Eu tou com muita dificuldade de falsificar (falsear?) estas duas aqui,

  ◻P → ◻⋄◻P

  ⋄◻⋄P → ⋄P,

alguém se lembra como se faz isso e toparia dar uma dica?

Na verdade eu tou tentando conseguir um relational model que

falsifique todas estas implicações reversas de uma vez...

           ⋄P

          ^  ^

         /    \

      ⋄◻⋄P     \

      ^  ^      \

     /    \      \

  ◻⋄P     ⋄◻P    P         (*)

     ^    ^      ^

      \  /      /

      ◻⋄◻P     /

        ^     /

         \   /

          ◻P

reparem que se

            1     2

           / \   /

(W,R) =   v   v v    = ({1,2,3,4}, {(1,3),(1,4),(2,4)})

         3     4

e v(P) = {(1,1),(2,0),(3,0),(4,1)} podemos representar P como

     1     0

    / \   /

   v   v v

  0     1

ou, mais compactamente, como:

   1 0

  0 1           

aí temos

  ◻P =  0 0

       0 1  ,

  ⋄P =  1 1

       0 1  ,

etc, e o diagrama (*) acima vira, neste relational model,

            1 1

           0 1

       =( ^   ^

         /     \

       1 1      \

      0 1        \

      ^  ^ =(     \

     /    \        \

   0 1      1 1     1 0         

  0 1      0 1     0 1      

     ^    ^        ^

   =( \  /        /

       0 1       /

      0 1       /

         ^     /

       =( \   /

           0 0

          0 1

eu marquei com "=("s os lugares onde a gente gostaria que as setas

distinguissem valores mas não distinguem.

Eu até consegui um outro relational model melhor, que só tem dois

"=("s, mas consegui ele meio no chute, e ele é bem pior de digitar

porque a relational frame dele é esta (reparem no truque de que os

mundos 6 e 7 se vêem um ao outro!):

           1      2       3      4

           | \  / |  | \  / |

  (W,R) =  |  \/  |  |  \/  |

           |  /\  |  |  /\  |

           v v  v v  v v  v v

           5      6 <---> 7      8

...mas, como eu falei, não estou conseguindo falsear/falsificar

  ◻P → ◻⋄◻P   e

  ⋄◻⋄P → ⋄P.

Tou fazendo alguma besteira tentando encontrar contramodelos usando

tableux pra S4... e, pior, acho que o Marcelo Coniglio me mostrou como

resolver isso quando a gente se encontrou em Istambul, mas o caderno

que a gente usou pra escrevinhar e discutir ficou em Rio das Ostras e

eu tou no Rio e só vou voltar pra lá na segunda... 8-(

Thanks in advance =),

  Eduardo

--
http://sequiturquodlibet.googlepages.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+unsubscribe@dimap.ufrn.br.
Para postar neste grupo, envie um e-mail para logi...@dimap.ufrn.br.
Visite este grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/.
Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAO6j_Lj1%3DO_na6fWjQZ4gC2xo4rUek1S6MmSHUYADgeaMU6MEA%40mail.gmail.com.

[cmor...@cfh.ufsc.br]

Caro Eduardo,

mas essas duas fórmulas:

> ◻P → ◻⋄◻P
> ⋄◻⋄P → ⋄P,

são válidas em S4; veja na lista abaixo que você colocou. Você está com
dificuldades para falsear as implicações na outra direção, ou seriam
outras as fórmulas causando problemas?

Abraços,

Cezar

>> [1]

>> São também oferecidos no paper cálculos de sequentes com a
>> propriedade
>> de analiticidade para várias lógicas nesta linguagem, estendida
>> por
>> conectivos de restauração para internalizar consistência e
>> determinação.
>>
>> Abraços,
>> Joao Marcos
>>
>> --

>> http://sequiturquodlibet.googlepages.com/ [2]

>>
>> --
>> 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/ [3].

>> Para ver esta discussão na web, acesse
>>
> https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAO6j_Lj1%3DO_na6fWjQZ4gC2xo4rUek1S6MmSHUYADgeaMU6MEA%40mail.gmail.com

>> [4].
>
> --
> 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/CADs%2B%2B6hc0njRHKspRqp-kSR_cnaF0_RU_VjLHhyfnd4Hq5Pi2A%40mail.gmail.com
> [5].
>
>
> Links:
> ------
> [1]
> https://dl.dropboxusercontent.com/u/9291912/papers/16-LMZ-SeqNegMod.pdf
> [2] http://sequiturquodlibet.googlepages.com/
> [3] https://groups.google.com/a/dimap.ufrn.br/group/logica-l/
> [4]
> https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAO6j_Lj1%3DO_na6fWjQZ4gC2xo4rUek1S6MmSHUYADgeaMU6MEA%40mail.gmail.com
> [5]
> https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CADs%2B%2B6hc0njRHKspRqp-kSR_cnaF0_RU_VjLHhyfnd4Hq5Pi2A%40mail.gmail.com?utm_medium=email&utm_source=footer

[Eduardo Ochs]

Oi Cezar,

Desculpa, cê tá certo, falei besteira no meu e-mail...

O correto é isto aqui:

    ◻P → ◻⋄◻P     é teorema

    ◻⋄◻P → ◻P     não é teorema

    ◻⋄◻P → ◻P     tem contra-modelo (qual?)

  ¬(◻⋄◻P → ◻P)    tem modelo (qual?)

Tou procurando um contra-modelo para ◻⋄◻P → ◻P...

  [[]] =\,

    Eduardo

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/2212e232eceb4a51da201e5c16e436d2%40cfh.ufsc.br.

[cmor...@cfh.ufsc.br]

Oi, Eduardo,

ah, ok. Para a fórmula ◻⋄◻P → ◻P, acho que isso é um contramodelo (se
fiz as contas certo):

W = {a,b}
R = {(a,a), (b,b), (a,b)} (R é reflexiva e transitiva)
V(P) = {a} (ou seja, P é falsa só no mundo a)

Em b, as fórmulas P, ◻P, ⋄◻P, ◻⋄◻P, e ◻⋄◻P → ◻P são todas verdadeiras.

Em a, P e ◻P são falsas, mas ⋄◻P é verdadeira (pois ◻P é verdadeira em
b) e ◻⋄◻P é verdadeira (pois ⋄◻P é verdadeira tanto em a quanto em b).
Isso torna ◻⋄◻P → ◻P falsa (em a).

Uma variante disso (P só é falsa em b) deve falsificar ⋄P → ⋄◻⋄P.

Se errei nas contas, me avisa, por favor, que eu tento de novo.

Abraços,

Cezar

> [3]

>
>> [1]
>> São também oferecidos no paper cálculos de sequentes com a
>> propriedade
>> de analiticidade para várias lógicas nesta linguagem, estendida
>> por
>> conectivos de restauração para internalizar consistência e
>> determinação.
>>
>> Abraços,
>> Joao Marcos
>>
>> --

>> http://sequiturquodlibet.googlepages.com/ [1] [2]

>>
>> --
>> 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/ [2] [3].

>> Para ver esta discussão na web, acesse
>
> https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAO6j_Lj1%3DO_na6fWjQZ4gC2xo4rUek1S6MmSHUYADgeaMU6MEA%40mail.gmail.com
> [4]
>
>> [4].
>
> --
> 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/ [2].

> Para ver essa discussão na Web, acesse
> https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CADs%2B%2B6hc0njRHKspRqp-kSR_cnaF0_RU_VjLHhyfnd4Hq5Pi2A%40mail.gmail.com
> [5]
> [5].
>
> Links:
> ------
> [1]
> https://dl.dropboxusercontent.com/u/9291912/papers/16-LMZ-SeqNegMod.pdf

> [3]
> [2] http://sequiturquodlibet.googlepages.com/ [1]
> [3] https://groups.google.com/a/dimap.ufrn.br/group/logica-l/ [2]
> [4]
> https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAO6j_Lj1%3DO_na6fWjQZ4gC2xo4rUek1S6MmSHUYADgeaMU6MEA%40mail.gmail.com
> [4]
> [5]
> https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CADs%2B%2B6hc0njRHKspRqp-kSR_cnaF0_RU_VjLHhyfnd4Hq5Pi2A%40mail.gmail.com?utm_medium=email&utm_source=footer
> [6]

>
> --
> 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/ [2].

> Para ver esta discussão na web, acesse

> https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/2212e232eceb4a51da201e5c16e436d2%40cfh.ufsc.br
> [7].

>
> --
> 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/CADs%2B%2B6gvQ1s5fG_TtisVsM9eYBuFZnPgS57o0zReyNYfZgaKJw%40mail.gmail.com
> [8].
>
>
> Links:
> ------
> [1] http://sequiturquodlibet.googlepages.com/
> [2] https://groups.google.com/a/dimap.ufrn.br/group/logica-l/
> [3]
> https://dl.dropboxusercontent.com/u/9291912/papers/16-LMZ-SeqNegMod.pdf

> [4]
> https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAO6j_Lj1%3DO_na6fWjQZ4gC2xo4rUek1S6MmSHUYADgeaMU6MEA%40mail.gmail.com
> [5]
> https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CADs%2B%2B6hc0njRHKspRqp-kSR_cnaF0_RU_VjLHhyfnd4Hq5Pi2A%40mail.gmail.com

> [6]
> https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CADs%2B%2B6hc0njRHKspRqp-kSR_cnaF0_RU_VjLHhyfnd4Hq5Pi2A%40mail.gmail.com?utm_medium=email&amp;utm_source=footer
> [7]
> https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/2212e232eceb4a51da201e5c16e436d2%40cfh.ufsc.br
> [8]
> https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CADs%2B%2B6gvQ1s5fG_TtisVsM9eYBuFZnPgS57o0zReyNYfZgaKJw%40mail.gmail.com?utm_medium=email&utm_source=footer

[Eduardo Ochs]

Obrigado, Cezar e Tony!!!

Consegui um contra-modelo pra cada seta do diagrama,

e depois consegui juntar tudo, ó:

          1     2     3

           \   / \   /

  (W,R) =   v v   v v

             4     5    6<->7

        = {(1,2,3,4,5,6,7),

           {(1,4), (2,4), (2,5), (3,5), (6,7), (7,6)}

          }

  v(   P) = {    3,4,    7}

  v(  ◻P) = {      4      }

  v( ⋄◻P) = {1,2,  4      }

  v(◻⋄◻P) = {1,   4      }

  v(  ⋄P) = {1,2,3,4,  6,7}

  v( ◻⋄P) = {1,    4,  6,7}

  v(⋄◻⋄P) = {1,2,  4,  6,7}

            1 1 1

             1 0  11

             ^    ^

            /      \

           /        \                         ⋄P

       1 1 0         \                       ^  ^

        1 0  11       \            /    \

        ^   ^          \         ⋄◻⋄P     \

       /     \          \         ^  ^      \

      /       \          \        /    \      \

  1 0 0      1 1 0       0 0 1     ◻⋄P     ⋄◻P     P

   1 0  11    1 0  00     1 0  01       ^    ^      ^

      ^         ^        ^         \  /      /

       \       /        /         ◻⋄◻P     /

        \     /        /           ^     /

        1 0 0         /            \   /

         1 0  00     /             ◻P

            ^       /

             \     /

              \   /

             0 0 0

              1 0  00

  [[]], jingobéu, etc, etc e tal! =)

    Eduardo

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/01713bc84cf8e02bcd5cff4fb6071151%40cfh.ufsc.br.