ok mais 2 centavos daqui de longe: gostaria de entender melhor o que JM quer dizer com: >note com efeito que a regra de substituição uniforme não se aplica ao símbolo de absurdo, como um *conectivo* nulário, tal como se aplica a sentenças atômicas.
da' pra repetir a ideia aqui? como eu passei uma boa parte da minha vida dizendo que interdefinabilidade entre conectivos e' ruim acho que preciso responder a: >Por outro lado, não vejo porque deveríamos pensar sempre na negação como conectivo *derivado*. Aliás, isto parece até uma ideia bem ruinzinha, do ponto de vista de lógicas não-clássicas em que a interdefinibilidade entre conectivos clássicos usualmente se perde pelo caminho. sim, seria bom nao ter a negação como conectivo derivado, mas nao sei como escapar disso. a consideracao maior 'e a consistencia como um todo e a relacao com logica classica. e' dessa nocao pre-formal de ecumenismo do Prawitz (no festscrift do Luiz Carlos) que vem a constraint que negacao 'e derivada, pra mim. se eu soubesse (re)construir o edificio inteiro (logica classica e intuicionista e suas inter relacoes) sem depender da hipotese de que negacao 'e implicacao no absurdo, eu o faria. mas pra saber fazer isso, precisaria de reprovar todos os resultados que temos com a nocao derivada de negacao. isso eu nao sei fazer e nem sei se e' possivel. abs Prawitzianos, 2017-04-07 5:54 GMT-07:00 Hermógenes Oliveira <hermogenes.oliveira@student. uni-tuebingen.de>: > Bruno Bentzen <b.bent...@hotmail.com> escreveu: > > > Oi Hermógenes, > > Olá, Bruno. > > > [...] > > > > PS: Posso estar enganado, mas acho um pouco equivocado e confuso usar > > a palavra “completude” (um termo de cunho técnico ou meta-matemático) > > neste caso quando estamos nos tratando de uma semântica informal ou > > justificativa filosófica (até onde sei, o estudo de semânticas formais > > para a lógica intuicionista nunca foi uma das preocupações principais > > do Martin-Löf). De qualquer forma, não vejo porque as explicações de > > significado não seriam “completas”, no sentido informal, para a MLETT, > > que, repito, é a única das duas vertentes tradicionais de sua teoria > > de tipos que interessa ao intuicionista. > > Você está correto em observar que as explicações semânticas de > Martin-Löf não foram propostas como uma semântica formal e que o estudo > de semânticas formais não tem lugar no espectro da obra dele. > > Porém, a questão da adequação das explicações semânticas pode ser > levantada também no âmbito informal, como tentei indicar na minha > mensagem original. > > Nas suas explicações semânticas, Martin-Löf toma as regras de introdução > como primitivas (como aquelas que conferem significado às constantes > lógicas) e justifica as regras de eliminação com base nelas. Se as > regras de eliminação também fossem consideradas primitivas, ele não > teria porquê se dar o trabalho de justificá-las com base nas regras de > introdução. A questão agora surge: Será que as regras de eliminação > justificadas por Martin-Löf são, de fato, as regras mais fortes que > podem ser justificadas, tomando como base as regras de introdução? Isto > é, seria possível fornecer regras de eliminação mais fortes que também > sejam justificadas com base nas regras de introdução? > > Como se trata de uma semântica (explicação, fundamentação) informal, > esta questão não pode ser respondida, no caso de Martin-Löf, com um > teorema. Mas isso não significa que a questão é inócua ou > desimportante, e, certamente, é uma questão que não pode ser afastada > simplesmente sob o pretexto de que a semântica é informal. Martin-Löf > fornece uma justificação, informal, obviamente, para as suas regras de > eliminação (suas regras de eliminação estão *corretas*). Mas, é > perfeitamente razoável se perguntar se haveriam outras regras de > eliminação que pudessem ser justificadas e que resultariam numa lógica > diferente da lógica intuicionista, que é a lógica alvo da semântica > informal em questão. > > O que, com respeito a Martin-Löf, é um mero questionamento informal, se > torna, no caso de Prawitz, uma conjectura[1], pois Prawitz, ainda que > num estilo similar ao de Martin-Löf, fornece definições rigorosas que > resultam, de fato, numa semântica formal. A conjectura de Prawitz é > justamente uma versão formal da questão que estou discutindo: Seriam as > regras de eliminação padrões as regras mais fortes que podem ser > validadas do ponto de vista das regras de introdução? > > Os resultados que mencionei anteriormente sugerem que a resposta a essa > conjectura possa ser "não". E, como esses resultados negativos incluem > mesmo contraexemplos, é fácil traduzir os contraexemplos na forma de > justificativas informais nos termos de semânticas informais como BHK e > as explicações semânticas de Martin-Löf. De fato, eu já forneci a você, > em conversa privada, uma justificativa informal em termos de BHK de uma > inferência que não é intuicionisticamente derivável. > > Eu entendo a objeção que faz ao meu uso do *termo* "completude" no > contexto de Martin-Löf, mas espero que tenha conseguido deixar claro que > o uso que fiz de "completude" e "correção" naquele contexto se referia à > *adequação* das explicações semânticas de Martin-Löf ao sistema de > regras de inferência dedutivas que conhecemos como lógica intuicionista. > Esta questão da adequação é legítima, não importa o quão informal seja a > sua fundamentação (explicação, semântica). > > Gostaria ainda de deixar claro que estas minhas observações não afetam > em nada a *utilidade* da TIT como teoria matemática e o fato de que suas > propriedades construtivas, concordo com a Valéria nesse ponto, podem ser > razões mais do que suficientes para favorecê-la em detrimento de ZF. > > Referências: > > [1] Dag Prawitz. An Approach to General Proof Theory and a Conjecture > of a Kind of Completeness of Intuitionistic Logic Revisited. In: > Advances in Natural Deduction, 269-279, 2014. > > -- > Hermógenes Oliveira > > -- > Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" > dos Grupos do Google. > Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie > um e-mail para logica-l+unsubscr...@dimap.ufrn.br. > Para postar neste grupo, envie um e-mail para logica-l@dimap.ufrn.br. > Visite este grupo em https://groups.google.com/a/di > map.ufrn.br/group/logica-l/. > Para ver esta discussão na web, acesse https://groups.google.com/a/di > map.ufrn.br/d/msgid/logica-l/874ly0e5sz.fsf%40camelot.oliveira. > -- Valeria de Paiva http://vcvpaiva.github.io/ http://research.nuance.com/author/valeria-de-paiva/ http://www.cs.bham.ac.uk/~vdp/ -- Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos Grupos do Google. Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+unsubscr...@dimap.ufrn.br. Para postar neste grupo, envie um e-mail para logica-l@dimap.ufrn.br. Visite este grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/. Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAESt%3DXvHCoPzwE6i%2BR-bLJwpWBC%3Dxtsymf6SwP8EiRuV1S0png%40mail.gmail.com.
