Teoria da prova - Proof theory

A teoria da prova é um ramo importante da lógica matemática que representa as provas como objetos matemáticos formais , facilitando sua análise por técnicas matemáticas. As provas são normalmente apresentadas como estruturas de dados definidas indutivamente , como listas simples, listas em caixas ou árvores , que são construídas de acordo com os axiomas e regras de inferência do sistema lógico. Como tal, a teoria da prova é de natureza sintática , em contraste com a teoria do modelo , que é semântica por natureza.

Algumas das principais áreas de teoria prova incluem teoria estrutural prova , análise ordinal , lógica provabilidade , matemática reversa , mineração prova , demonstração de teoremas automatizado , e complexidade prova . Muitas pesquisas também se concentram em aplicações em ciência da computação, linguística e filosofia.

História

Embora a formalização da lógica tenha sido muito avançada pelo trabalho de figuras como Gottlob Frege , Giuseppe Peano , Bertrand Russell e Richard Dedekind , a história da teoria da prova moderna é frequentemente vista como tendo sido estabelecida por David Hilbert , que iniciou o que é chamado de Hilbert's programa nos Fundamentos da Matemática . A ideia central deste programa era que se pudéssemos dar provas finitárias de consistência para todas as teorias formais sofisticadas necessárias aos matemáticos, então poderíamos fundamentar essas teorias por meio de um argumento metamatemático, que mostra que todas as suas afirmações puramente universais (mais tecnicamente, suas sentenças prováveis ) são finitariamente verdadeiras; uma vez assim fundamentados, não nos importamos com o significado não finitário de seus teoremas existenciais, considerando-os como estipulações pseudo-significativas da existência de entidades ideais. ${\ displaystyle \ Pi _ {1} ^ {0}}$

O fracasso do programa foi induzido pelos teoremas da incompletude de Kurt Gödel , que mostraram que qualquer teoria consistente com ω que seja suficientemente forte para expressar certas verdades aritméticas simples, não pode provar sua própria consistência, o que na formulação de Gödel é uma sentença. No entanto, versões modificadas do programa de Hilbert surgiram e pesquisas foram realizadas em tópicos relacionados. Isso levou, em particular, a: ${\ displaystyle \ Pi _ {1} ^ {0}}$

• Refinamento do resultado de Gödel, particularmente o refinamento de J. Barkley Rosser , enfraquecendo o requisito acima de consistência ω para consistência simples;
• Axiomatização do núcleo do resultado de Gödel em termos de uma linguagem modal, lógica de provabilidade ;
• Iteração transfinita de teorias, devido a Alan Turing e Solomon Feferman ;
• A descoberta de teorias de autoverificação , sistemas fortes o suficiente para falar sobre si mesmos, mas fracos demais para realizar o argumento diagonal que é a chave para o argumento da improvável de Gödel.

Paralelamente à ascensão e queda do programa de Hilbert, as bases da teoria da prova estrutural estavam sendo fundadas. Jan Łukasiewicz sugeriu em 1926 que alguém poderia melhorar os sistemas de Hilbert como uma base para a apresentação axiomática da lógica se alguém permitisse tirar conclusões de suposições nas regras de inferência da lógica. Em resposta a isso, Stanisław Jaśkowski (1929) e Gerhard Gentzen (1934) forneceram independentemente tais sistemas, chamados cálculos de dedução natural , com a abordagem de Gentzen introduzindo a ideia de simetria entre os fundamentos para afirmar proposições, expressos em regras de introdução , e as consequências de aceitar proposições nas regras de eliminação , uma ideia que se provou muito importante na teoria da prova. Gentzen (1934) introduziu ainda mais a ideia do cálculo sequente , um cálculo avançado em um espírito semelhante que melhor expressou a dualidade dos conectivos lógicos, e passou a fazer avanços fundamentais na formalização da lógica intuicionista, e fornecer a primeira prova combinatória da consistência da aritmética de Peano . Juntos, a apresentação da dedução natural e do cálculo sequente introduziu a ideia fundamental da prova analítica para a teoria da prova.

Teoria da prova estrutural

A teoria da prova estrutural é a subdisciplina da teoria da prova que estuda as especificidades dos cálculos da prova . Os três estilos mais conhecidos de cálculo de prova são:

• Os cálculos de Hilbert
• Os cálculos de dedução natural
• Os cálculos sequentes

Cada um deles pode dar uma formalização completa e axiomática da lógica proposicional ou predicativa do sabor clássico ou intuicionista , quase qualquer lógica modal e muitas lógicas subestruturais , como a lógica da relevância ou a lógica linear . Na verdade, é incomum encontrar uma lógica que resista a ser representada em um desses cálculos.

Os teóricos da prova estão tipicamente interessados ​​em cálculos de prova que apóiam uma noção de prova analítica . A noção de prova analítica foi introduzida por Gentzen para o cálculo sequente; lá, as provas analíticas são aquelas que são livres de cortes . Muito do interesse em provas livres de corte vem da propriedade da subfórmula: toda fórmula na sequência final de uma prova livre de corte é uma subfórmula de uma das premissas. Isso permite que se mostre facilmente a consistência do cálculo sequencial; se o sequente vazio fosse derivável, teria de ser uma subfórmula de alguma premissa, o que não é. O teorema intermediário de Gentzen, o teorema de interpolação de Craig e o teorema de Herbrand também seguem como corolários do teorema de eliminação de corte.

O cálculo de dedução natural de Gentzen também apóia a noção de prova analítica, como mostrado por Dag Prawitz . A definição é um pouco mais complexa: dizemos que as provas analíticas são as formas normais , que estão relacionadas à noção de forma normal na reescrita de termos. Cálculos de prova mais exóticos, como as redes de prova de Jean-Yves Girard , também apóiam a noção de prova analítica.

Uma família particular de provas analíticas que surgem na lógica redutiva são provas focalizadas que caracterizam uma grande família de procedimentos de busca de provas direcionados a objetivos. A capacidade de transformar um sistema de prova em uma forma focada é uma boa indicação de sua qualidade sintática, de maneira semelhante a como a admissibilidade de corte mostra que um sistema de prova é sintaticamente consistente.

A teoria da prova estrutural está conectada à teoria dos tipos por meio da correspondência Curry-Howard , que observa uma analogia estrutural entre o processo de normalização no cálculo de dedução natural e a redução beta no cálculo lambda tipado . Isso fornece a base para a teoria dos tipos intuicionista desenvolvida por Per Martin-Löf , e muitas vezes se estende a uma correspondência de três vias, a terceira perna das quais são as categorias fechadas cartesianas .

Outros tópicos de pesquisa em teoria estrutural incluem tableau analítico, que aplica a ideia central da prova analítica da teoria da prova estrutural para fornecer procedimentos de decisão e procedimentos de semidecisão para uma ampla gama de lógicas e a teoria da prova de lógicas subestruturais.

Análise ordinal

A análise ordinal é uma técnica poderosa para fornecer provas de consistência combinatória para subsistemas de aritmética, análise e teoria dos conjuntos. O segundo teorema da incompletude de Gödel é freqüentemente interpretado como uma demonstração de que as provas de consistência finitística são impossíveis para teorias de força suficiente. A análise ordinal permite medir com precisão o conteúdo infinitário da consistência das teorias. Para uma teoria T axiomatizada recursivamente consistente, pode-se provar na aritmética finitística que a fundamentação de um determinado ordinal transfinito implica a consistência do segundo teorema da incompletude de T. Gödel implica que a fundamentação de tal ordinal não pode ser provada na teoria T.

As consequências da análise ordinal incluem (1) consistência dos subsistemas da aritmética de segunda ordem clássica e teoria dos conjuntos em relação às teorias construtivas, (2) resultados de independência combinatória e (3) classificações de funções recursivas comprovadamente totais e ordinais comprovadamente bem fundamentados.

A análise ordinal foi originada por Gentzen, que comprovou a consistência da Aritmética de Peano usando indução transfinita até ε ₀ ordinal . A análise ordinal foi estendida a muitos fragmentos de aritmética de primeira e segunda ordem e teoria dos conjuntos. Um grande desafio tem sido a análise ordinal das teorias impredicativas. O primeiro avanço nessa direção foi a prova de Takeuti da consistência de Π¹
₁-CA ₀ usando o método de diagramas ordinais.

Lógica de Provabilidade

A lógica de provabilidade é uma lógica modal , na qual o operador de caixa é interpretado como 'é provável que'. O objetivo é capturar a noção de um predicado de prova de uma teoria formal razoavelmente rica . Como axiomas básicos da lógica de provabilidade GL ( Gödel - Löb ), que captura provável na Aritmética de Peano , toma-se análogos modais das condições de derivabilidade de Hilbert-Bernays e do teorema de Löb (se for provável que a provabilidade de A implica A, então A é comprovável).

Alguns dos resultados básicos relativos à incompletude da aritmética de Peano e teorias relacionadas têm análogos na lógica de provabilidade. Por exemplo, é um teorema em GL que se uma contradição não é provável, então não é provável que uma contradição não seja provável (segundo teorema da incompletude de Gödel). Existem também análogos modais do teorema do ponto fixo. Robert Solovay provou que a lógica modal GL é completa com respeito à aritmética de Peano. Ou seja, a teoria proposicional de provabilidade na Aritmética de Peano é completamente representada pela lógica modal GL. Isso implica diretamente que o raciocínio proposicional sobre a provabilidade na Aritmética de Peano é completo e decidível.

Outra pesquisa em lógica de provabilidade enfocou a lógica de provabilidade de primeira ordem, lógica de provabilidade polimodal (com uma modalidade representando provabilidade na teoria do objeto e outra representando provabilidade na metateoria) e lógicas de interpretabilidade destinadas a capturar a interação entre provabilidade e interpretabilidade . Algumas pesquisas muito recentes envolveram aplicações de álgebras de probabilidade graduada à análise ordinal de teorias aritméticas.

Matemática reversa

A matemática reversa é um programa em lógica matemática que visa determinar quais axiomas são necessários para provar teoremas da matemática. O campo foi fundado por Harvey Friedman . Seu método de definição pode ser descrito como "retroceder dos teoremas aos axiomas ", em contraste com a prática matemática comum de derivar teoremas de axiomas. O programa de matemática reversa foi prenunciado por resultados na teoria dos conjuntos, como o teorema clássico de que o axioma da escolha e o lema de Zorn são equivalentes à teoria dos conjuntos ZF . O objetivo da matemática reversa, no entanto, é estudar possíveis axiomas de teoremas ordinários da matemática, em vez de possíveis axiomas para a teoria dos conjuntos.

Na matemática reversa, começa-se com uma linguagem de estrutura e uma teoria básica - um sistema de axioma central - que é muito fraca para provar a maioria dos teoremas nos quais pode estar interessado, mas ainda poderosa o suficiente para desenvolver as definições necessárias para enunciar esses teoremas. Por exemplo, para estudar o teorema "Toda sequência limitada de números reais tem um supremo " é necessário usar um sistema de base que possa falar de números reais e sequências de números reais.

Para cada teorema que pode ser declarado no sistema de base, mas não pode ser demonstrado no sistema de base, o objetivo é determinar o sistema de axioma particular (mais forte do que o sistema de base) que é necessário para provar esse teorema. Para mostrar que um sistema S é necessário para provar um teorema T , duas provas são necessárias. A primeira prova mostra que T pode ser provado por S ; esta é uma prova matemática ordinária, juntamente com uma justificação que pode ser realizado no sistema S . A segunda prova, conhecida como reversão , mostra que o próprio T implica S ; esta prova é realizada no sistema básico. Os estabelece que nenhum sistema de reversão axioma S ' que se estende para o sistema de base pode ser mais fraca do que S enquanto ainda provando  T .

Um fenômeno notável na matemática reversa é a robustez dos sistemas de axiomas dos Cinco Grandes . Em ordem crescente de resistência, esses sistemas são nomeados pelos inicialismos RCA ₀ , WKL ₀ , ACA ₀ , ATR ₀ e Π¹
₁-CA ₀ . Quase todos os teoremas da matemática comum que foram analisados ​​matematicamente de forma reversa provaram ser equivalentes a um desses cinco sistemas. Muitas pesquisas recentes têm se concentrado em princípios combinatórios que não se encaixam perfeitamente nesta estrutura, como RT²
₂ (Teorema de Ramsey para pares).

A pesquisa em matemática reversa frequentemente incorpora métodos e técnicas da teoria da recursão , bem como da teoria da prova.

Interpretações funcionais

Interpretações funcionais são interpretações de teorias não construtivas em teorias funcionais. As interpretações funcionais geralmente ocorrem em dois estágios. Em primeiro lugar, "reduz-se" uma teoria clássica C a uma intuicionista I. Ou seja, fornece-se um mapeamento construtivo que traduz os teoremas de C aos teoremas de I. Em segundo lugar, reduz-se a teoria intuicionista I a uma teoria quantificadora livre de funcionais F. Essas interpretações contribuem para uma forma do programa de Hilbert, uma vez que provam a consistência das teorias clássicas em relação às construtivas. Interpretações funcionais bem-sucedidas resultaram em reduções de teorias infinitárias em teorias finitárias e teorias impredicativas em teorias predicativas.

As interpretações funcionais também fornecem uma maneira de extrair informações construtivas de provas na teoria reduzida. Como consequência direta da interpretação, geralmente obtém-se o resultado de que qualquer função recursiva cuja totalidade possa ser comprovada em I ou em C é representada por um termo de F. Se for possível fornecer uma interpretação adicional de F em I, que às vezes é possível, essa caracterização geralmente se mostra exata. Freqüentemente, os termos de F coincidem com uma classe natural de funções, como as funções primitivas recursivas ou computáveis ​​em tempo polinomial. Interpretações funcionais também têm sido usadas para fornecer análises ordinais de teorias e classificar suas funções comprovadamente recursivas.

O estudo das interpretações funcionais começou com a interpretação de Kurt Gödel da aritmética intuicionista em uma teoria livre de quantificadores de funcionais de tipo finito. Essa interpretação é comumente conhecida como interpretação Dialética . Junto com a interpretação de dupla negação da lógica clássica na lógica intuicionista, ele fornece uma redução da aritmética clássica à aritmética intuicionista.

Prova formal e informal

As provas informais da prática matemática cotidiana são diferentes das provas formais da teoria da prova. São mais como esboços de alto nível que permitiriam a um especialista reconstruir uma prova formal, pelo menos em princípio, com tempo e paciência suficientes. Para a maioria dos matemáticos, escrever uma prova totalmente formal é muito pedante e prolixo para ser de uso comum.

As provas formais são construídas com a ajuda de computadores na prova interativa de teoremas . Significativamente, essas provas podem ser verificadas automaticamente, também por computador. Verificar provas formais é geralmente simples, enquanto encontrar provas (prova automatizada de teoremas ) é geralmente difícil. Uma prova informal na literatura matemática, ao contrário, requer semanas de revisão por pares para ser verificada e ainda pode conter erros.

Semântica teórica de prova

Em lingüística , gramática tipo lógica , gramática categorial e Montague gramática aplicam formalismos baseados na teoria da prova estrutural para dar uma formais semântica de linguagem natural .

Veja também

• Lógica intermediária
• Teoria do modelo
• Prova (verdade)
• Técnicas de prova
• Cálculo sequencial

Notas

Referências

• J. Avigad e EH Reck (2001). "'Esclarecendo a natureza do infinito': o desenvolvimento da metamatemática e da teoria da prova ". Carnegie-Mellon Technical Report CMU-PHIL-120.
• J. Barwise , ed. (1978). Handbook of Mathematical Logic . Holanda do Norte.
• S. Buss, ed. (1998) Handbook of Proof Theory . Elsevier.
• AS Troelstra e H. Schwichtenberg (1996). Basic Proof Theory , Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, ISBN  0-521-77911-1 .
• G. Gentzen (1935/1969). " Investigações em dedução lógica ". Em ME Szabo, ed. Artigos coletados de Gerhard Gentzen . Holanda do Norte. Traduzido por Szabo de "Untersuchungen über das logische Schliessen", Mathematisches Zeitschrift v. 39, pp. 176–210, 405 431.
• D. Prawitz (1965). Dedução natural: um estudo teórico de prova , Dover Publications, ISBN  978-0-486-44655-4
• SG Simpson (2010). Subsistemas de aritmética de segunda ordem , segunda edição. Cambridge University Press, ISBN  978-0521150149 .
• H. Wang (1981). Popular Lectures on Mathematical Logic , Van Nostrand Reinhold Company , ISBN  0-442-23109-1 .

links externos

• "Teoria da prova" , Encyclopedia of Mathematics , EMS Press , 2001 [1994]
• J. von Plato (2008). The Development of Proof Theory . Stanford Encyclopedia of Philosophy .