Fernando Yamauti <fgyama...@gmail.com> 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 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/87shllitep.fsf%40camelot.oliveira.
