Dúvidas sobre Dummett
21 views
Skip to first unread message
Diogo Dias
Jan 10, 2018, 9:57:32 AM1/10/18
to Lista Lógica
Olá!
Eu estou estudando Dummett e sua teoria do significado. Em diversas ocasiões, ele defende a necessidade de distinguir entre prova e prova canônica, sendo que a última seria responsável por determinado o significado dos conectivos lógicos. Não obstante, não há uma definição precisa de prova canônica, e ele próprio reconhece isso. Gostaria de saber se alguém tem indicações de textos em que essa noção é definida com precisão. Em particular, estou investigando se, e como, é possível gerar lógicas diferentes a partir de formalizações diferentes da noção de prova canônica.
Obrigado e abraços!
Diogo Dias
Gabriel Barreto
Jan 10, 2018, 5:44:28 PM1/10/18
to LOGICA-L
Olá,
As provas canonicas são as provas que não são "roundabout"; i.e., provas que são diretas e que não podem ser reduzidas. Se não me engano, são as provas onde regras de introdução e eliminação consecutivas são eliminadas.
Por exemplo, se temos provas para A->B e A da forma
[A]
...
--------(-> int) ...
A->B A
------------------------(-> elim)
B
temos uma nova prova de B que é indireta e poderia ser reduzida tomando a prova de A->B e substituindo lugares onde foi usado a hipótese [A] pela proposição A e sua prova.
A normalização da prova é esse procedimento de reduzir a prova para sua forma canonica. Isto está ligado com a redução dos termos do cálculo lambda de tipos à sua forma
normal (leia sobre a realizabilidade modificada de Kreisel)
As provas canonicas são as provas que não são "roundabout"; i.e., provas que são diretas e que não podem ser reduzidas. Se não me engano, são as provas onde regras de introdução e eliminação consecutivas são eliminadas.
Por exemplo, se temos provas para A->B e A da forma
[A]
...
--------(-> int) ...
A->B A
------------------------(-> elim)
B
temos uma nova prova de B que é indireta e poderia ser reduzida tomando a prova de A->B e substituindo lugares onde foi usado a hipótese [A] pela proposição A e sua prova.
A normalização da prova é esse procedimento de reduzir a prova para sua forma canonica. Isto está ligado com a redução dos termos do cálculo lambda de tipos à sua forma
normal (leia sobre a realizabilidade modificada de Kreisel)
Hermógenes Oliveira
Jan 11, 2018, 4:55:50 AM1/11/18
to logi...@dimap.ufrn.br
Diogo Dias <diogo.bi...@gmail.com> escreveu:
> Olá!
Olá, Diogo.
> Eu estou estudando Dummett e sua teoria do significado. Em diversas
> ocasiões, ele defende a necessidade de distinguir entre prova e
> prova canônica, sendo que a última seria responsável por determinado
> o significado dos conectivos lógicos. Não obstante, não há uma
> definição precisa de prova canônica, e ele próprio reconhece
> isso. Gostaria de saber se alguém tem indicações de textos em que
> essa noção é definida com precisão.
Dummett oferece uma definição precisa de argumento canônico em _The
Logical Basis of Metaphysics_, em particular os capítulos 11 ao 13
(infelizmente, desconheço traduções deste livro para o português ou
espanhol).
Definições alternativas podem ser encontradas em diversos artigos de
Prawitz, Martin-Löf, Schroeder-Heister, Göran Sundholm, Tor Sandqvist
e outros. Contudo, dependendo do caso, essas definições podem se
distanciar bastante da perspectiva de Dummett.
> Em particular, estou investigando se, e como, é possível gerar
> lógicas diferentes a partir de formalizações diferentes da noção de
> prova canônica.
Dummett oferece duas definições distintas de validade lógica: uma com
base nas regras de introdução, e outra com base nas regras de
eliminação. As definições não pressupõe nenhuma lógica específica de
antemão e poderiam, *em princípio*, ser aplicadas a qualquer lógica
bem-comportada (normalização, propriedade da subfórmula). Por
exemplo, as definições com base nas regras de eliminação podem ser
levemente adaptadas de modo a obter lógicas subestruturais, como a
lógica relevante.
Eu estou trabalhando com isso no momento e, se você quiser, podemos
discutir os detalhes em privado (para não incomodar a lista).
--
Hermógenes Oliveira
> Olá!
Olá, Diogo.
> Eu estou estudando Dummett e sua teoria do significado. Em diversas
> ocasiões, ele defende a necessidade de distinguir entre prova e
> prova canônica, sendo que a última seria responsável por determinado
> o significado dos conectivos lógicos. Não obstante, não há uma
> definição precisa de prova canônica, e ele próprio reconhece
> isso. Gostaria de saber se alguém tem indicações de textos em que
> essa noção é definida com precisão.
Logical Basis of Metaphysics_, em particular os capítulos 11 ao 13
(infelizmente, desconheço traduções deste livro para o português ou
espanhol).
Definições alternativas podem ser encontradas em diversos artigos de
Prawitz, Martin-Löf, Schroeder-Heister, Göran Sundholm, Tor Sandqvist
e outros. Contudo, dependendo do caso, essas definições podem se
distanciar bastante da perspectiva de Dummett.
> Em particular, estou investigando se, e como, é possível gerar
> lógicas diferentes a partir de formalizações diferentes da noção de
> prova canônica.
base nas regras de introdução, e outra com base nas regras de
eliminação. As definições não pressupõe nenhuma lógica específica de
antemão e poderiam, *em princípio*, ser aplicadas a qualquer lógica
bem-comportada (normalização, propriedade da subfórmula). Por
exemplo, as definições com base nas regras de eliminação podem ser
levemente adaptadas de modo a obter lógicas subestruturais, como a
lógica relevante.
Eu estou trabalhando com isso no momento e, se você quiser, podemos
discutir os detalhes em privado (para não incomodar a lista).
--
Hermógenes Oliveira
Diogo Dias
Jan 11, 2018, 10:44:09 AM1/11/18
to Lista Lógica
Olá, Hermógenes.
Obrigado pela resposta. Quando disse que Dummett não apresenta uma definição precisa de prova canônica, estava pensando nas seguintes citações:
"What exaclty the notion of a canonical proof amounts to is obscure" (The Philosophical Basis of Intuitionistic Logic, p. 241), e "no one can at present give a detailed account of canonical proofs even of statements of first order arithmetic." (Elements of Intuitionism, p. 400)
Obrigado pela indicação do Logical Basis of Metaphysics. Acabei de ler os capítulos que você mencionou e, de fato, ali ele apresenta uma definição precisa dessa noção. Li, também, o texto Meaning approached via proofs, do Prawitz, em que ele apresenta outro possível tratamento de prova canônica, e compara com o do Dummett.
Meu interesse no tema é o seguinte: Eu estou atualmente estudando pluralismo lógico, e estou investigando se alguns argumentos que, a princípio, foram propostos como uma defesa de um tipo de monismo lógico, podem ser interpretados como dando margem à legitimidade de lógicas distintas. No caso do Dummett, me parece que, variando o tratamento da noção de prova canônica, mas respeitando as restrições gerais da sua proposta (normalização, harmonia, molecularidade da linguagem etc), é possível gerar lógicas distintas.
Você poderia me indicar alguns artigos desses autores que você mencionou que fazem isso? Em particular, fiquei interessado na possibilidade de obter uma lógica relevante mantendo o framework do Dummett.
Abraços,
Diogo
--
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/20180111105547.Horde.u3Xq_olxYd4hCleCkbl45C8%40webmail.uni-tuebingen.de.
Hermógenes Oliveira
Jan 11, 2018, 3:18:45 PM1/11/18
to logi...@dimap.ufrn.br
Diogo Dias <diogo.bi...@gmail.com> escreveu:
> Quando disse que Dummett não apresenta uma definição precisa de prova
> canônica, estava pensando nas seguintes citações:
>
> "What exaclty the notion of a canonical proof amounts to is obscure"
> (The Philosophical Basis of Intuitionistic Logic, p. 241), e "no one
> can at present give a detailed account of canonical proofs even of
> statements of first order arithmetic." (Elements of Intuitionism,
> p. 400)
Ao que me parece, Dummett tinha em mente nessas citações um contexto
mais amplo do que o da lógica pura: o contexto da aritmética ou mesmo da
matemática em geral (análise e etc.). Isso está inclusive explícito no
caso da segunda citação.
Enquanto a tese da canonicidade parece bastante natural e plausível no
âmbito da lógica pura, a coisa complica quando passamos para a
aritimética de primeira ordem ou teorias matemáticas mais complexas.
Problemas similares aparecem quando tentamos aplicar a tese da
canonicidade à teorias empíricas. O próprio Dummett chega a discutir
vários problemas com a tese da canonicidade (ali tratada como "hipótese
fundamental") em contextos extra-lógicos, tanto empíricos quanto
matemáticos, no capítulo 12 do "The Logical Basis of Metaphysics".
> Obrigado pela indicação do Logical Basis of Metaphysics. Acabei de ler
> os capítulos que você mencionou e, de fato, ali ele apresenta uma
> definição precisa dessa noção. Li, também, o texto Meaning approached
> via proofs, do Prawitz, em que ele apresenta outro possível tratamento
> de prova canônica, e compara com o do Dummett.
>
> Meu interesse no tema é o seguinte: Eu estou atualmente estudando
> pluralismo lógico, e estou investigando se alguns argumentos que, a
> princípio, foram propostos como uma defesa de um tipo de monismo
> lógico, podem ser interpretados como dando margem à legitimidade de
> lógicas distintas. No caso do Dummett, me parece que, variando o
> tratamento da noção de prova canônica, mas respeitando as restrições
> gerais da sua proposta (normalização, harmonia, molecularidade da
> linguagem etc), é possível gerar lógicas distintas.
>
> Você poderia me indicar alguns artigos desses autores que você
> mencionou que fazem isso? Em particular, fiquei interessado na
> possibilidade de obter uma lógica relevante mantendo o framework do
> Dummett.
Quanto à semântica Dummettiana para lógica relevante e outras lógicas
subestruturais, me referia a um trabalho preliminar meu e de dois
co-autores, Mattia Petrolo e Eugenio Orlandelli. Nosso impulso é, em
linhas gerais, exatamente a que você descreveu acima: trazer uma
perspectiva pluralista para o monismo característico do inferencialismo
semântico da tradição Prawitz-Dummett. Nós apresentamos nosso trabalho
em alguns congressos, mas ainda não temos nada publicado. Infelizmente,
não conheço nenhuma pesquisa nessa linha além da nossa, portanto não
tenho muito o que indicar.
No que concerne o nosso trabalho, a ideia é bastante simples. Grosso
modo, basta observar que a noção de argumento canônico de Dummett
trabalha com argumentos hipotéticos (com hipóteses abertas), em vez de
provas fechadas. Uma vez que as hipóteses são incorporadas de modo
essencial na abordagem, podemos refinar o tratamento das hipóteses de
modo a obter lógicas subestruturais.
Por exemplo, nas defininições baseadas nas regras de eliminação,
argumentos válidos são predicados, grosso modo, na possibilidade de
transformar certos argumentos canônicos em outros argumentos canônicos
que dependem, *no máximo*, das mesmas hipóteses. Se, em vez disso,
exigirmos que os argumentos canônicos resultantes dependam *exatamente
do mesmo conjunto de hipóteses*, temos uma lógica relevante (sem a lei
de distribuição) similar àquela de Prawitz (1965, Cap. VII). Se, além
disso, coletamos as hipóteses em multiconjuntos, em vez de conjuntos,
temos um fragmento da lógica linear intuicionista (sem exponenciais). E
por aí vai.
--
Hermógenes Oliveira
> Quando disse que Dummett não apresenta uma definição precisa de prova
> canônica, estava pensando nas seguintes citações:
>
> "What exaclty the notion of a canonical proof amounts to is obscure"
> (The Philosophical Basis of Intuitionistic Logic, p. 241), e "no one
> can at present give a detailed account of canonical proofs even of
> statements of first order arithmetic." (Elements of Intuitionism,
> p. 400)
mais amplo do que o da lógica pura: o contexto da aritmética ou mesmo da
matemática em geral (análise e etc.). Isso está inclusive explícito no
caso da segunda citação.
Enquanto a tese da canonicidade parece bastante natural e plausível no
âmbito da lógica pura, a coisa complica quando passamos para a
aritimética de primeira ordem ou teorias matemáticas mais complexas.
Problemas similares aparecem quando tentamos aplicar a tese da
canonicidade à teorias empíricas. O próprio Dummett chega a discutir
vários problemas com a tese da canonicidade (ali tratada como "hipótese
fundamental") em contextos extra-lógicos, tanto empíricos quanto
matemáticos, no capítulo 12 do "The Logical Basis of Metaphysics".
> Obrigado pela indicação do Logical Basis of Metaphysics. Acabei de ler
> os capítulos que você mencionou e, de fato, ali ele apresenta uma
> definição precisa dessa noção. Li, também, o texto Meaning approached
> via proofs, do Prawitz, em que ele apresenta outro possível tratamento
> de prova canônica, e compara com o do Dummett.
>
> Meu interesse no tema é o seguinte: Eu estou atualmente estudando
> pluralismo lógico, e estou investigando se alguns argumentos que, a
> princípio, foram propostos como uma defesa de um tipo de monismo
> lógico, podem ser interpretados como dando margem à legitimidade de
> lógicas distintas. No caso do Dummett, me parece que, variando o
> tratamento da noção de prova canônica, mas respeitando as restrições
> gerais da sua proposta (normalização, harmonia, molecularidade da
> linguagem etc), é possível gerar lógicas distintas.
>
> Você poderia me indicar alguns artigos desses autores que você
> mencionou que fazem isso? Em particular, fiquei interessado na
> possibilidade de obter uma lógica relevante mantendo o framework do
> Dummett.
subestruturais, me referia a um trabalho preliminar meu e de dois
co-autores, Mattia Petrolo e Eugenio Orlandelli. Nosso impulso é, em
linhas gerais, exatamente a que você descreveu acima: trazer uma
perspectiva pluralista para o monismo característico do inferencialismo
semântico da tradição Prawitz-Dummett. Nós apresentamos nosso trabalho
em alguns congressos, mas ainda não temos nada publicado. Infelizmente,
não conheço nenhuma pesquisa nessa linha além da nossa, portanto não
tenho muito o que indicar.
No que concerne o nosso trabalho, a ideia é bastante simples. Grosso
modo, basta observar que a noção de argumento canônico de Dummett
trabalha com argumentos hipotéticos (com hipóteses abertas), em vez de
provas fechadas. Uma vez que as hipóteses são incorporadas de modo
essencial na abordagem, podemos refinar o tratamento das hipóteses de
modo a obter lógicas subestruturais.
Por exemplo, nas defininições baseadas nas regras de eliminação,
argumentos válidos são predicados, grosso modo, na possibilidade de
transformar certos argumentos canônicos em outros argumentos canônicos
que dependem, *no máximo*, das mesmas hipóteses. Se, em vez disso,
exigirmos que os argumentos canônicos resultantes dependam *exatamente
do mesmo conjunto de hipóteses*, temos uma lógica relevante (sem a lei
de distribuição) similar àquela de Prawitz (1965, Cap. VII). Se, além
disso, coletamos as hipóteses em multiconjuntos, em vez de conjuntos,
temos um fragmento da lógica linear intuicionista (sem exponenciais). E
por aí vai.
--
Hermógenes Oliveira
Fernando Yamauti
Jan 12, 2018, 1:35:04 PM1/12/18
to logi...@dimap.ufrn.br
Uma prova canônica é uma prova direta ou imediata. Mais precisamente, uma prova canônica é qualquer termo dado por uma única aplicação de uma unica regra de introdução à qualquer termos, canônicos ou não. Essa definição difere da noção de forma canonica (termos dados somente por regras de introdução), apesar de ser relacionada. Portanto mudar o que é uma prova canônica, muda quais são as regras de introdução da teoria dos tipos por trás da sua lógica, logo tal modificação pode ou não gerar uma lógica equivalente dependendo da noção de equivalência que voce quer usar. Dê uma olhada em http://archive-pml.github.io/martin-lof/pdfs/Truth-of-a-Proposition-Evidence-of-a-Judgment-1987.pdf . Na pagina 412 ele fala do Dummet.
A propósito, eu discordo dessa noção de prova canônica, já que acho que a verdade de uma proposição e , portanto, seu significado é completamente determinada pelos termos canônicos, ie, na forma canônica. Isso bate com a nocao de verdade na teoria dos tipos computacional e com as varias definicoes de realização. Mas isso depende do que significa verdade no contexto do intuicionismo e provavelmente sai do escopo da discussão.
--
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/CAP9SZ5Sv%3DgXxJ7%3D_h8xwXtpwOrRB0cTmkRxhpYK6N%3Dji3-UfXQ%40mail.gmail.com.
Reply all
Reply to author
Forward
0 new messages