Oi Hermógenes, [...] 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.
Retomando um pouco o ponto da Valéria sobre a computação/construtividade: O intuicionismo, concebido como a escola de filosofia da matemática iniciada por Brouwer no começo do século XX, é fundamentado na noção de computação. Isso certamente é pouco claro em Brouwer, não só por suas inclinações ao misticismo, mas talvez principalmente pelo fato de que este iniciou o seu programa quase três décadas (1907, 1912) antes do amadurecimento matemático da noção de algorítimo fornecida pelos trabalhos de Turing e Church em cerca de 1936. Logo a noção de computação na qual Brouwer formulou o seu intuicionismo pode parecer obscura, estranha ou pouco familiar: uma noção primitiva de “construção mental” ou “intuição basal”, rotinas finitas que surgem no curso do tempo. A matemática seria o resultado de tais construções e a lógica apenas um aspecto da matemática. Felizmente, parte dos escritos de Brouwer acerca de sua lógica foi polida e tornada mais precisa com a interpretação BHK e paradigma de proposição como tipos, 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. mas, de todo modo, BHK (que se limita aos conectivos lógicos) é não mais que uma fotografia parcial do intuicionismo tradicional como todo. Acredito que, pela natureza do retrato, é natural que seja incompleto ou insatisfatório (nem mesmo todos “conectivos” são explicados, e.g. o que significa a igualdade?). Já o paradigma de proposição como tipos tem provocado muita confusão e mal-entendidos, levando muita gente a afirmar que intuicionismo nada mais é que meta-matemática [1] [2]. O cerne da questão é que – como recentemente comentei com o Fernando off-list – há duas formas na qual podemos entender a correspondência entre tipos e proposições. A primeira forma é bem óbvia: a sintática. A correspondência sintática entre proposição e tipos diz que os termos de uma teoria correspondem às derivações de uma respectiva teoria lógica. Aqui termos são meras caracterizações das derivações de uma teoria lógica. Isso também é refletido pelo fato de que o juízo de tipicidade, 'N : M', é analítico (no sentido de Martin-Löf [3], i.e. a checagem de tipos é decidível). Este é o caso da correspondência que ocorre na teoria de tipos intensional do Martin-Löf (MLITT) e é também – ao meu ver – a correspondência usada nos argumentos levantados por Rodrigo Freire acerca da circularidade da noção de verdade em Martin-Löf em Janeiro do ano passado. A segunda correspondência, menos conhecida que a primeira, é a endossada por Brouwer e a que interessa ao intuicionista: a semântica. Provas são caracterizações de uma computação passo a passo que realizam a verdade de uma proposição. Provas são termos, mas não termos de qualquer teoria dos tipos definida por regras de inferências: termos de uma teoria que traz embutida a noção de computação. Esta é a correspondência enfatizada pelas explicações de significado (meaning explanations) do Martin-Löf, sobre o qual a sua teoria de tipos extensional (MLETT) [4] é fundamentada, e, portanto, é a que vale na MLETT. O juízo de tipicidade, normalmente escrito 'N ∈ M' na literatura relevante à teoria extensional, é sintético (i.e. indecidível), dado que expressa não uma noção semântica: N é um programa que realiza o problema expresso por M. Ademais, o juízo 'N ∈ M' *deve* ser indecidível porque não há nenhuma maneira em geral de decidir se um programa, quando executado, gera um valor do tipo determinado: tal programa pode não ter nenhum valor. Pelo seu conteúdo computacional inerente, MLETT é frequentemente chamado de “teoria de tipos computacional” na literatura em torno do assistente de prova NuPRL [5], cujo próprio sistema é definido através da semântica fornecida pelas explicações de significado. De todo modo, o propósito desta mensagem certamente não é tentar convencer ninguém, nem retomar discussões passadas, mas apenas buscar ilustrar algumas das muitas razões que fazem com que outros e eu acreditem que o intuicionismo tradicional, concebida como uma escola em filosofia da matemática, apresenta uma posição filosoficamente coerente. Pagamos o preço da noção de computação, erguemos o edifício da matemática. 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. 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. Abraços lógicos, Bruno [1] – Bob Harper. Constructive mathematics is not meta-mathematics. https://existentialtype.wordpress.com/2013/07/10/constructive-mathematics-is-not-meta-mathematics/ [2] – Bob Harper. Extensionality, Intensionality, and Brouwer’s Dictum. https://existentialtype.wordpress.com/2012/08/11/extensionality-intensionality-and-brouwers-dictum/ [3] – Per Martin-Löf. Analytic and Synthetic Judgements in Type Theory. 1994 [4] – Per Martin-Löf. Constructive mathematics and computer programming. 1982 [5] – PRL Group. Implementing Mathematics with The Nuprl Proof Development System. 1985. -- Bruno Bentzen https://sites.google.com/site/bbentzena/ On Thursday, April 6, 2017 at 8:59:18 PM UTC+8, Hermógenes Oliveira wrote: > > Fernando Yamauti <fgya...@gmail.com <javascript:>> 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/5580aee2-3fc9-400c-a98d-984efcb754ad%40dimap.ufrn.br.
