Re: [Logica-l] tableaux + latex
Eduardo,
bem lembrado.
Em 27-05-2013 19:50, Eduardo Ochs escreveu:
> Oi Alessandro!
> Posso dar uma sugestao? =)
> Se voce incluir os headers - como no exemplo abaixo - acho que fica
> bem mais facil as pessoas testarem o seu codigo...
> [[]], Eduardo
>
>
> \documentclass{article}
> \usepackage{xypic}
> \usepackage{amssymb}
> \begin{document}
>
> \xymatrix@R=.7pt@C=8pt{
> 1. && \sim((\lozenge p\&\lozenge q)\supset\lozenge(p\& q))&&&(n)&NTF\\
> 2. && (\lozenge p\&\lozenge q)&&&(n)&1\\
> 3. && \sim\lozenge(p\& q)&&&(n)&&1\\
> 4. && \square\sim(p\& q)&&&(n)&3, MN\\
> 5. && \lozenge p &&& (n) & 2\\
> 6. && \lozenge q &&& (n) & 2\\
> 7. && p &&& (k) & 5, \lozenge \mbox{S}5\\
> 8. && q &&& (l) & 6, \lozenge \mbox{S}5\\
> 9. && \sim(p\& q) &&& (k) & 4,\square\mbox{S}5\\
> 10. && \sim(p\& q)\ar@{-}[dl]\ar@{-}[dr] &&& (l) & 4,\square\mbox{S}5\\
> 11. & \sim p\ (k) & & \sim q\ (k)\ar@{-}[ddl]\ar@{-}[ddr] &&& 9\\
>& \times & & &&& \\
> 12. & & \sim p\ (l)& &\sim q\ (l) && 10\\
> & & \uparrow& &\times&& \\
> }
>
> \end{document}
>
>
>
> On Mon, May 27, 2013 at 5:58 PM, Alessandro Bandeira Duarte
> > wrote:
>
> Caros,
>
> falei do xytree, mas percebi uma solução melhor: xypic, que permite
> modificar o espaçamento das células
>
> http://www.tug.org/applications/Xy-pic/
>
> código:
>
> \xymatrix@R=.7pt@C=8pt{
> 1. && \sim((\lozenge p\&\lozenge q)\supset\lozenge(p\& q))&&&(n)&NTF\\
> 2. && (\lozenge p\&\lozenge q)&&&(n)&1\\
> 3. && \sim\lozenge(p\& q)&&&(n)&&1\\
> 4. && \square\sim(p\& q)&&&(n)&3, MN\\
> 5. && \lozenge p &&& (n) & 2\\
> 6. && \lozenge q &&& (n) & 2\\
> 7. && p &&& (k) & 5, \lozenge \mbox{S}5\\
> 8. && q &&& (l) & 6, \lozenge \mbox{S}5\\
> 9. && \sim(p\& q) &&& (k) & 4,\square\mbox{S}5\\
> 10. && \sim(p\& q)\ar@{-}[dl]\ar@{-}[dr] &&& (l) &
> 4,\square\mbox{S}5\\
> 11. & \sim p\ (k) & & \sim q\ (k)\ar@{-}[ddl]\ar@{-}[ddr] &&& 9\\
>& \times & & &&& \\
> 12. & & \sim p\ (l)& &\sim q\ (l) && 10\\
> & & \uparrow& &\times&& \\
> }
>
>
> http://www.alessandroduarte.com.br/imagens/var/albums/xypic.png?m=1369687662
>
> ___
> Logica-l mailing list
> Logica-l@dimap.ufrn.br
> http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
>
>
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
Re: [Logica-l] tableaux + latex
Oi Alessandro!
Posso dar uma sugestao? =)
Se voce incluir os headers - como no exemplo abaixo - acho que fica
bem mais facil as pessoas testarem o seu codigo...
[[]], Eduardo
\documentclass{article}
\usepackage{xypic}
\usepackage{amssymb}
\begin{document}
\xymatrix@R=.7pt@C=8pt{
1. && \sim((\lozenge p\&\lozenge q)\supset\lozenge(p\& q))&&&(n)&NTF\\
2. && (\lozenge p\&\lozenge q)&&&(n)&1\\
3. && \sim\lozenge(p\& q)&&&(n)&&1\\
4. && \square\sim(p\& q)&&&(n)&3, MN\\
5. && \lozenge p &&& (n) & 2\\
6. && \lozenge q &&& (n) & 2\\
7. && p &&& (k) & 5, \lozenge \mbox{S}5\\
8. && q &&& (l) & 6, \lozenge \mbox{S}5\\
9. && \sim(p\& q) &&& (k) & 4,\square\mbox{S}5\\
10. && \sim(p\& q)\ar@{-}[dl]\ar@{-}[dr] &&& (l) & 4,\square\mbox{S}5\\
11. & \sim p\ (k) & & \sim q\ (k)\ar@{-}[ddl]\ar@{-}[ddr] &&& 9\\
& \times & & &&& \\
12. & & \sim p\ (l)& &\sim q\ (l) && 10\\
& & \uparrow& &\times&& \\
}
\end{document}
On Mon, May 27, 2013 at 5:58 PM, Alessandro Bandeira Duarte <
dedekin...@alessandroduarte.com.br> wrote:
> Caros,
>
> falei do xytree, mas percebi uma solução melhor: xypic, que permite
> modificar o espaçamento das células
>
> http://www.tug.org/applications/Xy-pic/
>
> código:
>
> \xymatrix@R=.7pt@C=8pt{
> 1. && \sim((\lozenge p\&\lozenge q)\supset\lozenge(p\& q))&&&(n)&NTF\\
> 2. && (\lozenge p\&\lozenge q)&&&(n)&1\\
> 3. && \sim\lozenge(p\& q)&&&(n)&&1\\
> 4. && \square\sim(p\& q)&&&(n)&3, MN\\
> 5. && \lozenge p &&& (n) & 2\\
> 6. && \lozenge q &&& (n) & 2\\
> 7. && p &&& (k) & 5, \lozenge \mbox{S}5\\
> 8. && q &&& (l) & 6, \lozenge \mbox{S}5\\
> 9. && \sim(p\& q) &&& (k) & 4,\square\mbox{S}5\\
> 10. && \sim(p\& q)\ar@{-}[dl]\ar@{-}[dr] &&& (l) & 4,\square\mbox{S}5\\
> 11. & \sim p\ (k) & & \sim q\ (k)\ar@{-}[ddl]\ar@{-}[ddr] &&& 9\\
>& \times & & &&& \\
> 12. & & \sim p\ (l)& &\sim q\ (l) && 10\\
> & & \uparrow& &\times&& \\
> }
>
>
> http://www.alessandroduarte.com.br/imagens/var/albums/xypic.png?m=1369687662
>
> ___
> Logica-l mailing list
> Logica-l@dimap.ufrn.br
> http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
>
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
Re: [Logica-l] tableaux + latex
Caros,
falei do xytree, mas percebi uma solução melhor: xypic, que permite
modificar o espaçamento das células
http://www.tug.org/applications/Xy-pic/
código:
\xymatrix@R=.7pt@C=8pt{
1. && \sim((\lozenge p\&\lozenge q)\supset\lozenge(p\& q))&&&(n)&NTF\\
2. && (\lozenge p\&\lozenge q)&&&(n)&1\\
3. && \sim\lozenge(p\& q)&&&(n)&&1\\
4. && \square\sim(p\& q)&&&(n)&3, MN\\
5. && \lozenge p &&& (n) & 2\\
6. && \lozenge q &&& (n) & 2\\
7. && p &&& (k) & 5, \lozenge \mbox{S}5\\
8. && q &&& (l) & 6, \lozenge \mbox{S}5\\
9. && \sim(p\& q) &&& (k) & 4,\square\mbox{S}5\\
10. && \sim(p\& q)\ar@{-}[dl]\ar@{-}[dr] &&& (l) & 4,\square\mbox{S}5\\
11. & \sim p\ (k) & & \sim q\ (k)\ar@{-}[ddl]\ar@{-}[ddr] &&& 9\\
& \times & & &&& \\
12. & & \sim p\ (l)& &\sim q\ (l) && 10\\
& & \uparrow& &\times&& \\
}
http://www.alessandroduarte.com.br/imagens/var/albums/xypic.png?m=1369687662
___
Logica-l mailing list
Logica-l@dimap.ufrn.br
http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
Re: [Logica-l] Fortaleza: ALFAn 2014
Olá, Jean-Yves, estava conversando com o Leclerc, parece mesmo que o encontro do ALFAn (associacao latino-americana de Filosofia Analítica) vai ser em Fortaleza e em maio de 2014. Este ainda vai congregar o encontro da SBFA (Sociedade Brasileira de Filosofia Analítica). Ou seja, vai ser evento grande. Já temos algumas datas: 27-30 de maio. De maneira que nao bate com o seu Square of Oppositions no Vaticano. Fique tranquilo. :) Espero te ver por aqui para a gente fazer turismo eco-etílico-filosófico na bela orla de Fortaleza. abraco, Marcos 2013/5/23 jean-yves beziau > Caro Marcos > > Bom saber que o proximo encontro da ALFAn vai ser em Fortaleza em 2014. > Pretendo ir, espero entao que nao seja no inicio de maio > porque nesta altura vamos organizar o congresso sobre o quadrado no > Vaticano > http://www.square-of-opposition.org/ > > Talvez depois deste ALFAn em Fortaleza seria bom organizar o proximo ALFAn > em Montréal. > O Walter fiz esta sugestao para o encontro de logica matematica > latino-americano SLALM, > mas sem successo, ninguem quiz admitir que o Québec faz parte da america > latina! > André Leclerc talvez consiga a convecer disso os filosofos panaliticos... > > Um abraço, JY > ___ > Logica-l mailing list > Logica-l@dimap.ufrn.br > http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l > ___ Logica-l mailing list Logica-l@dimap.ufrn.br http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
Re: [Logica-l] Lógicas modais proposicionais como teorias de 1a ordem clássicas
2013/5/27 Elaine Pimentel escreveu: > > Em primeiro lugar, eu nunca disse que a Sara inventou sistemas rotulados. Ei, eu não disse que você disse. :-) Mas não pude perder a chance de espicaçar a Sara, que é uma pessoa de uma antipatia cristalina. O cúmulo para mim foi ela lá no UNILOG interromper o Sambin para dizer que ela tinha feito isso ou aquilo, e dentre as coisas que ela citou estava o trabalho do Luca --- que por acaso estava na plateia. A moça é mesmo de mais. 2013/5/27 Marcelo Finger escreveu: > > Em relação à sua pergunta: > >>A pergunta, então, é: tem alguma lógica não-clássica que eu não vou conseguir >>resolver no meu software, simulando-a como uma teoria de primeira ordem >>clássica? > > Bom, pra não ser simulável em primeira ordem, que é turing completa, a > lógica teria de "mais indecidível" que a lógica de primeira ordem. Se entre "lógicas não-clássicas" a gente conta as lógicas não-monotônicas então temos exemplos deste gênero: de fato, enquanto para a lógica clássica de primeira ordem temos um teste positivo para consequência mas não um teste negativo (o complemento da noção de derivabilidade não é recursivamente enumerável), para muitas lógicas não-monotônicas não há sequer um teste positivo. JM -- http://sequiturquodlibet.googlepages.com/ ___ Logica-l mailing list Logica-l@dimap.ufrn.br http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
Re: [Logica-l] Lógicas modais proposicionais como teorias de 1a ordem clássicas
Hola, Valéria e João. Bem, eu ia me abster de responder, mas resolvi fazer um comentário rápido. Em primeiro lugar, eu nunca disse que a Sara inventou sistemas rotulados. O que eu disse foi que o cap 11 do livro de Proof Analysis é um bom lugar para ler sobre sistemas modais rotulados baseados em cálculo de sequentes. E sistemas baseados em dedução natural não são adequados para obter diversos resultados em teoria da prova, em especial aqueles que necessitam o conceito de focalização (pois só há focalização em sistemas que contenham apenas regras de introdução). Em tempo: o livro é muito ruim, de uma maneira geral. Salva-se apenas o cap 11, na minha opinião. Em segundo lugar, eu entendo (e concordo com) a maioria dos argumentos postos pela Valéria mas o que ocorre é que, na verdade, as regras "semânticas" de G3K podem ser vistas como pontos fixos em lógica linear com definições. De fato, os corpos das definições são cláusulas de Horn (portanto positivas) e focar sobre elas resulta em um passo de dedução. Ou seja, elas não interferem no restante da prova (lógica). Mas acho que nada disso interessa diretamente ao Daniel, que colocou a pergunta, em primeiro lugar. Abraços, 2013/5/27 Valeria de Paiva > hmm, obrigada JM pela referencia elogiosa ao meu trabalho com o Torben > sobre Deducao Natural pra logica hibrida construtiva! > > mas e': > > (É inteiramente misteriosa para mim a razão > > pela qual outros autores gastam tempo sobre sistemas dedutivos ad hoc > > para esta ou aquela lógica modal, dado que abordagens deste gênero são > > modulares e amplamente aplicáveis, além de fortemente adequadas do > > ponto de vista lógico.) > > a gente ja discutiu isso algumas vezes. hoje estou meio sem tempo pra > longas conversas, mas nao posso deixar passar em branco o argumento > usual... > > e', botar as relacoes de acessibilidade dos modelos de Kripke na sintaxe > da logica modal 'e um truque bacana que funciona muito bem pra muitas > coisas, mas > 1. isso da' aa nocao de modelo de mundos um papel especial, de definidor > dos sistemas modais, que eu nao sei se 'e razoavel. logicas modais existiam > antes dos modelos de mundos e podem existir sem os mesmos, a principio. a > principio semantica de mundos 'e que nem qq outra semantica (algebrica, > categorica, de valoracoes, etc...) se a semantica de mundos precisa ser > parte da definicao da *sintaxe* das logicas modais, bom entao > ontologicamente elas sao privilegiadas. Por que? > 2. botar a semantica desejada na sintaxe que voce quer modelar (apesar de > logicas hibridas) continua me parecendo roubalheira/cheating... a gente nao > precisa disso pra logica classica, a gente nao precisa disso pra logica > intuicionista, a gente nao precisa pra certos sistemas modais... a nocao de > corretude/soundness fica meio comprometida, pois se a semantica 'e parte da > sintaxe, corretude e' por definicao, nao por demonstracao...essas > discussoes (ou algumas delas) tb estao na tese do Simpson, junto com as > respostas dele de pq as minhas objecoes nao sao relevantes. > 3. quem quer fazer teoria da prova/ou da demonstracao nao pode transformar > as provas que estao interessados em, em provas de primeira ordem. porque > isso destroi a estrutura de demonstracoes que sao tao bem comportadas (como > os slides que o JM sugeriu explicaram) em coisas dentro do universo de 1a > ordem que nao sao bem comportadas de forma nenhuma. > 4. quem como eu e tantos outros esta' interessado nas provas e nao no fato > de um certo teorema ser verdadeiro ou falso, precisa ter muito cuidado com > as traducoes entre sistemas logicos que vai aceitar., pois muitas das > traducoes que preservam valor verdade destroem a estrutura das provas... > > bom, acho que ja chega, ja repetimos alguns dos argumentos tradicionais. > outros interessados em teoria da prova e (pra nao dzer que nao falei das > flores) em focussing ou hypersequentes podem tb dar seus palpites. > > Abracos logicos cordiais > Valeria > > 2013/5/27 Daniel Durante > > > Colegas, > > > > Muito obrigado MESMO pelas referências, já comecei estudar, e elas > > certamente me pouparão muito TEMPO :) E também confirmam minha suspeita > de > > que o assunto era mesmo bem desenvolvido. Aproveito, então, e deixo a > vocês > > uma pergunta séria, mas que vou formular em termos lúdicos: suponha que > por > > alguma limitação qualquer (não muito longe do real, no meu caso), por > > exemplo não tenho lápis e papel, nem boa memória (para fazer as coisas de > > cabeça), nem internet,... e em meu computador só tenho instalado o > software > > "Fitch", que me deixa (e auxilia a) fazer provas em dedução natural na > > lógica clássica de primeira ordem. Bem, com esta ferramenta eu já sei que > > posso construir teorias (conjuntos de premissas) para as diversas versões > > da lógica temporal, descobri que posso fazer o mesmo para os principais > > sistemas de lógica modal, imagino (para o meu desgosto) que posso fazer o > > mesmo inclusive para a lógi
Re: [Logica-l] Lógicas modais proposicionais como teorias de 1a ordem clássicas
Oi Daniel, Não sei entendi sua pergunta. Mas em Lógicas temporais o uso de operadores que são definidos usando-se fecho transitivo ou ponto fixo é bem comum, por exemplo o Until. Voce não irá conseguir expressá-los no sistema Fitch. Um abraço, Mario Em 27 de maio de 2013 15:42, Marcelo Finger escreveu: > Oi Daniel. > > Em relação à sua pergunta: > > >A pergunta, então, é: tem alguma lógica não-clássica que eu não vou > conseguir resolver no meu software, simulando-a como uma teoria de primeira > ordem clássica? > > Bom, pra não ser simulável em primeira ordem, que é turing completa, a > lógica teria de "mais indecidível" que a lógica de primeira ordem. > > Agora, se a v quiser simulação em tempo polinomial, a coisa já fica > mais interessante. Tem muita lógica que é duplamente exponencial, ou > não elementar, e essas, certamente, v não consegue simular. Tente, por > exemplo, simular um produto de duas lógicas intuicionistas e v se > estrepa completamente. > > []s > > Marcelo > > > > > > Eu tenho um palpite, João. A razão pode ser histórica. No caso das > lógicas modais, por exemplo, a regimentação em primeira ordem só se tornou > possível depois que a semântica dos modelos de Kripke se estabeleceu. É > preciso muita reflexão para converter os conceitos de "necessidade" e > "possibilidade", que traduzem-se diretamente em operadores lógicos, em uma > relação binária entre estados possíveis do mundo (ou mundos possíveis) que > rotulam proposições! Outra esquisitice histórica da lógica modal é o nome > dos sistemas! K, T, B, S4, S4.3, S5? > > ___ > > Logica-l mailing list > > Logica-l@dimap.ufrn.br > > http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l > > > > > > -- > Marcelo Finger > Department of Computer Science, Cornell University > > on leave from: > Departament of Computer Science, IME > University of Sao Paulo > http://www.ime.usp.br/~mfinger > ___ > Logica-l mailing list > Logica-l@dimap.ufrn.br > http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l > -- Federal University of Rio de Janeiro www.cos.ufrj.br/~mario ___ Logica-l mailing list Logica-l@dimap.ufrn.br http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
Re: [Logica-l] Lógicas modais proposicionais como teorias de 1a ordem clássicas
Oi Daniel. Em relação à sua pergunta: >A pergunta, então, é: tem alguma lógica não-clássica que eu não vou conseguir >resolver no meu software, simulando-a como uma teoria de primeira ordem >clássica? Bom, pra não ser simulável em primeira ordem, que é turing completa, a lógica teria de "mais indecidível" que a lógica de primeira ordem. Agora, se a v quiser simulação em tempo polinomial, a coisa já fica mais interessante. Tem muita lógica que é duplamente exponencial, ou não elementar, e essas, certamente, v não consegue simular. Tente, por exemplo, simular um produto de duas lógicas intuicionistas e v se estrepa completamente. []s Marcelo > > Eu tenho um palpite, João. A razão pode ser histórica. No caso das lógicas > modais, por exemplo, a regimentação em primeira ordem só se tornou possível > depois que a semântica dos modelos de Kripke se estabeleceu. É preciso muita > reflexão para converter os conceitos de "necessidade" e "possibilidade", que > traduzem-se diretamente em operadores lógicos, em uma relação binária entre > estados possíveis do mundo (ou mundos possíveis) que rotulam proposições! > Outra esquisitice histórica da lógica modal é o nome dos sistemas! K, T, B, > S4, S4.3, S5? > ___ > Logica-l mailing list > Logica-l@dimap.ufrn.br > http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l > -- Marcelo Finger Department of Computer Science, Cornell University on leave from: Departament of Computer Science, IME University of Sao Paulo http://www.ime.usp.br/~mfinger ___ Logica-l mailing list Logica-l@dimap.ufrn.br http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
Re: [Logica-l] Lógicas modais proposicionais como teorias de 1a ordem clássicas
hmm, obrigada JM pela referencia elogiosa ao meu trabalho com o Torben sobre Deducao Natural pra logica hibrida construtiva! mas e': > (É inteiramente misteriosa para mim a razão > pela qual outros autores gastam tempo sobre sistemas dedutivos ad hoc > para esta ou aquela lógica modal, dado que abordagens deste gênero são > modulares e amplamente aplicáveis, além de fortemente adequadas do > ponto de vista lógico.) a gente ja discutiu isso algumas vezes. hoje estou meio sem tempo pra longas conversas, mas nao posso deixar passar em branco o argumento usual... e', botar as relacoes de acessibilidade dos modelos de Kripke na sintaxe da logica modal 'e um truque bacana que funciona muito bem pra muitas coisas, mas 1. isso da' aa nocao de modelo de mundos um papel especial, de definidor dos sistemas modais, que eu nao sei se 'e razoavel. logicas modais existiam antes dos modelos de mundos e podem existir sem os mesmos, a principio. a principio semantica de mundos 'e que nem qq outra semantica (algebrica, categorica, de valoracoes, etc...) se a semantica de mundos precisa ser parte da definicao da *sintaxe* das logicas modais, bom entao ontologicamente elas sao privilegiadas. Por que? 2. botar a semantica desejada na sintaxe que voce quer modelar (apesar de logicas hibridas) continua me parecendo roubalheira/cheating... a gente nao precisa disso pra logica classica, a gente nao precisa disso pra logica intuicionista, a gente nao precisa pra certos sistemas modais... a nocao de corretude/soundness fica meio comprometida, pois se a semantica 'e parte da sintaxe, corretude e' por definicao, nao por demonstracao...essas discussoes (ou algumas delas) tb estao na tese do Simpson, junto com as respostas dele de pq as minhas objecoes nao sao relevantes. 3. quem quer fazer teoria da prova/ou da demonstracao nao pode transformar as provas que estao interessados em, em provas de primeira ordem. porque isso destroi a estrutura de demonstracoes que sao tao bem comportadas (como os slides que o JM sugeriu explicaram) em coisas dentro do universo de 1a ordem que nao sao bem comportadas de forma nenhuma. 4. quem como eu e tantos outros esta' interessado nas provas e nao no fato de um certo teorema ser verdadeiro ou falso, precisa ter muito cuidado com as traducoes entre sistemas logicos que vai aceitar., pois muitas das traducoes que preservam valor verdade destroem a estrutura das provas... bom, acho que ja chega, ja repetimos alguns dos argumentos tradicionais. outros interessados em teoria da prova e (pra nao dzer que nao falei das flores) em focussing ou hypersequentes podem tb dar seus palpites. Abracos logicos cordiais Valeria 2013/5/27 Daniel Durante > Colegas, > > Muito obrigado MESMO pelas referências, já comecei estudar, e elas > certamente me pouparão muito TEMPO :) E também confirmam minha suspeita de > que o assunto era mesmo bem desenvolvido. Aproveito, então, e deixo a vocês > uma pergunta séria, mas que vou formular em termos lúdicos: suponha que por > alguma limitação qualquer (não muito longe do real, no meu caso), por > exemplo não tenho lápis e papel, nem boa memória (para fazer as coisas de > cabeça), nem internet,... e em meu computador só tenho instalado o software > "Fitch", que me deixa (e auxilia a) fazer provas em dedução natural na > lógica clássica de primeira ordem. Bem, com esta ferramenta eu já sei que > posso construir teorias (conjuntos de premissas) para as diversas versões > da lógica temporal, descobri que posso fazer o mesmo para os principais > sistemas de lógica modal, imagino (para o meu desgosto) que posso fazer o > mesmo inclusive para a lógica intuicionista, já que há uma teoria clássica > para S4. Bem, então eu começo a pensar que poderia fazer o mesmo para > lógicas paraconsistentes, relevantes,… A pergunta, então, é: tem alguma > lógica não-clássica que eu não vou conseguir resolver no meu software, > simulando-a como uma teoria de primeira ordem clássica? > Parece que qualquer sistema formal que seja correto e completo com > respeito a alguma formulação semântica que possa ser expressa em uma teoria > de relações passível de ser axiomatizada em primeira ordem se tornaria > equivalente a uma teoria clássica de primeira ordem!!??!! Deve haver algo > errado com esta ideia, pois ela me faz pensar se existe mesmo alguma lógica > não-clássica no sentido de não poder ser tratada classicamente, de ser > incompatível com a lógica clássica! O que vocês acham (ou sabem) sobre o > assunto? > > Saudações, > Daniel > > PS: Sobre o que disse o João Marcos: > > > (É inteiramente misteriosa para mim a razão > > pela qual outros autores gastam tempo sobre sistemas dedutivos ad hoc > > para esta ou aquela lógica modal, dado que abordagens deste gênero são > > modulares e amplamente aplicáveis, além de fortemente adequadas do > > ponto de vista lógico.) > > Eu tenho um palpite, João. A razão pode ser histórica. No caso das lógicas > modais, por exemplo, a regimentação em primeira ordem só
Re: [Logica-l] Grupo = Modelo de ZF ?
Olás, Só pontuando algumas coisinhas; - resultados de consistência em modelos de ZFA, esses tais modelos de permutacoes com átomos, podem ser, em geral, transferidos para ZF por resultados de Pincus; quem quiser eu corro atrás da referência. Carlos devia saber disso já, é meio padrao no contexto de versoes fracas do Axioma da Escolha. - apesar desses Boolean Valued Models serem eventualmente meio misteriosos mesmos, modelos para fragmentos de ZFC nao sao tao difíceis de encontrar: tomamos o conjunto dos conjuntos hereditariamente menor do que kappa, para kappa regular e nao-enumerável (é o tal H(kappa)), e já temos um modelo de ZFC - Partes, tomando kappa suficientemente grande temos versoes restritas de Partes para o que precisarmos, usando LS pra baixo conseguimos um submodelo enumerável - ou elementar para trabalhar como submodelo elementar, ou transitivo se quiser fazer forcing - e... Pronto. Claro que no fundo no fundo é um modelo enumerável, mas a brincadeira de "o que se vê por dentro e o que se vê por fora" está no nosso meio desde o Paradoxo de Skolem e vai continuar né ? - eu tenho um aluno que é louco para fazer tudo em segunda ordem, impressionado por exemplo com a coisa da reta ser categórica em segunda ordem... Ganha-se algumas coisas, perde-se outras (LS é a primeira perda que eu sempre me lembro), mas é sim uma discussao fascinante e que quase nao se faz. Eu no final fico meio que "tranquilo" com a coisa de primeira ordem e segunda ordem porque, quando se vive dentro de ZFC sem nem ir na esquina (que é o que eu faco), como os subconjuntos de um conjunto sao também conjuntos os quantificadores de primeira ordem, para conjuntos, meio que descrevem tudo o que eu preciso (e aqueles papos do tipo "dizer que todo subconjunto é bem ordenado" é de segunda ordem, ou "dizer que todo subconjunto da reta limitado superiormente tem supremo" é de segunda ordem - pra mim nao incomodam, porque os meus quantificadores percorrem conjuntos e, em Teoria dos Conjuntos, tudo é conjunto - incluindo os subconjuntos de um conjunto - e "tudo bem"). Mas é claro que eu só digo isso porque eu nao vou nem na esquina, fico ali em ZFC tranquilinho. A(s) diferenca(s) entre primeira e segunda ordem está(ao) aí para ser(em) estudada(s), investigada(s) e discutida(s). Atés, []s Samuel Quoting Carlos Gonzalez : Não estou compreendendo muito bem qual é o direcionamento que estão querendo dar a esta discussão. Em primeiro lugar, já que nomearam L-S, entram em pauta as questões de relativização, pois se não considerarmos essas questões a coisa passa de confusa para contraditória. Eu gosto da linguagem metafórica na qual é comum falar de relativização. Uma pessoa pode viver num modelo de ZFC que tem grandes cardinais: inaccessíveis, mensuráveis, compactos, etc., e ele tem o maior orgulho dos seus grandes cardinais. Mas ele está enganado, pois vive num modelo enumerável, de modo que o que ele vê como grandes cardinais são, vistos desde fora, conjuntos enumeráveis. Analogamente, uma pessoa poderia viver num modelo de ZFC que é um grupo, sem poder saber nunca desde dentro do modelo, que ele é um grupo. Para piorar a coisa, foram inventados um monte de truques lógicos para evitar o sistema provar a sua própria consistência, contradizendo o Teorema de Gödel. Consequentemente, como não pode demonstrar um ZFC a existência de um conjunto que seja modelo de ZFC, então recorre a coisas como "classes próprias virtuais", fundadas em relativização de quantificadores, etc., etc., etc. Assim, é pensado intuitivamente como um modelo, mas não é um modelo na demonstração formal, no sentido estrito de "modelo". Por exemplo, nos Boolean Valued Models de ZFC, uma álgebra de Boole é o modelo, intuitivamente falando, mas nunca é demonstrado formalmente e no sentido estrito que existe uma tal álgebra. Na minha primeira prova de consistência em teoria de conjuntos, usei uma técnica denominada "modelos de permutação", modelos baseados em grupos de permutações: as permutações de um grupo específico, permutam todo o universo do modelo da teoria de conjuntos, falando intuitivamente. É uma técnica antiga, inventada por Fraenkel nos 1920's, melhorada por Mostowski e que está explicada muito bem no livro de Felgner nas LNM. Alguma das provas originais de Cohen com forcing usa esse sentido intuitivo de permutação para provar a independência do Axioma da Escolha. Quando começa a definir determinados grupos, pode encontrar surpresas. Por exemplo, parece que quase ninguém esperava que os grupos reticulados "ocultassem" uma aritmética, de modo que podem ser aplicados resultados de Gödel. Não sou a pessoa certa para falar de "grupos especiais" (no sentido técnico das palavras, os grupos usados por Miraglia e Dickmann), mas é um outro uso de grupos com ferramentas da teoria de modelos. Em síntese: não vejo nada de estranho uma pessoa morar num modelo de ZFC e que alguém prove que de
Re: [Logica-l] Lógicas modais proposicionais como teorias de 1a ordem clássicas
Colegas, Muito obrigado MESMO pelas referências, já comecei estudar, e elas certamente me pouparão muito TEMPO :) E também confirmam minha suspeita de que o assunto era mesmo bem desenvolvido. Aproveito, então, e deixo a vocês uma pergunta séria, mas que vou formular em termos lúdicos: suponha que por alguma limitação qualquer (não muito longe do real, no meu caso), por exemplo não tenho lápis e papel, nem boa memória (para fazer as coisas de cabeça), nem internet,... e em meu computador só tenho instalado o software "Fitch", que me deixa (e auxilia a) fazer provas em dedução natural na lógica clássica de primeira ordem. Bem, com esta ferramenta eu já sei que posso construir teorias (conjuntos de premissas) para as diversas versões da lógica temporal, descobri que posso fazer o mesmo para os principais sistemas de lógica modal, imagino (para o meu desgosto) que posso fazer o mesmo inclusive para a lógica intuicionista, já que há uma teoria clássica para S4. Bem, então eu começo a pensar que poderia fazer o mesmo para lógicas paraconsistentes, relevantes,… A pergunta, então, é: tem alguma lógica não-clássica que eu não vou conseguir resolver no meu software, simulando-a como uma teoria de primeira ordem clássica? Parece que qualquer sistema formal que seja correto e completo com respeito a alguma formulação semântica que possa ser expressa em uma teoria de relações passível de ser axiomatizada em primeira ordem se tornaria equivalente a uma teoria clássica de primeira ordem!!??!! Deve haver algo errado com esta ideia, pois ela me faz pensar se existe mesmo alguma lógica não-clássica no sentido de não poder ser tratada classicamente, de ser incompatível com a lógica clássica! O que vocês acham (ou sabem) sobre o assunto? Saudações, Daniel PS: Sobre o que disse o João Marcos: > (É inteiramente misteriosa para mim a razão > pela qual outros autores gastam tempo sobre sistemas dedutivos ad hoc > para esta ou aquela lógica modal, dado que abordagens deste gênero são > modulares e amplamente aplicáveis, além de fortemente adequadas do > ponto de vista lógico.) Eu tenho um palpite, João. A razão pode ser histórica. No caso das lógicas modais, por exemplo, a regimentação em primeira ordem só se tornou possível depois que a semântica dos modelos de Kripke se estabeleceu. É preciso muita reflexão para converter os conceitos de "necessidade" e "possibilidade", que traduzem-se diretamente em operadores lógicos, em uma relação binária entre estados possíveis do mundo (ou mundos possíveis) que rotulam proposições! Outra esquisitice histórica da lógica modal é o nome dos sistemas! K, T, B, S4, S4.3, S5? ___ Logica-l mailing list Logica-l@dimap.ufrn.br http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
Re: [Logica-l] Grupo = Modelo de ZF ?
Na verdade, como diz o Décio, dá pra construir um grupo que não cabe dentro de ZF. Sent from my iPhone On 26/05/2013, at 13:59, Décio Krause wrote: > Mas que tal se usássemos ZF de segunda ordem? L-S não poderia ser invocado... > Como se vê, o tema é legal e sutil. > Abraços > Décio > > > > -- > Décio Krause > Departamento de Filosofia > Universidade Federal de Santa Catarina > 88040-900 Florianópolis - SC - Brasil > http://www.cfh.ufsc.br/~dkrause > -- > > Em 25/05/2013, às 13:26, Joao Marcos escreveu: > >>> (Nao sei se G é candidato a modelar ZFC; nao vejo porque, por exemplo, valha >>> o Axioma da Substituicao com os quantificadores restritos a G, mas é algo a >>> se pensar, claro) >> >> Queria acrescentar que eu acho que não é um candidato. Eu só achei >> que o "argumento da cardinalidade" formulado antes não era >> convincente, pois os modelos de ZF afinal não precisam ser >> "grandes"... E, claro, você tem razão em dizer que "existem grupos >> para cada cardinalidade" (Löwenheim-Skolem na forma *ascendente* >> poderia ser invocado, neste caso, mesmo se não conhecêssemos os >> exemplos que você sugeriu?). >> >> Abraços, JM >> >> -- >> http://sequiturquodlibet.googlepages.com/ > ___ > Logica-l mailing list > Logica-l@dimap.ufrn.br > http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l ___ Logica-l mailing list Logica-l@dimap.ufrn.br http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
