Essa pergunta é inspirada por uma pergunta semelhante sobre a matemática aplicada no excesso de matemática, e esse pensamento persistente de que questões importantes do TCS, como P vs. NP, podem ser independentes do ZFC (ou de outros sistemas). Como pano de fundo, a matemática reversa é o projeto de encontrar os axiomas necessários para provar certos teoremas importantes. Em outras palavras, começamos com um conjunto de teoremas que esperamos ser verdadeiros e tentamos derivar o conjunto mínimo de axiomas "naturais" que os tornam verdadeiros.
Fiquei me perguntando se a abordagem da matemática reversa foi aplicada a algum teorema importante do TCS. Em particular à teoria da complexidade. Com o impasse em muitas questões abertas no TCS, parece natural perguntar "que axiomas não tentamos usar?". Como alternativa, alguma questão importante no TCS demonstrou ser independente de certos subsistemas simples da aritmética de segunda ordem?
fonte
Respostas:
Sim, o tópico foi estudado na complexidade da prova. É chamado de Matemática Reversa Limitada . Você pode encontrar uma tabela contendo alguns resultados de matemática reversa na página 8 do livro de Cook e Nguyen, " Fundamentos lógicos da complexidade da prova ", 2010. Alguns dos alunos anteriores de Steve Cook trabalharam em tópicos semelhantes, por exemplo, a tese de Nguyen, " Matemática reversa vinculada ". Universidade de Toronto, 2008.
Alexander Razborov (também outros teóricos da complexidade da prova) tem alguns resultados sobre as teorias fracas necessárias para formalizar as técnicas de complexidade do circuito e provar os limites inferiores da complexidade do circuito. Ele obtém alguns resultados de improvabilidade para teorias fracas, mas as teorias são consideradas fracas demais.
Todos esses resultados são prováveis em (teoria básica de Simpson para a matemática reversa), portanto, a AFAIK não temos resultados de independência de teorias fortes (e, de fato, esses resultados de independência teriam fortes consequências como Neel mencionou, veja o trabalho de Ben-David (e resultados relacionados) sobre a independência de de que é uma extensão do ).R CUMA0 0 P vs.N P PUMA1 1 PUMA1 1 PUMA
fonte
Como resposta positiva à sua pergunta final, provas de normalização de cálculos lambda polimórficos, como o cálculo de construções, exigem pelo menos aritmética de ordem superior, e sistemas mais fortes (como o cálculo de construções indutivas) são equivalentes ao ZFC, além de muitos inacessíveis.
Como resposta negativa à sua pergunta final, Ben-David e Halevi mostraram que se é independente de , a aritmética Peano estendida com axiomas para todas as verdades aritméticas universais, existe um algoritmo quase polinomial para SAT. Além disso, atualmente não há maneiras conhecidas de gerar sentenças independentes do mas não do .P≠ NP PUMA1 1 D TEuME( nregistro∗( N )) PUMA PUMA1 1
Mais filosoficamente, não cometa o erro de equiparar força de consistência com a força de uma abstração.
A maneira correta de organizar um assunto pode envolver princípios aparentemente teóricos, embora não sejam estritamente necessários em termos de força de consistência. Por exemplo, princípios fortes de coleta são muito úteis para declarar propriedades de uniformidade - por exemplo, os teóricos das categorias acabam querendo axiomas cardinais grandes e fracos para manipular coisas como categoria de todos os grupos como se fossem objetos. O exemplo mais famoso é a geometria algébrica, cujo desenvolvimento faz uso extensivo dos universos de Grothendieck, mas todas as aplicações (como o Último Teorema de Fermat) aparentemente se enquadram na aritmética de terceira ordem. Como um exemplo muito mais trivial, observe que as operações genéricas de identidade e composição não são funções, pois são indexadas em todo o universo de conjuntos.
Por outro lado, às vezes a relação entre força de consistência e abstração vai na direção oposta. Considere a relação entre medidas e medidas motivacionais. As medidas são definidos em famílias de subconjuntos ( -álgebras) ao longo de um conjunto , enquanto medidas motívicas são definidos directamente em fórmulas interpretados em . Portanto, mesmo que a medida motivadora generalize a medida, a complexidade da teoria dos conjuntos diminui , pois um uso do powerset desaparece.σ X X
EDIT: O sistema lógico A possui uma força de consistência maior que o sistema B, se a consistência de A implica a consistência de B. Por exemplo, o ZFC possui uma força de consistência maior que a aritmética Peano, pois é possível provar a consistência do PA no ZFC. A e B têm a mesma força de consistência se forem equiconsistentes. Como exemplo, a aritmética Peano é consistente se e somente se a aritmética Heyting (construtiva) for.
Na IMO, um dos fatos mais surpreendentes sobre a lógica é que a força da consistência se resume à pergunta "qual é a função que mais cresce que você pode provar ser total nessa lógica?" Como resultado, a consistência de muitas classes de lógicas pode ser ordenada linearmente! Se você possui uma notação ordinal capaz de descrever as funções de crescimento mais rápido que suas duas lógicas podem mostrar total, então você sabe por tricotomia que uma delas pode provar a consistência da outra ou é equiconsistente.
Mas esse fato surpreendente também é o motivo pelo qual a força da consistência não é a ferramenta certa para falar sobre abstrações matemáticas. É invariável em um sistema, incluindo truques de codificação, e uma boa abstração permite que você expresse uma ideia sem truques. No entanto, não sabemos o suficiente sobre lógica para expressar essa idéia formalmente.
fonte