Construtivismo (filosofia da matemática) - Constructivism (philosophy of mathematics)

Na filosofia da matemática , o construtivismo afirma que é necessário encontrar (ou "construir") um exemplo específico de um objeto matemático para provar que um exemplo existe. Em contraste, na matemática clássica , pode-se provar a existência de um objeto matemático sem "encontrar" esse objeto explicitamente, assumindo sua inexistência e, em seguida, derivando uma contradição dessa suposição. Tal prova por contradição pode ser chamada de não construtiva, e um construtivista pode rejeitá-la. O ponto de vista construtivo envolve uma interpretação verificacional do quantificador existencial , o que está em desacordo com sua interpretação clássica.

Existem muitas formas de construtivismo. Isso inclui o programa de intuicionismo fundado por Brouwer , o finitismo de Hilbert e Bernays , a matemática recursiva construtiva de Shanin e Markov e o programa de análise construtiva de Bishop . O construtivismo também inclui o estudo de teorias de conjuntos construtivos , como CZF e o estudo da teoria do topos .

O construtivismo é frequentemente identificado com o intuicionismo, embora o intuicionismo seja apenas um programa construtivista. O intuicionismo afirma que os fundamentos da matemática estão na intuição individual do matemático, tornando a matemática uma atividade intrinsecamente subjetiva. Outras formas de construtivismo não se baseiam neste ponto de vista da intuição e são compatíveis com um ponto de vista objetivo sobre a matemática.

Matemática construtiva

Grande parte da matemática construtiva usa a lógica intuicionista , que é essencialmente lógica clássica sem a lei do terceiro excluído . Essa lei afirma que, para qualquer proposição, ou essa proposição é verdadeira ou sua negação é. Isso não quer dizer que a lei do terceiro excluído seja totalmente negada; casos especiais da lei serão prováveis. Acontece que a lei geral não é assumida como um axioma . A lei da não contradição (que afirma que as afirmações contraditórias não podem ser ambas ao mesmo tempo verdadeiras) ainda é válida.

Por exemplo, na aritmética de Heyting , pode-se provar que para qualquer proposição p que não contenha quantificadores , é um teorema (onde x , y , z ... são as variáveis ​​livres na proposição p ). Nesse sentido, proposições restritas ao finito ainda são consideradas verdadeiras ou falsas, como o são na matemática clássica, mas essa bivalência não se estende a proposições que se referem a coleções infinitas .

Na verdade, LEJ Brouwer , fundador da escola intuicionista, via a lei do terceiro excluído como abstraída da experiência finita e então aplicada ao infinito sem justificativa . Por exemplo, a conjectura de Goldbach é a afirmação de que todo número par (maior que 2) é a soma de dois números primos . É possível testar qualquer número par particular se é ou não a soma de dois primos (por exemplo, por pesquisa exaustiva), então qualquer um deles é a soma de dois primos ou não. E até agora, cada um assim testado foi, na verdade, a soma de dois primos.

Mas não há nenhuma prova conhecida de que todos eles são assim, nem qualquer prova conhecida de que nem todos são assim. Assim, para Brouwer, não temos justificativa para afirmar "ou a conjectura de Goldbach é verdadeira ou não". E embora a conjectura possa um dia ser resolvida, o argumento se aplica a problemas semelhantes não resolvidos; para Brouwer, a lei do terceiro excluído era equivalente a supor que todo problema matemático tem uma solução.

Com a omissão da lei do terceiro excluído como um axioma, o sistema lógico remanescente tem uma propriedade de existência que a lógica clássica não tem: sempre que for provado construtivamente, então de fato é provado construtivamente para (pelo menos) um particular , freqüentemente chamado Uma testemunha. Assim, a prova da existência de um objeto matemático está ligada à possibilidade de sua construção.

Exemplo de análise real

Na análise real clássica , uma maneira de definir um número real é como uma classe de equivalência de sequências de Cauchy de números racionais .

Na matemática construtiva, uma maneira de construir um número real é como uma função ƒ que recebe um inteiro positivo e produz um ƒ ( n ) racional , junto com uma função g que recebe um inteiro positivo n e produz um inteiro positivo g ( n ) de tal modo que

de modo que à medida que n aumenta, os valores de ƒ ( n ) ficam cada vez mais próximos. Podemos usar ƒ e g juntos para calcular o mais próximo a aproximação racional como gostamos do número real que representam.

Sob esta definição, uma representação simples do número real e é:

Esta definição corresponde à definição clássica usando sequências de Cauchy, exceto com um toque construtivo: para uma sequência de Cauchy clássica, é necessário que, para qualquer distância dada, exista (no sentido clássico) um membro na sequência após a qual todos os membros estão mais próximos do que a distância. Na versão construtiva, é necessário que, para qualquer distância dada, seja realmente possível especificar um ponto na sequência onde isso acontece (esta especificação necessária é freqüentemente chamada de módulo de convergência ). Na verdade, a interpretação construtiva padrão da declaração matemática

é precisamente a existência da função que calcula o módulo de convergência. Assim, a diferença entre as duas definições de números reais pode ser considerada como a diferença na interpretação da afirmação "para todos ... existe ..."

Isso então abre a questão sobre que tipo de função de um conjunto contável para um conjunto contável, como f e g acima, pode realmente ser construída. Diferentes versões de construtivismo divergem neste ponto. As construções podem ser definidas de forma ampla como sequências de livre escolha , que é a visão intuicionista, ou de forma restrita como algoritmos (ou mais tecnicamente, as funções computáveis ), ou mesmo deixadas sem especificação. Se, por exemplo, a visão algorítmica é considerada, então os reais conforme construídos aqui são essencialmente o que classicamente seria chamado de números computáveis .

Cardinalidade

Tomar a interpretação algorítmica acima pareceria em desacordo com as noções clássicas de cardinalidade . Enumerando algoritmos, podemos mostrar classicamente que os números computáveis são contáveis. No entanto, o argumento diagonal de Cantor mostra que os números reais têm cardinalidade mais alta. Além disso, o argumento diagonal parece perfeitamente construtivo. Identificar os números reais com os números computáveis ​​seria uma contradição.

E, de fato, o argumento diagonal de Cantor é construtivo, no sentido de que dada uma bijeção entre os números reais e os números naturais, constrói-se um número real que não se encaixa e, portanto, prova uma contradição. Podemos, de fato, enumerar algoritmos para construir uma função T , sobre a qual inicialmente assumimos que é uma função dos números naturais para os reais. Mas, para cada algoritmo, pode ou não corresponder um número real, já que o algoritmo pode falhar em satisfazer as restrições, ou mesmo ser não-terminante ( T é uma função parcial ), então isso falha em produzir a bijeção necessária. Em suma, quem tem a visão de que os números reais são (individualmente) efetivamente computáveis ​​interpreta o resultado de Cantor como mostrando que os números reais (coletivamente) não são recursivamente enumeráveis .

Ainda assim, pode-se esperar que, como T é uma função parcial dos números naturais para os números reais, portanto os números reais não são mais do que contáveis. E, uma vez que todo número natural pode ser representado trivialmente como um número real, portanto, os números reais não são menos do que contáveis. Eles são, portanto, exatamente contáveis. No entanto, esse raciocínio não é construtivo, pois ainda não constrói a bijeção necessária. O teorema clássico que prova a existência de uma bijeção em tais circunstâncias, ou seja, o teorema de Cantor-Bernstein-Schroeder , não é construtivo. Recentemente, foi demonstrado que o teorema de Cantor-Bernstein-Schroeder implica a lei do terceiro excluído , portanto, não pode haver prova construtiva do teorema.

Axioma de escolha

O status do axioma da escolha em matemática construtiva é complicado pelas diferentes abordagens de diferentes programas construtivistas. Um significado trivial de "construtivo", usado informalmente por matemáticos, é "demonstrável na teoria dos conjuntos ZF sem o axioma da escolha." No entanto, os proponentes de formas mais limitadas de matemática construtiva afirmariam que o próprio ZF não é um sistema construtivo.

Nas teorias intuicionistas da teoria dos tipos (especialmente na aritmética de tipo superior), muitas formas do axioma da escolha são permitidas. Por exemplo, o axioma AC 11 pode ser parafraseado para dizer que para qualquer relação R no conjunto de números reais, se você provou que para cada número real x existe um número real y tal que R ( x , y ) é válido, então, há na verdade uma função F tal que R ( x , F ( x )) vale para todos os números reais. Princípios de escolha semelhantes são aceitos para todos os tipos finitos. A motivação para aceitar esses princípios aparentemente não construtivos é a compreensão intuicionista da prova de que "para cada número real x há um número real y tal que R ( x , y ) é válido". De acordo com a interpretação de BHK , esta prova em si é essencialmente a função F desejada. Os princípios de escolha que os intuicionistas aceitam não implicam na lei do terceiro excluído .

No entanto, em certos sistemas de axiomas para a teoria dos conjuntos construtivos, o axioma da escolha implica a lei do meio excluído (na presença de outros axiomas), como mostrado pelo teorema de Diaconescu-Goodman-Myhill . Algumas teorias de conjuntos construtivas incluem formas mais fracas do axioma da escolha, como o axioma da escolha dependente na teoria dos conjuntos de Myhill.

Teoria da medida

A teoria clássica da medida é fundamentalmente não construtiva, uma vez que a definição clássica de medida de Lebesgue não descreve nenhuma maneira de calcular a medida de um conjunto ou a integral de uma função. Na verdade, se alguém pensa em uma função apenas como uma regra que "entra com um número real e produz um número real", então não pode haver nenhum algoritmo para calcular a integral de uma função, uma vez que qualquer algoritmo só seria capaz de chamar um número finito valores da função por vez, e muitos valores finitos não são suficientes para calcular a integral para qualquer precisão não trivial. A solução para esse enigma, apresentada pela primeira vez no livro de Bishop de 1967, é considerar apenas funções que são escritas como o limite pontual de funções contínuas (com módulo de continuidade conhecido), com informações sobre a taxa de convergência. Uma vantagem de construir a teoria da medida é que se alguém pode provar que um conjunto é construtivamente de medida completa, então existe um algoritmo para encontrar um ponto naquele conjunto (novamente, ver o livro de Bishop). Por exemplo, esta abordagem pode ser usada para construir um número real que seja normal para todas as bases.

O lugar do construtivismo na matemática

Tradicionalmente, alguns matemáticos suspeitam, se não antagônicos, do construtivismo matemático, em grande parte por causa das limitações que eles acreditam que ele representa para a análise construtiva. Essas opiniões foram expressas com força por David Hilbert em 1928, quando ele escreveu em Grundlagen der Mathematik , "Tomar o princípio do meio excluído do matemático seria o mesmo, digamos, que prescrever o telescópio ao astrônomo ou ao boxeador o uso de seus punhos ".

Errett Bishop , em sua obra Foundations of Constructive Analysis , de 1967 , trabalhou para dissipar esses temores desenvolvendo uma grande quantidade de análises tradicionais em uma estrutura construtiva.

Embora a maioria dos matemáticos não aceite a tese do construtivista de que apenas a matemática feita com base em métodos construtivos é válida, os métodos construtivos são cada vez mais interessantes por motivos não ideológicos. Por exemplo, provas construtivas em análise podem garantir a extração de testemunhas , de tal forma que trabalhar dentro das restrições dos métodos construtivos pode tornar mais fácil encontrar testemunhas para teorias do que usar métodos clássicos. Aplicações para matemática construtiva também foram encontradas em cálculos lambda digitados , teoria de topos e lógica categórica , que são assuntos notáveis ​​em matemática fundamental e ciência da computação . Na álgebra, para entidades como topoi e álgebras de Hopf , a estrutura suporta uma linguagem interna que é uma teoria construtiva; trabalhar dentro das restrições dessa linguagem é frequentemente mais intuitivo e flexível do que trabalhar externamente por meios como raciocinar sobre o conjunto de álgebras concretas possíveis e seus homomorfismos .

O físico Lee Smolin escreve em Three Roads to Quantum Gravity que a teoria do topos é "a forma certa de lógica para a cosmologia" (página 30) e "Em suas primeiras formas era chamada de 'lógica intuicionista'" (página 31). "Nesse tipo de lógica, as afirmações que um observador pode fazer sobre o universo são divididas em pelo menos três grupos: aquelas que podemos julgar verdadeiras, aquelas que podemos julgar falsas e aquelas cuja verdade não podemos decidir. o tempo presente "(página 28).

Matemáticos que deram grandes contribuições ao construtivismo

Galhos

Veja também

Notas

Referências

links externos