Prova construtiva - Constructive proof

Em matemática , uma prova construtiva é um método de prova que demonstra a existência de um objeto matemático criando ou fornecendo um método para criar o objeto. Isso contrasta com uma prova não construtiva (também conhecida como prova de existência ou teorema da existência pura ), que prova a existência de um tipo particular de objeto sem fornecer um exemplo. Para evitar confusão com o conceito mais forte que se segue, essa prova construtiva é às vezes chamada de prova eficaz .

Uma prova construtiva também pode se referir ao conceito mais forte de uma prova que é válida na matemática construtiva . O construtivismo é uma filosofia matemática que rejeita todos os métodos de prova que envolvem a existência de objetos que não são explicitamente construídos. Isso exclui, em particular, o uso da lei do meio excluído , o axioma do infinito e o axioma da escolha , e induz um significado diferente para alguma terminologia (por exemplo, o termo "ou" tem um significado mais forte em termos construtivos matemática do que na clássica).

Algumas provas não construtivas mostram que se certa proposição é falsa, segue-se uma contradição; conseqüentemente, a proposição deve ser verdadeira ( prova por contradição ). No entanto, o princípio da explosão ( ex falso quodlibet ) foi aceito em algumas variedades da matemática construtiva, incluindo o intuicionismo .

Provas construtivas pode ser visto como definindo matemáticas certificados algoritmos : essa idéia é explorada na interpretação Brouwer-Heyting-Kolmogorov da lógica construtiva , a correspondência Curry-Howard entre provas e programas, e tais sistemas lógicos como Per Martin-Löf 's tipo intuitionistic teoria , e Thierry Coquand e Gérard Huet 's cálculo das construções .

Um exemplo histórico

Até o final do século 19, todas as provas matemáticas eram essencialmente construtivas. As primeiras construções não construtivas apareceram com a teoria dos conjuntos infinitos de Georg Cantor e a definição formal de números reais .

O primeiro uso de provas não construtivas para resolver problemas previamente considerados parece ser o Nullstellensatz de Hilbert e o teorema da base de Hilbert . Do ponto de vista filosófico, o primeiro é especialmente interessante, pois implica a existência de um objeto bem especificado.

O Nullstellensatz pode ser declarado da seguinte forma: Se são polinômios em n indeterminados com coeficientes complexos , que não têm zeros complexos comuns , então existem polinômios tais que ${\ displaystyle f_ {1}, \ ldots, f_ {k}}$${\ displaystyle g_ {1}, \ ldots, g_ {k}}$

${\ displaystyle f_ {1} g_ {1} + \ ldots + f_ {k} g_ {k} = 1.}$

Esse teorema da existência não construtiva foi uma surpresa tão grande para os matemáticos da época que um deles, Paul Gordan , escreveu: "isto não é matemática, é teologia ".

Vinte e cinco anos depois, Grete Hermann forneceu um algoritmo para computação que não é uma prova construtiva no sentido forte, pois ela usou o resultado de Hilbert. Ela provou que, se existem, podem ser encontrados com graus menores que . ${\ displaystyle g_ {1}, \ ldots, g_ {k},}$${\ displaystyle g_ {1}, \ ldots, g_ {k}}$${\ displaystyle 2 ^ {2 ^ {n}}}$

Isso fornece um algoritmo, pois o problema é reduzido a resolver um sistema de equações lineares , considerando como incógnitas o número finito de coeficientes do ${\ displaystyle g_ {i}.}$

Exemplos

Provas não construtivas

Considere primeiro o teorema de que há uma infinidade de números primos . A prova de Euclides é construtiva. Mas uma maneira comum de simplificar a prova de Euclides postula que, ao contrário da afirmação do teorema, há apenas um número finito deles, caso em que há um maior, denotado n . Então considere o número n ! + 1 (1 + o produto dos primeiros n números). Ou esse número é primo ou todos os seus fatores primos são maiores que n . Sem estabelecer um número primo específico, isso prova que existe um que é maior que n , ao contrário do postulado original.

Agora considere o teorema "existem números irracionais e isso é racional ." Este teorema pode ser provado usando uma prova construtiva e uma prova não construtiva. ${\ displaystyle a}$${\ displaystyle b}$${\ displaystyle a ^ {b}}$

A seguinte prova de 1953 por Dov Jarden tem sido amplamente usada como um exemplo de uma prova não construtiva desde pelo menos 1970:

CURIOSA
339. Uma prova simples de que a potência de um número irracional para um expoente irracional pode ser racional. é racional ou irracional. Se for racional, nossa afirmação está provada. Se for irracional, comprova nossa afirmação.      Dov Jarden Jerusalém
${\ displaystyle {\ sqrt {2}} ^ {\ sqrt {2}}}$${\ displaystyle ({\ sqrt {2}} ^ {\ sqrt {2}}) ^ {\ sqrt {2}} = 2}$

Em um pouco mais de detalhes:

• Lembre-se de que isso é irracional e 2 é racional. Considere o número . Ou é racional ou é irracional. ${\ displaystyle {\ sqrt {2}}}$ ${\ displaystyle q = {\ sqrt {2}} ^ {\ sqrt {2}}}$
• Se for racional, então o teorema é verdadeiro, com e ambos sendo . ${\ displaystyle q}$${\ displaystyle a}$${\ displaystyle b}$${\ displaystyle {\ sqrt {2}}}$
• Se for irracional, então o teorema é verdadeiro, com ser e ser , uma vez que ${\ displaystyle q}$${\ displaystyle a}$${\ displaystyle {\ sqrt {2}} ^ {\ sqrt {2}}}$${\ displaystyle b}$${\ displaystyle {\ sqrt {2}}}$

${\ displaystyle \ left ({\ sqrt {2}} ^ {\ sqrt {2}} \ right) ^ {\ sqrt {2}} = {\ sqrt {2}} ^ {({\ sqrt {2}} \ cdot {\ sqrt {2}})} = {\ sqrt {2}} ^ {2} = 2.}$

Em sua essência, essa prova não é construtiva porque se baseia na afirmação "Ou q é racional ou é irracional" - uma instância da lei do terceiro excluído , que não é válida dentro de uma prova construtiva. A prova não construtiva não constrói um exemplo a e b ; simplesmente dá uma série de possibilidades (neste caso, duas possibilidades mutuamente exclusivas) e mostra que uma delas - mas não mostra qual - deve fornecer o exemplo desejado.

Ao que parece, é irracional por causa do teorema de Gelfond-Schneider , mas esse fato é irrelevante para a correção da prova não construtiva. ${\ displaystyle {\ sqrt {2}} ^ {\ sqrt {2}}}$

Provas construtivas

Uma prova construtiva do teorema acima sobre os poderes irracionais dos irracionais daria um exemplo real, como:

${\ displaystyle a = {\ sqrt {2}} \ ,, \ quad b = \ log _ {2} 9 \ ,, \ quad a ^ {b} = 3 \ ,.}$

A raiz quadrada de 2 é irracional e 3 é racional. também é irracional: se fosse igual a , então, pelas propriedades dos logaritmos , 9 ⁿ seria igual a 2 ^m , mas o primeiro é ímpar e o último é par. ${\ displaystyle \ log _ {2} 9}$${\ displaystyle m \ over n}$

Um exemplo mais substancial é o teorema menor do gráfico . Uma consequência desse teorema é que um gráfico pode ser desenhado no toro se, e somente se, nenhum de seus menores pertencer a um certo conjunto finito de " menores proibidos ". No entanto, a prova da existência desse conjunto finito não é construtiva, e os menores proibidos não são realmente especificados. Eles ainda são desconhecidos.

Contra-exemplos brouwerianos

Na matemática construtiva , uma afirmação pode ser refutada dando-se um contra - exemplo , como na matemática clássica. No entanto, também é possível dar um contra - exemplo brouweriano para mostrar que a afirmação não é construtiva. Esse tipo de contra-exemplo mostra que a afirmação implica algum princípio que se sabe ser não construtivo. Se puder ser provado construtivamente que uma afirmação implica algum princípio que não pode ser provado construtivamente, então a afirmação em si não pode ser provada de forma construtiva.

Por exemplo, uma declaração particular pode ser mostrada para implicar a lei do terceiro excluído. Um exemplo de contraexemplo brouweriano desse tipo é o teorema de Diaconescu , que mostra que o axioma completo da escolha é não construtivo em sistemas de teoria dos conjuntos construtivos , uma vez que o axioma da escolha implica a lei do meio excluído em tais sistemas. O campo da matemática reversa construtiva desenvolve ainda mais essa ideia, classificando vários princípios em termos de "quão não construtivos" eles são, mostrando que são equivalentes a vários fragmentos da lei do terceiro excluído.

Brouwer também forneceu contra-exemplos "fracos". Esses contra-exemplos não refutam uma afirmação, entretanto; eles apenas mostram que, no momento, nenhuma prova construtiva da afirmação é conhecida. Um contra-exemplo fraco começa pegando algum problema não resolvido de matemática, como a conjectura de Goldbach , que pergunta se todo número natural par maior do que 4 é a soma de dois primos. Defina uma sequência a ( n ) de números racionais da seguinte forma:

${\ displaystyle a (n) = {\ begin {cases} (1/2) ^ {n} & {\ mbox {se cada número natural par no intervalo}} [4, n] {\ mbox {é a soma de dois primos}}, \\ (1/2) ^ {k} & {\ mbox {if}} k {\ mbox {é o menor número natural par no intervalo}} [4, n] {\ mbox { que não é a soma de dois primos}} \ end {cases}}}$

Para cada n , o valor de a ( n ) pode ser determinado por pesquisa exaustiva e, portanto, a é uma sequência bem definida, construtivamente. Além disso, como a é uma sequência de Cauchy com uma taxa fixa de convergência, a converge para algum número real α, de acordo com o tratamento usual de números reais em matemática construtiva.

Vários fatos sobre o número real α podem ser provados construtivamente. No entanto, com base no significado diferente das palavras na matemática construtiva, se houver uma prova construtiva de que "α = 0 ou α ≠ 0", isso significaria que há uma prova construtiva da conjectura de Goldbach (no primeiro caso) ou uma prova construtiva de que a conjectura de Goldbach é falsa (no último caso). Como nenhuma prova desse tipo é conhecida, a declaração citada também não deve ter uma prova construtiva conhecida. No entanto, é inteiramente possível que a conjectura de Goldbach possa ter uma prova construtiva (como não sabemos no momento se tem), caso em que a declaração citada teria uma prova construtiva também, embora uma que seja desconhecida no momento. O principal uso prático de contra-exemplos fracos é identificar a "dureza" de um problema. Por exemplo, o contra-exemplo mostrado mostra que a declaração citada é "pelo menos tão difícil de provar" quanto a conjectura de Goldbach. Contra-exemplos fracos desse tipo costumam estar relacionados ao princípio limitado da onisciência .

Veja também

• Construtivismo (filosofia da matemática)
• Errett Bishop - autor do livro "Foundations of Constructive Analysis".
• Teorema da existência § Resultados da existência 'pura'
• Provas de existência de algoritmo não construtivo
• Método probabilístico

Referências

Leitura adicional

links externos

• Fracos contra-exemplos de Mark van Atten, Stanford Encyclopedia of Philosophy