prova analítica - Analytic proof

Em matemática , uma prova analítica é uma prova de um teorema na análise que só faz uso de métodos de análise, e que não predominantemente fazer uso de métodos algébricos ou geométricos. O termo foi utilizado pela primeira vez por Bernard Bolzano , que primeiro fornecida uma prova não analítica do seu teorema valor intermédio e, em seguida, alguns anos mais tarde fornecida uma prova do teorema que estava livre de intuição referentes às linhas que atravessam um ao outro num ponto, e assim ele se sentia feliz chamando-analítica (Bolzano 1817).

Obra filosófica de Bolzano incentivou uma leitura mais abstrata de quando uma demonstração poderia ser considerado como analítica, onde a prova é analítica se ele não excede seu assunto (Sebastik 2007). Em teoria da prova , uma prova analítica passou a significar uma prova cuja estrutura é simples, de modo especial, devido às condições sobre o tipo de inferências que asseguram que nenhum deles vai além do que está contido nos pressupostos e que está demonstrado.

teoria da prova estrutural

Em teoria da prova, a noção da prova analítica fornece o conceito fundamental que traz as semelhanças entre uma série de essencialmente distinta cálculos prova , por isso, definir o subcampo da teoria da prova estrutural . Não existe uma definição geral incontroversa da prova analítica, mas para vários cálculos prova existe uma noção aceita. Por exemplo:

• Em Gerhard Gentzen 's cálculo dedução natural as provas analíticas são aqueles em forma normal; isto é, não ocorrência fórmula é tanto o principal pressuposto de uma regra de eliminação e a conclusão de uma regra de introdução;
• Em de Gentzen cálculo de sequentes as provas analíticas são aquelas que não usam a regra de corte .

No entanto, é possível estender as regras de inferência de ambos os cálculos para que não haja provas de que satisfazem a condição, mas não são analíticas. Por exemplo, um exemplo particularmente difícil de esta é a regra corte analítico , amplamente utilizado no método de quadro , que é um caso especial da regra de corte, onde a fórmula corte é um subfórmula de fórmulas laterais da regra de corte: uma prova de que contém um corte analítico é em virtude de que a regra não analítica.

Além disso, as teorias à prova estruturais que não são análogas às teorias de Gentzen ter outras noções de prova analítica. Por exemplo, o cálculo de estruturas organiza suas regras de inferência em pares, chamado o fragmento para cima e o fragmento para baixo, e uma prova analítica é aquele que contém apenas o fragmento baixo.

Veja também

• semântica prova teórica

Referências

• Bernard Bolzano (1817). Prova puramente analítica do teorema que entre quaisquer dois valores que dão resultados de sinal oposto, encontra-se pelo menos uma verdadeira raiz da equação. Em Abhandlungen der Königlichen bohmischen Gesellschaft der Wissenschaften Vol. V, pp.225-48.
• Pfenning (1984). Analítica e Provas não-analíticas. Em Proc. 7ª Conferência Internacional sobre Automated dedução .
• Sebastik (2007). Lógica de Bolzano . Entrada na Stanford Encyclopedia of Philosophy .