Aritmética de segunda ordem - Second-order arithmetic

Na lógica matemática , a aritmética de segunda ordem é uma coleção de sistemas axiomáticos que formalizam os números naturais e seus subconjuntos. É uma alternativa à teoria axiomática dos conjuntos como base para grande parte, mas não toda, da matemática.

Um precursor da aritmética de segunda ordem que envolve parâmetros de terceira ordem foi introduzido por David Hilbert e Paul Bernays em seu livro Grundlagen der Mathematik . A axiomatização padrão da aritmética de segunda ordem é denotada por Z 2 .

A aritmética de segunda ordem inclui, mas é significativamente mais forte do que a aritmética de Peano , sua contraparte de primeira ordem . Ao contrário da aritmética de Peano, a aritmética de segunda ordem permite a quantificação sobre conjuntos de números naturais, bem como os próprios números. Como os números reais podem ser representados como conjuntos ( infinitos ) de números naturais de maneiras bem conhecidas, e como a aritmética de segunda ordem permite a quantificação sobre esses conjuntos, é possível formalizar os números reais na aritmética de segunda ordem. Por esse motivo, a aritmética de segunda ordem às vezes é chamada de “ análise ” (Sieg 2013, p. 291).

A aritmética de segunda ordem também pode ser vista como uma versão fraca da teoria dos conjuntos em que cada elemento é um número natural ou um conjunto de números naturais. Embora seja muito mais fraca do que a teoria dos conjuntos de Zermelo-Fraenkel , a aritmética de segunda ordem pode provar essencialmente todos os resultados da matemática clássica expressáveis ​​em sua linguagem.

Um subsistema de aritmética de segunda ordem é uma teoria na linguagem da aritmética de segunda ordem, cada axioma da qual é um teorema da aritmética de segunda ordem completa (Z 2 ). Esses subsistemas são essenciais para reverter a matemática , um programa de pesquisa que investiga quanto da matemática clássica pode ser derivado em certos subsistemas fracos de intensidade variável. Grande parte da matemática básica pode ser formalizada nesses subsistemas fracos, alguns dos quais são definidos a seguir. A matemática reversa também esclarece a extensão e a maneira pela qual a matemática clássica não é construtiva .

Definição

Sintaxe

A linguagem da aritmética de segunda ordem é dividida em duas categorias . O primeiro tipo de termos e em variáveis particulares , geralmente denotadas por letras minúsculas, consiste em indivíduos , cuja interpretação pretendida é como números naturais. Os outros tipos de variáveis, também chamados de “variáveis ​​de conjunto”, “variáveis ​​de classe” ou mesmo “predicados” são geralmente denotados por letras maiúsculas. Eles se referem a classes / predicados / propriedades de indivíduos e, portanto, podem ser considerados conjuntos de números naturais. Tanto os indivíduos quanto as variáveis ​​definidas podem ser quantificados universal ou existencialmente. Uma fórmula sem variáveis ​​de conjunto limitadas (ou seja, sem quantificadores sobre variáveis ​​de conjunto) é chamada de aritmética . Uma fórmula aritmética pode ter variáveis ​​de conjunto livre e variáveis ​​individuais limitadas.

Os termos individuais são formados a partir da constante 0, da função unária S (a função sucessora ) e das operações binárias + e (adição e multiplicação). A função sucessora adiciona 1 à sua entrada. As relações = (igualdade) e <(comparação de números naturais) relacionam dois indivíduos, enquanto a relação ∈ (pertencimento) relaciona um indivíduo e um conjunto (ou classe). Assim, na notação, a linguagem da aritmética de segunda ordem é dada pela assinatura .

Por exemplo, é uma fórmula bem formada de aritmética de segunda ordem que é aritmética, tem uma variável de conjunto livre X e uma variável individual limitada n (mas nenhuma variável de conjunto limitada, como é exigido de uma fórmula aritmética) - o que é um fórmula bem formada que não é aritmética, tendo uma variável de conjunto limitada X e uma variável individual limitada n .

Semântica

Várias interpretações diferentes dos quantificadores são possíveis. Se a aritmética de segunda ordem for estudada usando a semântica completa da lógica de segunda ordem , os quantificadores de conjunto variam em todos os subconjuntos do intervalo das variáveis ​​numéricas. Se a aritmética de segunda ordem for formalizada usando a semântica da lógica de primeira ordem (semântica de Henkin), então qualquer modelo inclui um domínio para o intervalo das variáveis ​​do conjunto, e este domínio pode ser um subconjunto adequado do conjunto completo de poderes do domínio do número variáveis ​​(Shapiro 1991, pp. 74-75).

Axiomas

Básico

Os axiomas a seguir são conhecidos como axiomas básicos ou, às vezes, axiomas de Robinson. A teoria de primeira ordem resultante , conhecida como aritmética de Robinson , é essencialmente aritmética de Peano sem indução. O domínio do discurso para as variáveis ​​quantificadas são os números naturais , denotados coletivamente por N , e incluindo o membro distinto , denominado " zero ".

As funções primitivas são a função sucessora unária , denotada por prefixo , e duas operações binárias , adição e multiplicação , denotadas pelo infixo "+" e " ", respectivamente. Existe também uma relação binária primitiva chamada ordem , denotada pelo infixo "<".

Axiomas que regem a função sucessora e zero :

1. (“o sucessor de um número natural nunca é zero”)
2. ("a função sucessora é injetiva ")
3. (“todo número natural é zero ou um sucessor”)

Adição definida recursivamente :

4
5

Multiplicação definida recursivamente:

6
7

Axiomas que regem a relação de ordem "<":

8. (“nenhum número natural é menor que zero”)
9
10. (“todo número natural é zero ou maior que zero”)
11

Todos esses axiomas são afirmações de primeira ordem . Ou seja, todas as variáveis ​​variam sobre os números naturais e não sobre seus conjuntos , fato ainda mais forte do que o fato de serem aritméticos. Além disso, há apenas um quantificador existencial , no axioma 3. Os axiomas 1 e 2, juntamente com um esquema de axioma de indução, constituem a definição usual de N de Peano-Dedekind . Adicionar a esses axiomas qualquer tipo de esquema de axioma de indução torna redundantes os axiomas 3, 10 e 11.

Esquema de indução e compreensão

Se φ ( n ) é uma fórmula da aritmética de segunda ordem com uma variável de número livre n e possível outro número livre ou conjunto de variáveis ​​(escrito m e X ), o axioma de indução para φ é o axioma:

O esquema de indução de segunda ordem ( completo ) consiste em todas as instâncias deste axioma, sobre todas as fórmulas de segunda ordem.

Um exemplo particularmente importante do esquema de indução é quando φ é a fórmula “ ” expressando o fato de que n é um membro de X ( X sendo uma variável de conjunto livre): neste caso, o axioma de indução para φ é

Essa frase é chamada de axioma de indução de segunda ordem .

Se φ ( n ) é uma fórmula com uma variável livre n e possivelmente outras variáveis ​​livres, mas não a variável Z , o axioma de compreensão para φ é a fórmula

Este axioma torna possível formar o conjunto de números naturais que satisfazem φ ( n ). Existe uma restrição técnica de que a fórmula φ pode não conter a variável Z , caso contrário a fórmula levaria ao axioma da compreensão

,

o que é inconsistente. Essa convenção é assumida no restante deste artigo.

O sistema completo

A teoria formal da aritmética de segunda ordem (na linguagem da aritmética de segunda ordem) consiste nos axiomas básicos, o axioma de compreensão para cada fórmula φ (aritmética ou outra) e o axioma de indução de segunda ordem. Essa teoria é algumas vezes chamada de aritmética de segunda ordem completa para distingui-la de seus subsistemas, definidos abaixo. Como a semântica de segunda ordem completa implica que todos os conjuntos possíveis existem, os axiomas de compreensão podem ser considerados parte do sistema dedutivo quando essa semântica é empregada (Shapiro 1991, p. 66).

Modelos

Esta seção descreve a aritmética de segunda ordem com semântica de primeira ordem. Assim, um modelo da linguagem da aritmética de segunda ordem consiste em um conjunto M (que forma o intervalo de variáveis ​​individuais) junto com uma constante 0 (um elemento de M ), uma função S de M a M , duas operações binárias + e · Em M , uma relação binária <em M , e uma coleção D de subconjuntos de M , que é o intervalo das variáveis ​​do conjunto. A omissão de D produz um modelo da linguagem da aritmética de primeira ordem.

Quando D é o conjunto de potência completo de M , o modelo é chamado de modelo completo . O uso da semântica de segunda ordem completa é equivalente a limitar os modelos da aritmética de segunda ordem aos modelos completos. Na verdade, os axiomas da aritmética de segunda ordem têm apenas um modelo completo. Isso decorre do fato de que os axiomas da aritmética de Peano com o axioma de indução de segunda ordem têm apenas um modelo sob a semântica de segunda ordem.

Quando M é o conjunto usual de números naturais com suas operações usuais, é chamado de modelo ω . Nesse caso, o modelo pode ser identificado com D , sua coleção de conjuntos de naturais, pois esse conjunto é suficiente para determinar completamente um modelo ω.

O modelo completo exclusivo, que é o conjunto usual de números naturais com sua estrutura usual e todos os seus subconjuntos, é chamado de modelo pretendido ou padrão da aritmética de segunda ordem.

Funções definíveis

As funções de primeira ordem que são comprovadamente totais na aritmética de segunda ordem são precisamente as mesmas que aquelas representáveis ​​no sistema F (Girard e Taylor 1987, pp. 122-123). Quase equivalentemente, o sistema F é a teoria dos funcionais correspondentes à aritmética de segunda ordem de uma maneira paralela a como o sistema T de Gödel corresponde à aritmética de primeira ordem na interpretação da Dialética .

Subsistemas

Existem muitos subsistemas nomeados de aritmética de segunda ordem.

Um subscrito 0 no nome de um subsistema indica que ele inclui apenas uma parte restrita do esquema de indução de segunda ordem completo (Friedman 1976). Tal restrição reduz significativamente a força teórica da prova do sistema. Por exemplo, o sistema ACA 0 descrito abaixo é equiconsistente com a aritmética de Peano . A teoria correspondente ACA, consistindo em ACA 0 mais o esquema de indução de segunda ordem completo, é mais forte do que a aritmética de Peano.

Compreensão aritmética

Muitos dos subsistemas bem estudados estão relacionados às propriedades de fechamento dos modelos. Por exemplo, pode ser mostrado que todo modelo ω da aritmética de segunda ordem completa é fechado sob o salto de Turing , mas nem todo modelo ω fechado sob o salto de Turing é um modelo da aritmética de segunda ordem completa. O subsistema ACA 0 inclui axiomas suficientes para capturar a noção de fechamento sob o salto de Turing.

ACA 0 é definido como a teoria que consiste nos axiomas básicos, o esquema do axioma de compreensão aritmética (em outras palavras, o axioma de compreensão para cada fórmula aritmética φ) e o axioma de indução de segunda ordem comum. Seria equivalente a incluir todo o esquema do axioma de indução aritmética, em outras palavras, incluir o axioma de indução para cada fórmula aritmética φ.

Pode ser mostrado que uma coleção S de subconjuntos de ω determina um modelo ω de ACA 0 se e somente se S for fechado sob o salto de Turing, redutibilidade de Turing e junção de Turing (Simpson 2009, pp. 311-313).

O subscrito 0 em ACA 0 indica que nem todas as instâncias do esquema de axioma de indução estão incluídas neste subsistema. Isso não faz diferença para os modelos ω, que satisfazem automaticamente todas as instâncias do axioma de indução. É importante, no entanto, no estudo de modelos não ω. O sistema que consiste em ACA 0 mais indução para todas as fórmulas às vezes é chamado de ACA sem subscrito.

O sistema ACA 0 é uma extensão conservadora da aritmética de primeira ordem (ou axiomas de Peano de primeira ordem), definidos como os axiomas básicos, mais o esquema de axiomas de indução de primeira ordem (para todas as fórmulas φ envolvendo nenhuma variável de classe, ligada ou caso contrário), na linguagem da aritmética de primeira ordem (que não permite variáveis ​​de classe de forma alguma). Em particular, ele tem o mesmo ordinal da teoria da prova ε 0 que a aritmética de primeira ordem, devido ao esquema de indução limitado.

A hierarquia aritmética para fórmulas

Uma fórmula é chamada de aritmética limitada , ou Δ 0 0 , quando todos os seus quantificadores são da forma ∀ n < t ou ∃ n < t (onde n é a variável individual sendo quantificada e t é um termo individual), onde

apoia

e

apoia

.

Uma fórmula é chamada de Σ 0 1 (ou às vezes Σ 1 ), respectivamente Π 0 1 (ou às vezes Π 1 ) quando tem a forma ∃ m (φ), respectivamente ∀ m (φ) onde φ é uma fórmula aritmética limitada e m é uma variável individual (que é livre em φ). De forma mais geral, uma fórmula é chamada Σ 0 n , respectivamente Π 0 n quando é obtida pela adição de quantificadores individuais existenciais, respectivamente universais, a uma fórmula Π 0 n −1 , respectivamente Σ 0 n −1 (e Σ 0 0 e Π 0 0 são todos equivalentes a Δ 0 0 ). Por construção, todas essas fórmulas são aritméticas (nenhuma variável de classe é nunca vinculada) e, de fato, ao colocar a fórmula na forma prenex de Skolem, pode-se ver que toda fórmula aritmética é equivalente a uma fórmula Σ 0 n ou Π 0 n para todos grande o suficiente n .

Compreensão recursiva

O subsistema RCA 0 é um sistema mais fraco do que ACA 0 e é freqüentemente usado como sistema base na matemática reversa . Consiste em: os axiomas básicos, o esquema de indução Σ 0 1 e o esquema de compreensão Δ 0 1 . O primeiro termo é claro: o esquema de indução Σ 0 1 é o axioma de indução para toda fórmula Σ 0 1 φ. O termo “ compreensão de Δ 0 1 ” é mais complexo, porque não existe uma fórmula de Δ 0 1 . O esquema de compreensão Δ 0 1 , em vez disso, afirma o axioma de compreensão para cada fórmula Σ 0 1 que é equivalente a uma fórmula Π 0 1 . Este esquema inclui, para cada Σ 0 1 fórmula φ e cada Π 0 1 fórmula ψ, o axioma:

O conjunto de consequências de primeira ordem de RCA 0 é o mesmo do subsistema IΣ 1 da aritmética de Peano, no qual a indução é restrita a Σ 0 1 fórmulas. Por sua vez, IΣ 1 é conservador sobre a aritmética recursiva primitiva (PRA) para sentenças. Além disso, o ordinal da teoria da prova de é ω ω , o mesmo de PRA.

Pode-se ver que uma coleção S de subconjuntos de ω determina um modelo ω de RCA 0 se e somente se S for fechado sob redutibilidade de Turing e junção de Turing. Em particular, a coleção de todos os subconjuntos computáveis ​​de ω dá um modelo ω de RCA 0 . Esta é a motivação por trás do nome deste sistema - se for possível provar a existência de um conjunto usando RCA 0 , então o conjunto é recursivo (ou seja, computável).

Sistemas mais fracos

Às vezes, um sistema ainda mais fraco do que RCA 0 é desejado. Um tal sistema é definido da seguinte forma: deve-se primeiro aumentar a linguagem da aritmética com uma função exponencial (em sistemas mais fortes, o exponencial pode ser definido em termos de adição e multiplicação pelo truque usual, mas quando o sistema se torna muito fraco, isso não é possível) e os axiomas básicos pelos axiomas óbvios que definem a exponenciação indutivamente da multiplicação; então o sistema consiste nos axiomas básicos (enriquecidos), mais a compreensão de Δ 0 1 , mais a indução de Δ 0 0 .

Sistemas mais fortes

Sobre ACA 0 , cada fórmula da aritmética de segunda ordem é equivalente a uma fórmula Σ 1 n ou Π 1 n para todos os n grandes o suficiente . O sistema Π 1 1 -compreensão é o sistema que consiste nos axiomas básicos, mais o axioma de indução de segunda ordem comum e o axioma de compreensão para cada Π 1 1 fórmula φ. Isso é equivalente a Σ 1 1 -compreensão (por outro lado, Δ 1 1 -compreensão, definida analogamente à Δ 0 1 -compreensão, é mais fraca).

Determinação projetiva

A determinação projetiva é a afirmação de que todo jogo de informação perfeito para dois jogadores com lances inteiros, a duração do jogo ω e o conjunto de payoff projetivo são determinados, ou seja, um dos jogadores tem uma estratégia vencedora. (O primeiro jogador ganha o jogo se a jogada pertence ao conjunto de recompensas; caso contrário, o segundo jogador vence.) Um conjunto é projetivo iff (como um predicado) é expressável por uma fórmula na linguagem da aritmética de segunda ordem, permitindo números reais como parâmetros, de modo que a determinação projetiva pode ser expressa como um esquema na linguagem de Z 2 .

Muitas proposições naturais expressáveis ​​na linguagem da aritmética de segunda ordem são independentes de Z 2 e até de ZFC, mas são prováveis ​​de determinação projetiva. Os exemplos incluem propriedade de subconjunto perfeito coanalítico , mensurabilidade e a propriedade de Baire para conjuntos, uniformização , etc. Sobre uma teoria de base fraca (como RCA 0 ), a determinação projetiva implica compreensão e fornece uma teoria essencialmente completa da aritmética de segunda ordem - afirmações naturais na linguagem de Z 2 que são independentes de Z 2 com determinação projetiva são difíceis de encontrar (Woodin 2001).

ZFC + {há n cardinais de Woodin : n é um número natural} é conservador sobre Z 2 com determinação projetiva, ou seja, uma afirmação na linguagem da aritmética de segunda ordem pode ser demonstrada em Z 2 com determinação projetiva sse sua tradução para a linguagem da teoria dos conjuntos é demonstrável em ZFC + {há n cardeais de Woodin: n ∈N}.

Codificando matemática

A aritmética de segunda ordem formaliza diretamente os números naturais e conjuntos de números naturais. No entanto, é capaz de formalizar outros objetos matemáticos indiretamente por meio de técnicas de codificação, fato que foi percebido pela primeira vez por Weyl (Simpson 2009, p. 16). Os inteiros, números racionais e números reais podem ser formalizados no subsistema RCA 0 , junto com espaços métricos separáveis ​​completos e funções contínuas entre eles (Simpson 2009, Capítulo II).

O programa de pesquisa da matemática reversa usa essas formalizações da matemática na aritmética de segunda ordem para estudar os axiomas de existência de conjunto necessários para provar teoremas matemáticos (Simpson 2009, p. 32). Por exemplo, o teorema do valor intermediário para funções de reais para reais é demonstrável em RCA 0 (Simpson 2009, p. 87), enquanto o teorema de Bolzano - Weierstrass é equivalente a ACA 0 sobre RCA 0 (Simpson 2009, p. 34 )

A codificação mencionada funciona bem para funções contínuas e totais, como mostrado em (Kohlenbach 2002, Seção 4), assumindo uma teoria de base de ordem superior mais o lema de Koenig fraco . Como talvez esperado, no caso da topologia ou teoria da medida, a codificação não é sem problemas, como explorado em eg (Hunter, 2008) ou (Normann-Sanders, 2019). No entanto, mesmo a codificação de funções integráveis ​​de Riemann leva a problemas: como mostrado em (Normann-Sanders, 2020), os axiomas mínimos (compreensão) necessários para provar o teorema de convergência de Arzelà para a integral de Riemann são * muito * diferentes dependendo se se usa um segundo- códigos de pedido ou funções de terceira ordem.

Veja também

Referências

  • Burgess, JP (2005), Fixing Frege , Princeton University Press.
  • Buss, SR (1998), Manual da teoria da prova , Elsevier. ISBN  0-444-89840-9
  • Friedman, H. (1976), "Sistemas de aritmética de segunda ordem com indução restrita", I, II (Abstracts). Journal of Symbolic Logic , v. 41, pp. 557–559. JStor
  • Girard, L. e Taylor (1987), Proofs and Types , Cambridge University Press.
  • Hilbert, D. e Bernays, P. (1934), Grundlagen der Mathematik , Springer-Verlag. MR 0237246
  • Hunter, James, Higher order Reverse Topology , Dissertation, University of Madison-Wisconsin [1] .
  • Kohlenbach, U. , Fundamentos e usos matemáticos de tipos superiores , Reflexões sobre os fundamentos da matemática, Lect. Notes Log., Vol. 15, ASL, 2002, pp. 92-116.
  • Dag Normann e Sam Sanders, Representações na teoria da medida , arXiv: 1902.02756 , (2019).
  • Dag Normann e Sam Sanders, Sobre a incontabilidade de $ \ mathbb {R} $ , arxiv: [2] , (2020), pp. 37.
  • Sieg, W. (2013), Hilbert's Programs and Beyond , Oxford University Press.
  • Shapiro, S. (1991), Foundations without foundationalism , Oxford University Press. ISBN  0-19-825029-0
  • Simpson, SG (2009), Subsystems of second order aritmetic , 2nd edition, Perspectives in Logic, Cambridge University Press. ISBN  978-0-521-88439-6 MR 2517689
  • Takeuti, G. (1975) Teoria da prova ISBN  0-444-10492-5
  • Woodin, WH (2001), "The Continuum Hypothesis, Part I", Notices of the American Mathematical Society , v. 48 n. 6