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. Em quarta-feira, 10 de janeiro de 2018, Diogo Dias < [email protected]> escreveu: > 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 > > -- > 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 [email protected]. > Para postar nesse grupo, envie um e-mail para [email protected]. > 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 > <https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAP9SZ5Sv%3DgXxJ7%3D_h8xwXtpwOrRB0cTmkRxhpYK6N%3Dji3-UfXQ%40mail.gmail.com?utm_medium=email&utm_source=footer> > . > -- 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 [email protected]. Para postar neste grupo, envie um e-mail para [email protected]. 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/CAJGvw-3wNkVKjcKNqApKFtGhF1D3rYhj%3Dx1rcjkjp5JPiL%3D%2Big%40mail.gmail.com.
