Construtivismo (matemática)

Na filosofia da matemática, o construtivismo afirma que é preciso encontrar (ou "construir") um objeto matemático para provar que ele existe. Quando se assume que um objeto não existe e deriva uma contradição dessa suposição, ainda não encontrou-se o objeto e, portanto, não é provada a sua existência, de acordo com o construtivismo. Este ponto de vista envolve uma interpretação verificacional do quantificador de existência, o que está em desacordo com a sua interpretação clássica.

Há muitas formas de construtivismo. Estes incluem o programa de intuicionismo fundado por Brouwer, o finitismo de Hilbert e Bernays, a matemática recursiva construtiva de Shanin, e o programa de análise construtiva. de Markov e Bishop. O Construtivismo também inclui o estudo da teoria dos conjuntos construtivos como IZF e o estudo da teoria dos topos.

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

Matemática Construtiva

Muito da matemática construtiva usa a lógica intuicionista, que é essencialmente a lógica clássica sem a lei do terceiro excluído. Esta lei estabelece que, para qualquer proposição, a própria proposição ou sua negação é verdadeira. Isso não quer dizer que a lei do terceiro excluído é 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 declarações contraditórias não podem ser verdadeiras ao mesmo tempo) ainda é válida.

Por exemplo, na aritmética de Heyting, pode-se provar que, para qualquer proposição P que não contém quantificadores, $\forall x,y,z,\ldots \in \mathbb {N} :p\vee \neg p$ é um teorema (onde x, y, z... são as variáveis livres na proposição p). Neste sentido, as proposições restritas ao finito ainda são consideradas como sendo verdadeiras ou falsas, pois elas estão na matemática clássica, mas esta bivalência não se estende às proposições que referem-se a infinitas coleções.

Na verdade, L.E.J. Brouwer, fundador da escola intuicionista, viu a lei do terceiro excluído como abstraída da experiência finita, e em seguida, aplicada ao infinito sem justificação. Por exemplo, a conjectura de Goldbach é a afirmação de que todo número par (maior que 2) é a soma de dois número primos. É possível testar para qualquer número par em particular, seja ele a soma de dois números primos ou não (por exemplo, por pesquisa exaustiva), de modo que qualquer um deles ou é a soma de dois números primos, ou não é. E até agora, cada número até hoje testado tem sido de fato a soma de dois números primos.

Mas não há nenhuma prova conhecida de que todos eles são assim, nem qualquer prova conhecida que nem todos eles sejam. Assim, para Brouwer, não temos justificativas em afirmar "ou conjectura de Goldbach é verdadeira, ou não." E enquanto a conjectura pode um dia ser resolvida, o argumento aplica-se a problemas semelhantes não resolvidos; para Brouwer, a lei do terceiro excluído era equivalente a assumir 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 restante tem uma propriedade existencial que a lógica clássica não: sempre que $\exists _{x\in X}P(x)$ é comprovada de forma construtiva, então $P(a)$ é provada de forma construtiva para (pelo menos) um $a\in x$ , muitas vezes chamado de testemunha . Assim, a comprovação da existência de um objeto matemático está ligada à possibilidade da sua construção.

Exemplo de análise real

Na análise real clássica, uma maneira para definir um número real é como uma classe equivalente da sucessão de Cauchys de números racionais.

na matemática construtiva, uma maneira de se construir um número real é como uma função matemática ƒ que recebe como entrada um inteiro positivo $n$ e retorna um ƒ(n) racional, juntos com a função g que recebe um inteiro positivo n and retorna um g(n) inteiro positivo de modo que

\forall n\ \forall i,j\geq g(n)\quad |f(i)-f(j)|\leq {1 \over n}

assim enquanto n aumenta, os valores de ƒ(n) ficam cada vez mais próximos. Podemos usar ƒ e 'g juntos para computar uma aproximação racional tão próxima quanto possível ao número real que elas representam

A partir dessa definição, uma simples representação do número real e é:

f(n)=\sum _{i=0}^{n}{1 \over i!},\quad g(n)=n.

Esta definição corresponde à definição clássica usando sequências de Cauchy, exceto por uma diferença na construção: para uma sequência de Cauchy clássica, é necessário que, para qualquer distância dada, existe (no sentido clássico) um membro na sequência em que todos os membros estão mais próximos que essa distância. Na versão construtiva, é necessário que, para qualquer distância, seja possível especificar um ponto na sequência onde isso acontece (Essa necessidade é geralmente chamada como módulo de convergência). na verdade, a interpretação construtiva padrão

\forall n:\exists m:\forall i,j\geq m:|f(i)-f(j)|\leq {1 \over n}

é precisamente a existência da função computando o módulo de convergência. Apesar da diferença entre as duas definições de números reais poder ser encarada como a diferença na interpretação da declaração "para todo... existe..."

Isto então abre a questão de que tipo de função de um conjunto enumerável para um conjunto enumerável, como f e g mostradas acima, podem ser realmente construídas. Diferentes versões de construtivismo discordam nesse ponto. Construções podem ser definidas de forma tão ampla como sequencias de livre escolha, que é o ponto de vista intuicionista, ou tão restritas quanto algoritmos(ou mais tecnicamente, à função computável), ou até mesmo ser deixadas indeterminadas. Se, por exemplo, a visão algorítmica é feita, então os reais construídos aqui são essencialmente o que classicamente seria chamado número calculável.

Cardinalidade

A interpretação algorítmica acima pode parecer estranha à noção clássica de cardinalidade. Enumerando algoritmos, podemos mostrar classicamente que os números computáveis são enumeráveis. Ainda assim o Argumento de diagonalização de Cantor mostra que números reais possuem maior cardinalidade. Além disso, o argumento diagonal parece perfeitamente construtivo. Identificar os números reais com os números computáveis seria então uma contradição.

E, de fato, o argumento diagonal de Cantor é construtivo, no senso de que dada a bijeção entre os números reais e os números naturais, se constrói um número real que não se encaixa, e assim prova uma contradição. Nós podemos de fato enumerar algoritmos para construir a função T, sobre a qual inicialmente assumiremos que se trata de uma função dos números naturais sobre os números reais. Mas, para cada algoritmo, pode-se corresponder ou não um número real, já que o algoritmo pode falhar em satisfazer as restrições, ou até não encerrar(T é uma função parcial), falhando assim em produzir a bijeção requerida. Resumindo, quem vê que os números reais são efetivamente computáveis interpreta os resultados de Cantor como se mostrando que os números reais não são conjuntos recursivamente enumeráveis. (veja Teorema de Cantor-Bernstein-Schroeder).

Axioma da escolha

O status de axioma da escolha em construtivismo matemático é complicado pelas diferentes abordagens de programas construtivistas diferentes. Um significado trivial de "construtivo", usado informalmente por matemáticos, é "provável na teoria dos conjuntos ZF sem o axioma da escolha." Entretanto, defensores de formas mais limitadas do construtivismo matemático não afirmaria que ZF é um sistema construtivo.

Nas teorias intuicionistas da teoria dos tipos (especialmente aritmética de alto nível), muitas formas do axioma da escolha são permitidas. Por exemplo, o axioma AC₁₁ pode ser parafraseado para dizer que para qualquer relação R no conjunto de números reais, se você provar que para cada número real x existe um número real y como R(x,y) possui, então deve existir uma função F onde R(x,F(x)) possui todos os números reais. Uma escolha similar de princípios são aceitas para todos os casos finitos. A motivação para aceitar esses princípios não construtivistas é o entendimento intuicionistas da prova que "para cada número real x existe um número real y que R('x,y) possui". De acordo com a interpretação de BHK, a própria prova é essencialmente a função F que é desejada. A escolha de princípios que intuicionalistas aceitam simplesmente não implicam na lei do terceiro excluído.

Entretanto, em certos sistemas axiomáticos para teoria dos conjuntos construtivicionistas, o axioma da escolha não implica a lei do terceiro excluído (na presença de axiomas), como mostrado pelo teorema de Diaconescu. Algumas teorias de conjuntos construtivicionistas incluem formas mais fracas de axiomas de escolha, como o axioma da escolha dependente na teoria dos conjuntos de Myhill.

Teoria da medida

A teoria da medida clássica faz uso pesado do axioma da escolha, que é fundamental para, primeiro, distinguir entre conjuntos mensuráveis e não mensuráveis, a existência do último estando por trás de resultado famosos como o Paradoxo de Banach–Tarski, e segundo, a hierarquia de noções de medida, capturadas por noções como a Álgebra de Borel, que são uma importante fonte de intuições para a teoria dos conjuntos. A teoria das medidas fornece fundação para a noção moderna de integral, a integral de Lebesgue.

O lugar do construtivismo na matemática

Tradicionalmente, alguns matemáticos têm sido duvidosos, se não antagônicos, a respeito do construtivismo matemático, principalmente por causa das limitações que eles acreditam que são impostas para a análise construtivista. Essas perspectivas foram fortemente expressadas por David Hilbert em 1928, quando ele escreveu em Die Grundlagen der Mathematik, "Tirar a lei do terceiro excluído de um matemático seria o equivalente a, por exemplo, tirar o telescópio de um astrônomo ou proibir um lutador de boxe de usar seus punhos". ^[1]

Errett Bishop, em seu trabalho Foundations of Constructive Analysis em 1967, se dedicou a dissipar esses medos através do desenvolvimento de uma grande quantidade de análises tradicionais em um enquadramento contrutivista. Não obstante, alguns matemáticos^[quem?] não aceitam que Bishop foi bem sucedido, uma vez que seu livro é necessariamente mais complicado do que um texto de análise clássica seria.

Ainda que a maior parte dos matemáticos não aceitem as teses construtivistas, métodos construtivistas estão ganhando interesse em áreas não ideológicas. Aplicações para a matemática construtivista foram encontradas no cálculo lambda tipado e lógica categórica.

Matemáticos construtivistas que fizeram grandes contribuções ao construtivismo

Ramos

Ver também

Notas

↑ Tradução tirada da Enciclopédia de Stanford de Filosofia [1].

Referências

Solomon Feferman (1997), Relationships between Constructive, Predicative and Classical Systems of Analysis, http://math.stanford.edu/~feferman/papers/relationships.pdf.
A. S. Troelstra (1977a), "Aspects of constructive mathematics", Handbook of Mathematical Logic, pp. 973–1052.
A. S. Troelstra (1977b), Choice sequences, Oxford Logic Guides. ISBN 0-19-853163-X
A. S. Troelstra (1991), "A History of Constructivism in the 20th Century", University of Amsterdam, ITLI Prepublication Series ML-91-05, https://web.archive.org/web/20060209210015/http://staff.science.uva.nl/~anne/hhhist.pdf,
H. M. Edwards (2005), Essays in Constructive Mathematics, Springer-Verlag, 2005, ISBN 0-387-21978-1
Douglas Bridges, Fred Richman, "Varieties of Constructive Mathematics", 1987.
Michael J. Beeson, "Foundations of constructive mathematics: metamathematical studies", 1985.
Anne Sjerp Troelstra, Dirk van Dalen, "Constructivism in Mathematics: An Introduction, Volume 1", 1988
Anne Sjerp Troelstra, Dirk van Dalen, "Constructivism in Mathematics: An Introduction, Volume 2", 1988

Ligações externas

Stanford Encyclopedia of Philosophy entry

[1] Tradução tirada da Enciclopédia de Stanford de Filosofia [1].

[1]