Matemática reversa - Reverse mathematics

A matemática reversa é um programa em lógica matemática que busca determinar quais axiomas são necessários para provar teoremas da matemática. Seu método de definição pode ser descrito resumidamente como "retroceder dos teoremas aos axiomas ", em contraste com a prática matemática comum de derivar teoremas de axiomas. Pode ser conceituado como a modelagem de condições necessárias a partir de condições suficientes .

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 comuns da matemática, em vez de possíveis axiomas para a teoria dos conjuntos.

A matemática reversa é geralmente realizada usando subsistemas de aritmética de segunda ordem , onde muitas de suas definições e métodos são inspirados em trabalhos anteriores em análise construtiva e teoria da prova . O uso da aritmética de segunda ordem também permite que muitas técnicas da teoria da recursão sejam empregadas; muitos resultados em matemática reversa têm resultados correspondentes em análises computáveis . Na matemática reversa de ordem superior , o foco está nos subsistemas da aritmética de ordem superior e na linguagem mais rica associada.

O programa foi fundado por Harvey Friedman  ( 1975 , 1976 ) e apresentado por Steve Simpson . Uma referência padrão para o assunto é Simpson (2009) , enquanto uma introdução para não especialistas é Stillwell (2018) . Uma introdução à matemática reversa de ordem superior, e também o artigo de base, é Kohlenbach (2005) .

Princípios gerais

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 .

Uso de aritmética de segunda ordem

A maioria das pesquisas em matemática reversa concentra-se em subsistemas da aritmética de segunda ordem . O corpo de pesquisas em matemática reversa estabeleceu que subsistemas fracos da aritmética de segunda ordem são suficientes para formalizar quase toda a matemática de graduação. Na aritmética de segunda ordem, todos os objetos podem ser representados como números naturais ou conjuntos de números naturais. Por exemplo, para provar teoremas sobre números reais, os números reais podem ser representados como sequências de Cauchy de números racionais , cada um dos quais pode ser representado como um conjunto de números naturais.

Os sistemas de axiomas mais freqüentemente considerados na matemática reversa são definidos usando esquemas de axiomas chamados de esquemas de compreensão . Tal esquema afirma que existe qualquer conjunto de números naturais definíveis por uma fórmula de uma dada complexidade. Nesse contexto, a complexidade das fórmulas é medida por meio da hierarquia aritmética e da hierarquia analítica .

A razão pela qual a matemática reversa não é realizada usando a teoria dos conjuntos como sistema de base é que a linguagem da teoria dos conjuntos é muito expressiva. Conjuntos extremamente complexos de números naturais podem ser definidos por fórmulas simples na linguagem da teoria dos conjuntos (que podem ser quantificados em conjuntos arbitrários). No contexto da aritmética de segunda ordem, resultados como o teorema de Post estabelecem uma ligação estreita entre a complexidade de uma fórmula e a (não) computabilidade do conjunto que ela define.

Outro efeito do uso da aritmética de segunda ordem é a necessidade de restringir os teoremas matemáticos gerais às formas que podem ser expressas na aritmética. Por exemplo, a aritmética de segunda ordem pode expressar o princípio "Todo espaço vetorial contável tem uma base", mas não pode expressar o princípio "Todo espaço vetorial tem uma base". Em termos práticos, isso significa que os teoremas de álgebra e combinatória são restritos a estruturas contáveis, enquanto os teoremas de análise e topologia são restritos a espaços separáveis . Muitos princípios que implicam o axioma da escolha em sua forma geral (como "Todo espaço vetorial tem uma base") tornam-se prováveis ​​em subsistemas fracos da aritmética de segunda ordem quando são restritos. Por exemplo, "todo campo tem um fechamento algébrico" não é demonstrável na teoria dos conjuntos ZF, mas a forma restrita "todo campo contável tem um fechamento algébrico" é demonstrável em RCA ₀ , o sistema mais fraco normalmente empregado na matemática reversa.

Uso de aritmética de ordem superior

Uma recente vertente de pesquisa matemática reversa de ordem superior , iniciada por Ulrich Kohlenbach , concentra-se em subsistemas de aritmética de ordem superior . Devido à linguagem mais rica da aritmética de ordem superior, o uso de representações (também conhecidas como 'códigos') comuns na aritmética de segunda ordem é bastante reduzido. Por exemplo, uma função contínua no espaço Cantor é apenas uma função que mapeia sequências binárias em sequências binárias, e que também satisfaz a definição usual de continuidade 'épsilon delta'.

A matemática reversa de ordem superior inclui versões de ordem superior de esquemas de compreensão (de segunda ordem). Tal axioma de ordem superior afirma a existência de um funcional que decide a verdade ou falsidade das fórmulas de uma dada complexidade. Nesse contexto, a complexidade das fórmulas também é medida por meio da hierarquia aritmética e da hierarquia analítica . As contrapartes de ordem superior dos principais subsistemas da aritmética de segunda ordem geralmente provam as mesmas sentenças de segunda ordem (ou um grande subconjunto) que os sistemas originais de segunda ordem. Por exemplo, a teoria básica da matemática reversa de ordem superior, chamada RCA^ω
₀, prova as mesmas sentenças que RCA ₀ , até o idioma.

Conforme observado no parágrafo anterior, os axiomas de compreensão de segunda ordem generalizam-se facilmente para a estrutura de ordem superior. No entanto, teoremas que expressam a compactação de espaços básicos se comportam de maneira bastante diferente na aritmética de segunda e de ordem superior: por um lado, quando restrito a coberturas contáveis ​​/ a linguagem da aritmética de segunda ordem, a compactação do intervalo de unidade é demonstrável em WKL ₀ da próxima seção. Por outro lado, dadas as incontáveis ​​capas / linguagem da aritmética de ordem superior, a compactação do intervalo unitário só pode ser demonstrada a partir da aritmética de segunda ordem (completa). Outros lemas de cobertura (por exemplo, devido a Lindelöf , Vitali , Besicovitch , etc.) exibem o mesmo comportamento, e muitas propriedades básicas da integral de calibre são equivalentes à compactação do espaço subjacente.

Os cinco grandes subsistemas da aritmética de segunda ordem

A aritmética de segunda ordem é uma teoria formal dos números naturais e conjuntos de números naturais. Muitos objetos matemáticos, como anéis contáveis , grupos e campos , bem como pontos em espaços poloneses efetivos , podem ser representados como conjuntos de números naturais, e o módulo dessa representação pode ser estudado em aritmética de segunda ordem.

A matemática reversa faz uso de vários subsistemas da aritmética de segunda ordem. Um teorema matemático reverso típico mostra que um teorema matemático particular T é equivalente a um subsistema particular S da aritmética de segunda ordem sobre um subsistema B mais fraco . Este sistema B mais fraco é conhecido como o sistema de base para o resultado; a fim de que a matemática reversa resultar de ter significado, este sistema não deve-se ser capaz de provar o teorema matemático T .

Simpson (2009) descreve cinco subsistemas particulares da aritmética de segunda ordem, que ele chama de Big Five , que ocorrem com frequência na matemática reversa. Em ordem crescente de resistência, esses sistemas são nomeados pelos inicialismos RCA ₀ , WKL ₀ , ACA ₀ , ATR ₀ e Π¹
₁-CA ₀ .

A tabela a seguir resume os "cinco grandes" sistemas e lista os sistemas correspondentes em aritmética de ordem superior. O último geralmente prova as mesmas sentenças de segunda ordem (ou um grande subconjunto) que os sistemas originais de segunda ordem.

Subsistema	Apoia	Ordinal	Corresponde aproximadamente a	Comentários	Contraparte de ordem superior
RCA 0	Axioma de compreensão recursiva	ω ω	Matemática construtiva ( bispo )	A teoria básica	RCAω 0; prova as mesmas sentenças de segunda ordem que RCA 0
WKL 0	Lema de Kőnig fraco	ω ω	Reducionismo finito ( Hilbert )	Conservador sobre PRA (resp. RCA 0 ) para Π0 2(resp. Π1 1) frases	Ventilador funcional; calcula o módulo de continuidade uniforme ativado para funções contínuas ${\ displaystyle 2 ^ {\ mathbb {N}}}$
ACA 0	Axioma da compreensão aritmética	ε 0	Predicativismo ( Weyl , Feferman )	Conservador em relação à aritmética de Peano para sentenças aritméticas	O funcional 'salto de Turing' expressa a existência de uma função descontínua em${\ displaystyle \ existe ^ {2}}$${\ displaystyle \ mathbb {R}}$
ATR 0	Recursão transfinita aritmética	Γ 0	Reducionismo predicativo (Friedman, Simpson)	Conservador em relação ao IR do sistema de Feferman para Π1 1 frases	As saídas funcionais de 'recursão transfinita' que o conjunto alegou existir pelo ATR 0 .
Π1 1-CA 0	Π1 1 axioma de compreensão	Ψ 0 (Ω ω )	Impredicativismo		O funcional Suslin decide Π${\ displaystyle S ^ {2}}$1 1-fórmulas (restritas a parâmetros de segunda ordem).

O subscrito ₀ nesses nomes significa que o esquema de indução foi restringido do esquema de indução de segunda ordem completo. Por exemplo, ACA ₀ inclui o axioma indução (0 ∈  X  ∧ ∀ n ( n  ∈  X  →  n  + 1 ∈  X )) → ∀ n  n  ∈ X . Isso, juntamente com o axioma de compreensão total da aritmética de segunda ordem, implica o esquema de indução de segunda ordem completo dado pelo fechamento universal de ( φ (0) ∧ ∀ n ( φ ( n ) → φ ( n +1))) → ∀ n φ ( n ) para qualquer fórmula de segunda ordem φ . No entanto, ACA ₀ não tem o axioma de compreensão total, e o subscrito ₀ é um lembrete de que ele também não tem o esquema de indução de segunda ordem completo. Esta restrição é importante: sistemas com indução restrita têm ordinais teóricos de prova significativamente mais baixos do que sistemas com o esquema de indução de segunda ordem completo.

O sistema básico RCA ₀

RCA ₀ é o fragmento da aritmética de segunda ordem cujos axiomas são os axiomas da aritmética de Robinson , indução para Σ⁰
₁fórmulas e compreensão para Δ⁰
₁ fórmulas.

O subsistema RCA ₀ é o mais comumente usado como sistema básico para matemática reversa. As iniciais "RCA" significam "axioma de compreensão recursiva", onde "recursivo" significa "computável", como na função recursiva . Este nome é usado porque RCA ₀ corresponde informalmente a "matemática computável". Em particular, qualquer conjunto de números naturais cuja existência pode ser comprovada em RCA ₀ é computável e, portanto, qualquer teorema que implique que conjuntos não computáveis ​​existem não pode ser provado em RCA ₀ . Nesse sentido, RCA ₀ é um sistema construtivo, embora não atenda aos requisitos do programa de construtivismo, porque é uma teoria na lógica clássica que inclui a lei do meio excluído .

Apesar de sua aparente fraqueza (de não provar que nenhum conjunto não computável existe), RCA ₀ é suficiente para provar uma série de teoremas clássicos que, portanto, requerem apenas uma força lógica mínima. Esses teoremas estão, em certo sentido, abaixo do alcance do empreendimento da matemática reversa porque já podem ser demonstrados no sistema de base. Os teoremas clássicos demonstráveis ​​em RCA ₀ incluem:

• Propriedades básicas dos números naturais, inteiros e números racionais (por exemplo, que os últimos formam um campo ordenado ).
• Propriedades básicas dos números reais (os números reais são um campo ordenado de Arquimedes ; qualquer sequência aninhada de intervalos fechados cujos comprimentos tendem a zero tem um único ponto em sua interseção; os números reais não são contáveis).
• O teorema da categoria de Baire para um espaço métrico separável completo (a condição de separabilidade é necessária para definir o teorema na linguagem da aritmética de segunda ordem).
• O teorema do valor intermediário em funções reais contínuas.
• O teorema de Banach – Steinhaus para uma sequência de operadores lineares contínuos em espaços de Banach separáveis.
• Uma versão fraca do teorema da completude de Gödel (para um conjunto de sentenças, em uma linguagem contável, que já está fechado por conseqüência).
• A existência de um fechamento algébrico para um campo contável (mas não sua unicidade).
• A existência e singularidade do fechamento real de um campo ordenado contável.

A parte de primeira ordem do RCA ₀ (os teoremas do sistema que não envolvem nenhum conjunto de variáveis) é o conjunto de teoremas da aritmética de Peano de primeira ordem com indução limitada a Σ⁰
₁fórmulas. É comprovadamente consistente, assim como RCA ₀ , na aritmética de Peano de primeira ordem completa.

Lema de Kőnig fraco WKL ₀

O subsistema WKL ₀ consiste em RCA ₀ mais uma forma fraca do lema de Kőnig , a saber, a afirmação de que cada subárvore infinita da árvore binária completa (a árvore de todas as sequências finitas de 0 e 1) tem um caminho infinito. Essa proposição, que é conhecida como lema de Kőnig fraco , é fácil de declarar na linguagem da aritmética de segunda ordem. WKL ₀ também pode ser definido como o princípio de Σ⁰
₁ separação (dado dois Σ⁰
₁fórmulas de uma variável livre n que são exclusivas, há uma classe contendo todos os n satisfazendo um e nenhum n satisfazendo o outro).

A seguinte observação sobre a terminologia está em ordem. O termo “lema de Kőnig fraco” refere-se à frase que diz que qualquer subárvore infinita da árvore binária tem um caminho infinito. Quando este axioma é adicionado ao RCA ₀ , o subsistema resultante é denominado WKL ₀ . Uma distinção semelhante entre axiomas específicos, por um lado, e subsistemas incluindo os axiomas básicos e indução, por outro lado, é feita para os subsistemas mais fortes descritos abaixo.

Em certo sentido, o lema de Kőnig fraco é uma forma de axioma de escolha (embora, como afirmado, possa ser provado na teoria dos conjuntos clássica de Zermelo – Fraenkel sem o axioma de escolha). Não é construtivamente válido em alguns sentidos da palavra construtivo.

Para mostrar que WKL ₀ é realmente mais forte do que (não demonstrável em) RCA ₀ , é suficiente exibir um teorema de WKL ₀ que implica que existem conjuntos não-computáveis. Isso não é difícil; WKL ₀ implica a existência de conjuntos de separação para conjuntos recursivamente enumeráveis ​​efetivamente inseparáveis.

Acontece que RCA ₀ e WKL ₀ têm a mesma parte de primeira ordem, o que significa que provam as mesmas sentenças de primeira ordem. WKL ₀ pode provar um bom número de resultados matemáticos clássicos que não seguem de RCA ₀ , entretanto. Esses resultados não são expressos como declarações de primeira ordem, mas podem ser expressos como declarações de segunda ordem.

Os seguintes resultados são equivalentes ao lema de Kőnig fraco e, portanto, a WKL ₀ sobre RCA ₀ :

• O teorema de Heine-Borel para o intervalo real unitário fechado, no seguinte sentido: toda cobertura por uma sequência de intervalos abertos tem uma subcobertura finita.
• O teorema de Heine-Borel para espaços métricos separáveis ​​totalmente delimitados completos (onde a cobertura é por uma sequência de bolas abertas).
• Uma função real contínua no intervalo de unidade fechado (ou em qualquer espaço métrico separável compacto, como acima) é limitada (ou: limitada e atinge seus limites).
• Uma função real contínua no intervalo de unidade fechada pode ser uniformemente aproximada por polinômios (com coeficientes racionais).
• Uma função real contínua no intervalo da unidade fechada é uniformemente contínua.
• Uma função real contínua no intervalo de unidade fechada é Riemann integrável.
• O Brouwer teorema ponto fixo (para funções contínuas sobre um produto finito de cópias do intervalo unidade fechada).
• O teorema separável de Hahn-Banach na forma: uma forma linear limitada em um subespaço de um espaço separável de Banach se estende a uma forma linear limitada em todo o espaço.
• A curva teorema de Jordan
• Teorema da completude de Gödel (para uma linguagem contável).
• Determinação para jogos abertos (ou mesmo clopen) em {0,1} de comprimento ω.
• Todo anel comutativo contável tem um ideal primário .
• Cada campo contável formalmente real pode ser solicitado.
• Singularidade do fechamento algébrico (para um campo contável).

Compreensão aritmética ACA ₀

ACA ₀ é RCA ₀ mais o esquema de compreensão para fórmulas aritméticas (que às vezes é chamado de "axioma de compreensão aritmética"). Ou seja, ACA ₀ nos permite formar o conjunto de números naturais que satisfazem uma fórmula aritmética arbitrária (uma sem variáveis ​​de conjunto limitadas, embora possivelmente contendo parâmetros de conjunto). Na verdade, basta adicionar ao RCA ₀ o esquema de compreensão das fórmulas Σ ₁ para obter a compreensão aritmética completa.

A parte de primeira ordem do ACA ₀ é exatamente a aritmética de Peano de primeira ordem; ACA ₀ é uma extensão conservadora da aritmética de Peano de primeira ordem. Os dois sistemas são comprovadamente (em um sistema fraco) equiconsistentes. ACA ₀ pode ser pensado como uma estrutura da matemática predicativa , embora existam teoremas prováveis ​​de forma predicativa que não são prováveis ​​em ACA ₀ . A maioria dos resultados fundamentais sobre os números naturais, e muitos outros teoremas matemáticos, podem ser provados neste sistema.

Uma maneira de ver que ACA ₀ é mais forte do que WKL ₀ é exibir um modelo de WKL ₀ que não contém todos os conjuntos aritméticos. Na verdade, é possível construir um modelo de WKL ₀ consistindo inteiramente em conjuntos baixos usando o teorema de base baixa , uma vez que conjuntos baixos em relação aos conjuntos baixos são baixos.

As seguintes afirmações são equivalentes a ACA ₀ sobre RCA ₀ :

• A completude sequencial dos números reais (cada sequência crescente limitada de números reais tem um limite).
• O teorema de Bolzano-Weierstrass .
• Teorema de Ascoli : toda sequência equicontínua limitada de funções reais no intervalo de unidade tem uma subsequência uniformemente convergente.
• Cada anel comutativo contável tem um ideal máximo .
• Cada espaço vetorial contável sobre os racionais (ou sobre qualquer campo contável) tem uma base.
• Cada campo contável tem uma base de transcendência .
• Lema de Kőnig (para árvores arbitrariamente ramificadas, ao contrário da versão fraca descrita acima).
• Vários teoremas em combinatória, como certas formas do teorema de Ramsey .

ATR _{0 de} recursão aritmética transfinida

O sistema ATR ₀ adiciona ao ACA ₀ um axioma que afirma, informalmente, que qualquer funcional aritmético (ou seja, qualquer fórmula aritmética com uma variável de número livre n e uma variável de classe livre X , visto como o operador levando X ao conjunto de n satisfazendo o fórmula) pode ser iterado transfinitamente ao longo de qualquer ordenação de poço contável começando com qualquer conjunto. ATR ₀ é equivalente em ACA ₀ ao princípio de Σ¹
₁separação. ATR ₀ é impredicativo e tem o ordinal da teoria da prova , o supremo daquele dos sistemas predicativos. ${\ displaystyle \ Gamma _ {0}}$

ATR ₀ prova a consistência de ACA ₀ e, portanto, pelo teorema de Gödel , é estritamente mais forte.

As seguintes afirmações são equivalentes a ATR ₀ sobre RCA ₀ :

• Quaisquer duas ordenações de poços contáveis ​​são comparáveis. Ou seja, eles são isomórficos ou um é isomórfico a um segmento inicial adequado do outro.
• Teorema de Ulm para grupos Abelianos reduzidos contáveis.
• O teorema do conjunto perfeito , que afirma que todo subconjunto fechado incontável de um espaço métrico separável completo contém um conjunto fechado perfeito.
• Teorema de separação de Lusin (essencialmente Σ¹
  ₁ separação).
• Determinação para conjuntos abertos no espaço Baire .

Π¹
₁ compreensão Π¹
₁-CA ₀

Π¹
₁-CA ₀ é mais forte do que a recursão transfinita aritmética e é totalmente impredicativa. Consiste em RCA ₀ mais o esquema de compreensão para Π¹
₁ fórmulas.

Em certo sentido, Π¹
₁A compreensão -CA ₀ é para recursão transfinita aritmética (Σ¹
₁separação), pois ACA ₀ é para o lema de Kőnig fraco (Σ⁰
₁separação). É equivalente a várias declarações da teoria dos conjuntos descritivos cujas provas fazem uso de argumentos fortemente impredicativos; essa equivalência mostra que esses argumentos impredicativos não podem ser removidos.

Os seguintes teoremas são equivalentes a Π¹
₁-CA ₀ sobre RCA ₀ :

• O teorema de Cantor-Bendixson (cada conjunto fechado de reais é a união de um conjunto perfeito e um conjunto contável).
• Cada grupo abeliano contável é a soma direta de um grupo divisível e um grupo reduzido.

Sistemas adicionais

• Sistemas mais fracos do que a compreensão recursiva podem ser definidos. O fraco sistema RCA^*
  ₀consiste na função aritmética elementar EFA (os axiomas básicos mais Δ⁰
  ₀ indução na linguagem enriquecida com uma operação exponencial) mais Δ⁰
  ₁compreensão. Sobre RCA^*
  ₀, compreensão recursiva conforme definido anteriormente (ou seja, com Σ⁰
  ₁indução) é equivalente à afirmação de que um polinômio (sobre um campo contável) tem apenas muitas raízes finitas e ao teorema de classificação para grupos Abelianos finitamente gerados. O sistema RCA^*
  ₀tem o mesmo ordinal teórico de prova ω ³ que EFA e é conservador sobre EFA para Π⁰
  ₂ frases.
• Fraco Fraco O Lema de Kőnig é a afirmação de que uma subárvore da árvore binária infinita sem caminhos infinitos tem uma proporção de folhas de comprimento n assintoticamente desaparecendo (com uma estimativa uniforme de quantas folhas de comprimento n existem). Uma formulação equivalente é que qualquer subconjunto de espaço Cantor que tenha medida positiva é não vazio (isso não pode ser provado em RCA ₀ ). WWKL ₀ é obtido juntando este axioma a RCA ₀ . É equivalente à afirmação de que se o intervalo real unitário é coberto por uma sequência de intervalos, a soma de seus comprimentos é pelo menos um. A teoria do modelo de WWKL ₀ está intimamente ligada à teoria das sequências algorítmicas aleatórias . Em particular, um modelo-ω de RCA ₀ satisfaz lema fraco fraco de Konig se e somente se para cada conjunto X tem um conjunto Y que é 1-aleatório em relação ao X .
• DNR (abreviação de "diagonalmente não recursiva") adiciona ao RCA ₀ um axioma que afirma a existência de uma função diagonalmente não recursiva em relação a cada conjunto. Ou seja, DNR afirma que, para qualquer conjunto A , existe uma função total de f tal que para todo e do e th função recursiva parcial com a Oracle A não é igual a f . DNR é estritamente mais fraco do que WWKL (Lempp et al. , 2004).
• Δ¹
  ₁-compreensão é em certos aspectos análoga à recursão transfinita aritmética como a compreensão recursiva é ao lema fraco de Kőnig. Possui os conjuntos hiperaritméticos como modelo ω mínimo. A recursão transfinita aritmética prova Δ¹
  ₁-compreensão, mas não o contrário.
• Σ¹
  ₁- escolha é a afirmação de que se η ( n , X ) é um Σ¹
  ₁fórmula tal que para cada n existe um X que satisfaz η, então existe uma sequência de conjuntos X _n tal que η ( n , X _n ) vale para cada n . Σ¹
  ₁-choice também tem os conjuntos hiperaritméticos como modelo ω mínimo. A recursão transfinita aritmética prova Σ¹
  ₁-escolher, mas não o contrário.
• HBU (abreviação de "incontáveis ​​Heine-Borel") expressa a compactação (tampa aberta) do intervalo da unidade, envolvendo incontáveis ​​tampas . O último aspecto do HBU o torna expressável apenas na linguagem da aritmética de terceira ordem . O teorema de Cousin (1895) implica HBU, e esses teoremas usam a mesma noção de cobertura devido a Cousin e Lindelöf . HBU é difícil de provar: em termos da hierarquia usual de axiomas de compreensão, uma prova de HBU requer aritmética de segunda ordem completa.
• O teorema de Ramsey para gráficos infinitos não se enquadra em nenhum dos cinco grandes subsistemas e existem muitas outras variantes mais fracas com intensidades de prova variadas.

modelos ω e modelos β

O ω no modelo ω representa o conjunto de inteiros não negativos (ou ordinais finitos). Um modelo ω é um modelo para um fragmento da aritmética de segunda ordem cuja parte de primeira ordem é o modelo padrão da aritmética de Peano, mas cuja parte de segunda ordem pode não ser padrão. Mais precisamente, um modelo ω é dado por uma escolha S ⊆2 ^ω de subconjuntos de ω. As variáveis de primeira ordem são interpretadas da maneira usual como elementos de ω, e +, × têm os seus significados usuais, enquanto as variáveis de segunda ordem são interpretados como elementos de S . Existe um modelo ω padrão em que apenas se considera que S consiste em todos os subconjuntos de inteiros. No entanto, também existem outros modelos ω; por exemplo, RCA ₀ tem um modelo mínimo ω onde S consiste nos subconjuntos recursivos de ω.

Um modelo β é um modelo ω que é equivalente ao modelo ω padrão para Π¹
₁ e Σ¹
₁ sentenças (com parâmetros).

Modelos não-ω também são úteis, especialmente nas provas de teoremas de conservação.

Veja também

• Expressão de forma fechada § Conversão de formas numéricas
• Princípios de indução, limitação e número mínimo
• Otimização matemática
• Análise ordinal
• Regressão simbólica

Notas

Referências

• Ambos-Spies, K .; Kjos-Hanssen, B .; Lempp, S .; Slaman, TA (2004), "Comparing DNR and WWKL", Journal of Symbolic Logic , 69 (4): 1089, arXiv : 1408.2281 , doi : 10.2178 / jsl / 1102022212 .
• Friedman, Harvey (1975), "Alguns sistemas de aritmética de segunda ordem e seu uso", Proceedings of the International Congress of Mathematicians (Vancouver, BC, 1974), Vol. 1 , Canad. Matemática. Congress, Montreal, Que., Pp. 235-242, MR  0429508
• Friedman, Harvey (1976), Baldwin, John; Martin, DA ; Soare, RI ; Tait, WW (eds.), "Sistemas de aritmética de segunda ordem com indução restrito, I, II", Encontro da Associação para simbólica Lógica, The Journal of Lógica simbólica , 41 (2): 557-559, DOI : 10,2307 / 2272259 , JSTOR  2272259
• Hirschfeldt, Denis R. (2014), Slicing the Truth , Lecture Notes Series do Institute for Mathematical Sciences, National University of Singapore, 28 , World Scientific
• Hunter, James (2008), Topologia reversa (PDF) (tese de doutorado), University of Wisconsin – Madison
• Kohlenbach, Ulrich (2005), "Higher order reverse mathematics" , em Simpson, Stephen G (ed.), Higher Order Reverse Mathematics, Reverse Mathematics 2001 (PDF) , Lecture notes in Logic, Cambridge University Press , pp. 281–295 , CiteSeerX  10.1.1.643.551 , doi : 10.1017 / 9781316755846.018 , ISBN 9781316755846
• Normann, Dag; Sanders, Sam (2018), "On the mathematical and foundational meaning of the uncountable", Journal of Mathematical Logic , 19 : 1950001, arXiv : 1711.08939 , doi : 10.1142 / S0219061319500016
• Simpson, Stephen G. (2009), Subsystems of second-order arithmetic , Perspectives in Logic (2ª ed.), Cambridge University Press , doi : 10.1017 / CBO9780511581007 , ISBN 978-0-521-88439-6, MR  2517689
• Stillwell, John (2018), Reverse Mathematics, provas de dentro para fora , Princeton University Press , ISBN 978-0-691-17717-5
• Solomon, Reed (1999), "Grupos ordenados: um estudo de caso em matemática reversa", The Bulletin of Symbolic Logic , 5 (1): 45–58, CiteSeerX  10.1.1.364.9553 , doi : 10.2307 / 421140 , ISSN  1079- 8986 , JSTOR  421140 , MR  1681895

links externos

• Página inicial de Harvey Friedman
• Página inicial de Stephen G. Simpson
• Zoológico de matemática reversa