meus dois centavos nessa discussao (so' pra voces nao ficarem com a impressao de que ninguem le...):
1.>Muitos, porém, acham o preço a se pagar muito salgado: falha da transitividade (monotonicidade, regra de corte). eu acho um preco absurdo. pior do que se tem que pagar por chifre de unicornio! 2.>Neste ponto, a única vantagem de TIT em comparação à ZF (sua concorrente igualmente ad hoc), principalmente se você é um computeiro ou matemático preocupado com computabilidade, é o fato de TIT ser construtiva. well, well, well... "a única vantagem" 'e vantagem a beca, pra alguns, ne', cara-palida? abracos constructivos e MartinLoefianos pra todos, ;) Valeria 2017-04-06 5:59 GMT-07:00 Hermógenes Oliveira < [email protected]>: > Fernando Yamauti <[email protected]> escreveu: > > > [...] > > > > Um outro caso que me incomoda muito e o Martin-Löf sempre joga em > > baixo do tapete: o porquê de " 'A true' infere 'B true' " ser > > correto, onde A é falso (onde o "falso" é clássico, ou seja, existe > > uma prova de \neg A) , para um construtivista. Como se constrói uma > > prova, a partir de uma prova de que o falso é verdadeiro? > > Martin-Löf possui um conceito de "prova hipotética", isto é, em vez de > "prova" no sentido categórico, teríamos uma "prova" sob a assunção de > hipóteses. Nesse caso, se nós temos que "¬A true", isto é, "A→⊥ > true", e também temos "A true", então "B true" se segue por modus > pones e ex contradictione quodlibet (ECQ). Uma primeira questão, > então, seria: > > a) Por que ECQ seria correto de um ponto de vista construtivo? > > Aqui, vale notar que a validade construtiva de ECQ não é uma posição > unânime. Nesse sentido, G. F. C. Griss[1] é um dos dissidentes mais > importantes e interessantes, pois parece argumentar de um ponto de > vista puramente construtivo. Outros construtivistas apresentam > motivações diversas para se rejeitar ECQ, em especial, motivações > relacionadas à relevância e ao uso da implicação na linguagem > cotidiana (por exemplo, Johansson[2] e Tennant[3]). > > Eu, pessoalmente, acho ECQ um princípio *muito* suspeito. O difícil é > que, sem ECQ, um construtivista ficaria basicamente sem negação (ao > estilo do cálculo mínimo de Johansson), ou a negação cessaria de ser um > operador *lógico*. Uma exceção interessante é o caso da "Core Logic" de > Tennant, onde a negação é dada um caráter lógico, mesmo sem ECQ, pela > admissão de modus tollendo ponens (ou silogismo disjuntivo) e uma regra > especial para a implicação que permite obter ¬A,A⊢B. Muitos, porém, > acham o preço a se pagar muito salgado: falha da transitividade > (monotonicidade, regra de corte). > > De qualquer maneira, talvez ECQ possa ser fundamentado de um ponto de > vista construtivo. Contudo, as fundamentações (explicações) > oferecidas até o momento, por Martin-Löf e outros, também me parecem > insatisfatórias. > > b) Um outro problema é que Martin-Löf explica (reduz) o conceito de > "prova hipotética" ao conceito de "prova categórica" (sem hipóteses > abertas). > > Isto significa que a correção de uma prova hipotética (dedução) é > predicada na possibilidade de se transformar provas categóricas das > hipóteses em provas categóricas da conclusão, isto é, na construção de > provas categóricas da conclusão com base em provas categóricas das > hipóteses. Portanto, em última instância, a justificativa de > inferências como "¬A (A→⊥) true","A true" / "B true" apelam a provas > categóricas de "¬A true" e "A true" e daí, por modus ponens, a provas > categóricas do absurdo! Estas provas categóricas não precisam ser > provas reais, mas devem, pelo menos, ser concebíveis, se é que a > explicação de Martin-Löf faz qualquer sentido. Caberia a Martin-Löf, > e demais construtivistas que defendem posições similares, explicar o > que significa conceber provas categóricas do absurdo, em outras > palavras, o que significa conceber o impossível. > > Alguns meses atrás, conversava com Bruno Bentzen a respeito de uma > anedota sobre o tema. Segundo a anedota, alguém teria perguntado a > Martin-Löf, ou Prawitz, não me lembro qual, como seria possível > conceber uma construção que transformasse provas do absurdo em provas > de outra sentença, dado que não há provas do absurdo. Ele teria > respondido: "Como se transforma um unicórnio num cavalo? Cortando > fora o chifre. Mas não há unicórnios." A anedota é divertida, e > ilustra como podemos tratar de construções que talvez nunca poderão > ser efetuadas (seja porque não existem unicórnios ou porque não > existem provas do absurdo). Porém, a inexistência de unicórnios > parece estar num patamar diferente (contingente) comparado com a > inexistência de provas do absurdo. > > A concepção de raciocínios hipotéticos defendida por Martin-Löf, e > compartilhada por Prawitz e muitos outros, é tributária de BHK, > especialmente a cláusula para implicação. Esta concepção também > recebe o nome de "primazia do categórico sobre o hipotético" ou > "concepção das hipóteses como variáveis" (a serem saturadas por provas > categóricas)[4]. Ela parece estar por trás de alguns resultados > negativos[5][6] publicados nos últimos anos com respeito a > fundamentações apoiadas nas regras de introdução, ou nas cláusulas BHK > concebidas como regras de introdução. Estes resultados mostram que, > sob certas condições, tais fundamentações fracassam em capturar > exatamente os raciocínios intuicionisticamente deriváveis. > > Martin-Löf, no artigo de fundamentação filosófica da sua Teoria dos > Tipos[7], assume que as regras de introdução dão o significado das > constantes lógicas e, a partir daí, justifica as regras de eliminação. > Isto demonstra, em terminologia corrente, a correção da lógica > intuicionista (como sistema formal) com respeito a uma fundamentação > baseada nas introduções (estilo BHK). Contudo, a contrapartida (a > questão se todos os princípios de raciocínio justificáveis são de fato > deriváveis intuicionisticamente), isto é, completude, em terminologia > corrente, permanece em aberto no artigo, pois Martin-Löf não oferece > nenhum argumento em seu favor. Os resultados mencionados > anteriormente mostram que, sob certas condições que parecem razoáveis > de um ponto de vista construtivo, uma fundamentação estilo BHK, quando > formulada precisamente (uma vez que BHK é uma espécia de fundamentação > (semântica) informal), justificaria inferências que não são > intuicionisticamente deriváveis. > > Me parece que em ambos os quesitos, a) e b), a posição construtivista > de vertente intuicionista, conforme tradicionalmente concebida, deixa > muito a desejar. Confesso que, às vezes, me pergunto se o > intuicionismo tradicional, como exemplificado pela tradição BHK, seria > mesmo uma posição filosoficamente coerente. > > > [...] > > > > Ou ainda, outro problema que leva ao regresso infinito e a > > identificação de um objeto do conhecimento com o conhecimento desse > > objeto (que o Rodrigo havia comentado a um tempo atras de maneira > > diferente). Um juízo do tipo 'A true' pode virar uma proposição onde > > '(A true) true' se torna um juízo. E, mais. No ponto de vista > > epistemico, essas duas coisas são equivalentes (saber que vc sabe é > > igual a saber). Acho que o ponto de vista epistemico não bate com a > > teoria, já que garantir que o tipo "A é habitado" não é equivalente > > a A (em um dado universo), ou será que é? Ou seja, a justificativa > > do ML não é adequada e só a teoria funciona. > > Na minha opinião, o potencial explanatório e de fundamentação da > Teoria Intuicionista de Tipos (TIT) se estraçalha a partir do momento > que se introduz universos. A partir daí, me parece, a TIT assume um > caráter fortemente ad hoc e muitas da intuições iniciais vão para o > espaço. Neste ponto, a única vantagem de TIT em comparação à ZF (sua > concorrente igualmente ad hoc), principalmente se você é um computeiro > ou matemático preocupado com computabilidade, é o fato de TIT ser > construtiva. Por outro lado, os argumentos de que ZF seria > filosoficamente mais robusta e conceitualmente mais coerente (ver, por > exemplo, Harvey Friedman na FOM) não me convencem. Acontece que, dado > que ZF é a doutrina ortodoxa, estamos acostumados a fazer vista grossa > para as aberrações em ZF e maldizer excessivamente qualquer > idiossincrasia de propostas alternativas, como TIT. > > De qualquer maneira, mesmo num contexto muito elementar, abordar o > intuicionismo, ou construtivismo, de um ponto de vista epistemológico, > tal como Martin-Löf faz, me parece um equívoco. Concordo ainda que a > discussão epistemológica de Martin-Löf em conexão com a fundamentação > da sua Teoria de Tipos é muito confusa, para se dizer o mínimo. > > A epistemologia, contudo, não é a única rota para o intuicionismo, e > sequer me parece a melhor. No âmbito puramente lógico, uma rota mais > interessante rumo ao intuicionismo passa pela filosofia da linguagem, > em particular, por um certo pragmatismo linguístico. Neste sentido, > princípios lógicos estariam apoiados em práticas linguísticas regradas > (ver trabalho recente do Marcos Silva). Esse tipo de inferencialismo > lógico ainda é muito incipiente, é verdade, mas me parece muito > promissor. > > Saudações, > > Referências: > > [1] Arend Heyting. G. F. C. Griss and his negationsless > intuitionistic mathematics. Synthese 9 (1):91-96, 1955. > (ver referências nesse artigo para os escritos de Griss) > > [2] Ingebrigt Johansson. Der Minimalkalkül, ein reduzierter > intuitionistischer Formalismus. Compositio Mathematica 4, 119-136, > 1937. > > [3] Neil Tennant. The Taming of the True. Clarendon Press, 1997. > (ver também artigos no RSL sobre "Core Logic") > > [4] Peter Schroeder-Heister. The Categorical and the Hypothetical: A > critique of some fundamental assumptions of standard > semantics. Synthese 187 (3), 925-942, 2012. > > [5] Wagner de Campos Sanz, Thomas Piecha and Peter > Schroeder-Heister. Constructive Semantics, Admissibility of Rules and > the Validity of Peirce's Law. Logic Journal of the IGPL 22 (2), > 297-308, 2014. > > [6] Thomas Piecha, Wagner de Campos Sanz and Peter > Schroeder-Heister. Failure of Completeness in Proof-Theoretic > Semantics. Journal of Philosophical Logic 44 (3), 321-335, 2015. > > [7] Per Martin-L\"of. On the Meanings of the Logical Constants and the > Justifications of the Logical Laws. Nordic Journal of Philosophical > Logic 1 (1), 11-60, 1996. > > -- > 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 [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/87shllitep.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 [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/CAESt%3DXu6tY1XNsdCW%3Dr%3DBtVfsg6M9zaBvNwcGv5L16Esy_F%3D1g%40mail.gmail.com.
