Dúvida no ``S5 is a Paraconsistent Logic...'' do JYB

[Eduardo Ochs]

Oi todos,

eu tou tentando ler o ``S5 is a Paraconsistent Logic and so is

first-order classical logic'', do Jean-Yves Beziau (obs: d� pra

baixar ele aqui: http://www.jyb-logic.org/papers.html) e tou com uma

d�vida, que na verdade � uma d�vida sobre S5...

O artigo diz que em S5 com um operador ∼ definido deste jeito,

  ∼a := ⋄¬a

todas estas implicações são estritas,

     8) ∼(a∧b)→(∼a∨∼b)

     9) ∼(∼a∧∼b)→(a∨b)

    10) ∼(a∧∼b)→(∼a∨b)

    11) ∼(∼a∧b)→(a∨∼b)

    12) ∼(∼a∨b)→(a∧∼b)

    13) ∼(a∨b)→(∼a∧∼b)

    14) ∼(a∨∼b)→(∼a∧b)

    15) ∼(∼a∨∼b)→(a∧b)

e eu consegui verificar isso pra todas exceto pra 8...

Eu LaTeXei as minhas anotações e contas e pus aqui:

  http://angg.twu.net/LATEX/2016modal.pdf

Agradeço qualquer ajuda...

  [[]], Eduardo

P.S.: vou começar a estudar LFIs assim que eu entender melhor esse

sistema baseado em S5, juro!

[Marcelo Finger]

Oi Eduardo.

Me parece imediato:

 ∼(a∧b) = ⋄¬(a∧b) <-> ⋄ (¬a ∨ ¬b) -> ⋄¬a ∨ ⋄¬b = (∼a∨∼b)

Qual a dificuldade? A única manipulação modal é a versão ⋄ do axioma K da lógica modal:

⋄ (¬a ∨ ¬b) -> (⋄¬a ∨ ⋄¬b )

[]s

--
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/CADs%2B%2B6gq68QNFiUq2m4pQfuz72aD2A1xYzSpbwA43hqEBw7ESw%40mail.gmail.com.

--

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

[Eduardo Ochs]

Oi Marcelo!

Obrigado, e desculpa eu ter me expressado um pouco mal...

O que você respondeu me ajuda sim, mas a minha dúvida principal era

outra; deixa eu desmontar ela em várias partes.

  a) ∼(a∧b)→(∼a∨∼b) é uma implicação estrita

  b) ∼(a∧b)→(∼a∨∼b) é um teorema

  c) ∼(a∧b)←(∼a∨∼b) não é um teorema

  d) ∼(a∧b)←(∼a∨∼b) tem um contra-modelo

  e) existe um modelo M=(W,R,v) no qual ∼(a∧b)←(∼a∨∼b) é

     falso em pelo menos um dos mundos de W

Você mostrou o (b), o que é útil porque eu tou tentando aprender a

demonstrar coisas em lógica modal (mas tou fazendo isso bem aos

poucos - não é a maior prioridade agora), mas pelo que eu entendi do

paper do JYB os itens c, d e e são "claramente verdade" e só eu é que

não consigo ver porquê...

Deixa eu contar onde eu tou empacado - e desculpem a abordagem

não-padrão.

Vou tentar encontrar o modelo do item (e) acima.

Seja (W,R) um frame com três mundos, todos relacionados entre si (R=W×W).

Sabemos que ∼(a∧b) ou é 111 (verdadeiro em todos os mundos) ou 000

(falso em todos os mundos). Se ∼(a∧b) for 111 então ∼(a∧b)←(∼a∨∼b) vai

ser 111 também, então pra gente ter alguma chance de satisfazer o (e)

neste frame a gente tem que ter ∼(a∧b) valendo 000. O único modo de

∼(a∧b) valer 000 é a gente ter a∧b valendo 111, e aí vamos ter que ter

a valendo 111 e b valendo 111 também. Se a vale 111 e b vale 111,

então ∼a vale 000, ∼b vale 000, ∼a∨∼b vale 000 também, e daí

∼(a∧b)←(∼a∨∼b) vale 111 - e a gente se ferrou.

Dá pra adaptar o argumento acima pra qualquer frame (W,R).

  [[]] =(,

    Eduardo...

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

[Joao Marcos]

> c) ∼(a∧b)←(∼a∨∼b) não é um teorema
> d) ∼(a∧b)←(∼a∨∼b) tem um contra-modelo

Tal afirmação é FALSA. Ambas as consecuções a seguir são válidas em
*qualquer* enquadramento modal, para ambas as negações não-clássicas
óbvias (negation as impossibility, negation as unnecessity):

~(a∨b) ⊢ ∼a∧∼b
~a∨~b ⊢ ∼(a∧b)

Isto segue diretamente da regra de contraposição global (a ⊢ b / ~b ⊢
~a), a qual é válida em qualquer lógica modal normal com modalidades
negativas (analogamente às regras a ⊢ b / #a ⊢ #b, válidas para as
modalidades positivas [] e <>).

Derivações curtinhas podem ser encontradas na Proposition 2.5 deste paper:
https://scholar.google.com.br/citations?view_op=view_citation&hl=pt-BR&user=fVoG0bYAAAAJ&pagesize=100&citation_for_view=fVoG0bYAAAAJ:NaGl4SEjCO4C

Sobre De Morgan, em geral, a Table 5 do outro paper que eu lhe mandei
antes podem lhe ajudar a checar rapidamente quais as condições
correspondentes sobre os enquadramentos, em cada caso:
https://dl.dropboxusercontent.com/u/9291912/papers/16-LMZ-SeqNegMod.pdf

[]s, Joao Marcos

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

[jyb]

Aproveito para dizer que S5 é uma logica paraconsistante bem interessante

tem  boas propriedades logicas e meta-logicas
em particular é self-extensional (vale o teorema de replacement)

também a negação paraconsistente de S5 tem um sentido intuitivo 

comecei a trabalhar nisso desenvolvendo a logica Z 

que é a logica classica positiva junto com uma negacao paraconsistente que tem um sentido intuitivo

Em Z é possivel définir uma negacao classica e a necessidade, entao no final Z = S5

Z é um maneira de reconstruir S5 na base da paraconsitencia

No meu artigo original sobre Z apresentei uma axiomatizaçao tipo Hilbert

(depois  ameliorada por Omori, Nasniewski e Nasniewska)

que  tambem entao é um maneira diferente de axiomatizar S5

A negacao de Z corresponde a ⋄¬a em S5 e é possivel estudar o comportamente deste operador em outras logicas modais que tambem entao sao paraconsistentes

ou que o João Marcos em particular fiz 
JYB