Aritmética de segunda ordem

Na Lógica matemática, aritmética de segunda ordem é uma coleção de sistemas axiomáticos que formalizam os números naturais e seus subconjuntos. É uma alternativa para a teoria axiomática dos conjuntos como fundamentos, mas não tudo, da matemática. Foi introduzida por David Hilbert e Paul Bernays em seu livro Grundlagen der Mathematik. A axiomatização padrão da aritmética de segunda ordem é denotada Z₂.

Aritmética de segunda ordem inclui, mas é significativamente mais forte do que, a aritmética de Peano. Ao contrário da aritmética de Peano, aritmética de segunda ordem permite a quantificação sobre conjuntos de números, 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 dado que a aritmética de segunda ordem permite a quantificação sobre esses conjuntos, é possível formalizar os números reais em aritmética de segunda ordem. Por esta razão, a aritmética de segunda ordem é chamada algumas vezes de "análise".

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

Um subsistema de aritmética de segunda ordem é uma teoria na linguagem da aritmética de segunda ordem onde cada axioma é um teorema da aritmética de segunda ordem plena (Z₂). Esses subsistemas são essenciais para a matemática reversa, um programa de pesquisa que investiga o quanto a matemática clássica pode ser derivada em certos subsistemas fracos de intensidade variável. A maior parte do núcleo da matemática pode ser formalizada por esses subsistemas fracos, alguns dos quais são definidos a seguir. Matemática reversa também esclarece o âmbito e as modalidades em que a matemática clássica é não-construtiva.

Definição

Sintaxe

A linguagem da aritmética de segunda ordem é dividida em duas partes. A primeira parte de termos e variáveis, geralmente indicados por letras minúsculas, é composta por indivíduos, cuja interpretação pretendida é como números naturais. A outra parte de variáveis, chamadas "variáveis de ajuste", "variáveis de classe", ou mesmo "predicados" são normalmente indicados por letras maiúsculas. Eles se referem a classes/predicados/propriedades dos indivíduos, e por isso pode ser pensado como conjuntos de números naturais. Ambos os indivíduos e as variáveis definidas podem ser quantificadas universalmente ou existencialmente. Uma fórmula sem variáveis de conjuntos livres (ou seja, nenhum quantificador sobre variáveis de conjuntos) é chamado aritmético. Uma fórmula matemática pode ter conjuntos de variáveis livres e variáveis individuais limitadas.

Termos individuais são formados a partir da constante 0, a função unária S (função sucessor), e as operações binárias + e • (adição e multiplicação). A função sucessor adiciona 1 (=S0) para a entrada. As relações = (igualdade) e < (comparação dos números naturais) relacionam dois indivíduos, enquanto que a relação ∈ (pertence) relaciona um indivíduo e um conjunto (ou classe). Por exemplo, $\forall n(n\in X\rightarrow Sn\in X)$, é uma fórmula bem formada da aritmética de segunda ordem, tem um conjunto variável livre X e uma variável individual n (porém sem conjuntos finitos de variáveis, como é exigido em uma fórmula aritmética) enquanto $\exists X\forall n(n\in X\leftrightarrow n<SSSSSS0\cdot SSSSSSS0)$ é uma fórmula bem formada que não é aritmética com um conjunto de variáveis finitas X e uma variável individual finita 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 plena da lógica de segunda ordem, então os quantificadores sobre conjuntos variam sobre todos os subconjuntos de variáveis de núméros. Se a aritmética de segunda ordem for formalizada através da semântica da lógica de primeira ordem, então qualquer modelo inclui um domínio para o conjunto de variáveis, e esse domínio pode ser um subconjunto próprio do conjunto pleno do conjunto das partes do domínio de variáveis de n´umeros.

Embora a aritmética de segunda ordem tenha sido estudada inicialmente usando a semântica plena de segunda ordem, a grande maioria das pesquisas atuais trata a aritmética de segunda ordem no cálculo de predicados de primeira ordem. Isto é porque a teoria de modelos de subsistemas da aritmética de segunda ordem é mais interessante no seio da lógica de primeira ordem.

Axiomas

Básico

Os seguintes axiomas são conhecidos como os axiomas básicos, ou, por vezes, os axiomas de Robinson. A teoria de primeira ordem resultante, conhecida como aritmética de Robinson, é essencialmente a aritmética de Peano sem indução. O universo de discurso para as variáveis quantificadas são os números naturais, denotado coletivamente por N, e incluindo o membro destacado $\ 0$, chamado de "zero".

As funções primitivas são a função unária sucessor, denotada pelo prefixo $\ S$, e duas operações binárias, adição e multiplicação, denotadas pelos infixos "+" e "$\cdot$", respectivamente. Existe também uma relação binária chamada ordem, denotada pelo infixo "<".

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

1. $\forall m[Sm=0\rightarrow \bot ].$ (“o sucessor de um número natural nunca é zero”)

2. $\forall m\forall n[Sm=Sn\rightarrow m=n].$ (“a função sucessor é injetora”)

3. $\forall n[0=n\lor \exists m[Sm=n]].$ (“cada número natural é zero ou um sucessor”)

Adição definida recursivamente:

4. $\forall m[m+0=m].$

5. $\forall m\forall n[m+Sn=S(m+n)].$

Multiplicação definida recursivamente:

6. $\forall m[m\cdot 0=0].$

7. $\forall m\forall n[m\cdot Sn=(m\cdot n)+m].$

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

8. $\forall m[m<0\rightarrow \bot ].$ (“nenhum número natural é menor do que zero”)

9. $\forall m[m<Sn\leftrightarrow (m<n\lor m=n)].$

10. $\forall n[0=n\lor 0<n].$ (“todo número natural é zero ou maior do que zero”)

11. $\forall m\forall n[(Sm<n\lor Sm=n)\leftrightarrow m<n].$

Estes axiomas são todos enunciados de primeira ordem. Ou seja, todas as variáveis são definidas sobre os números naturais e não conjuntos do mesmo, um fato ainda mais forte do que ser aritmético. Além disso, há apenas um quantificador existencial, em axioma 3. Axiomas 1 e 2, juntamente com um esquema de axioma de indução compõem a definição Peano-Dedekind usual de N. Somando-se a estes axiomas qualquer tipo de esquema de axioma da indução torna redundante os axiomas 3, 10 e 11.

Indução e esquema de compreensão

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

$\forall m_{\bullet }\forall X_{\bullet }((\varphi (0)\land \forall n(\varphi (n)\rightarrow \varphi (Sn))\rightarrow \forall n\varphi (n))$

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

Um exemplo particularmente importante do regime de indução é quando φ é a fórmula "$n\in X$" expressar o fato de que n é um membro de X (X é um conjunto de variável livre): neste caso, o axioma de indução para φ é:

$\forall X((0\in X\land \forall n(n\in X\rightarrow Sn\in X))\rightarrow \forall n(n\in X))$

Esta sentença é chamada de axioma de indução de segunda ordem.

Voltando ao caso em que φ (n) é uma fórmula com um n variável livre e possivelmente outras variáveis livres, definimos o axioma compreensão para φ sendo:

$\forall m_{\bullet }\forall X_{\bullet }\exists Z\forall n(n\in Z\leftrightarrow \varphi (n))$

Essencialmente, isso nos permite formar o conjunto $Z=\{n|\varphi (n)\}$ dos números naturais satisfazendo φ (n). Não existe uma restrição técnica para que a fórmula φ não possa conter a variável Z, pois caso contrário a fórmula $n\not \in Z$ levaria ao axioma da compreensão :$\exists Z\forall n(n\in Z\leftrightarrow n\not \in Z)$ , o que é inconsistente. Esta 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) é composta pelos axiomas básicos, o axioma de compreensão para cada fórmula φ (aritmética ou não), e o axioma da indução de segunda ordem. Esta teoria é às vezes chamada de aritmética de segunda ordem completa para distingui-la de seus subsistemas, definidos abaixo. Semântica de segunda ordem elimina a necessidade para o axioma da compreensão, porque estas semânticas implicam que cada conjunto possível exista.

Na presença do esquema da compreensão sem restrições, o único axioma da indução de segunda ordem implica cada instância do regime de indução completa. Subsistemas que limitam a compreensão de alguma forma pode compensar essa limitação, incluindo parte do esquema de indução. Exemplos de tais sistemas são fornecidos abaixo.

Modelos da aritmética de segunda ordem

Vamos lembrar que nós vemos a aritmética de segunda ordem como uma teoria no cálculo de predicados de primeira ordem. Assim um modelo ${\mathcal {M}}$ da linguagem da aritmética de segunda ordem é constituído por um conjunto M (que forma o contradomínio de variáveis individuais), juntamente com uma constante 0 (um elemento de M), uma função S de M para 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 contradomínio das variáveis definidas. Ao omitir D obtemos um modelo da linguagem de primeira ordem aritmética. Quando D é o conjunto das partes de M, o modelo ${\mathcal {M}}$ é chamado modelo pleno. O uso da semantica de segunda ordem completa é equivalente a limitar os modelos de aritmética de segunda ordem a modelos plenos. De fato, os axiomas da aritmética de segunda ordem têm apenas um único modelo pleno. Isto segue do fato de que axiomas da aritmética de Peano com o axioma de indução de segunda ordem têm um único modelo pela semântica de segunda ordem. Quando M é um conjunto usual de números naturais com operações usuais, M é chamado de um modelo ω. Neste caso podemos identificar o modelo com D, sua coleção de conjuntos naturais, porque este conjunto é suficiente para determinar completamente um modelo ω. O único modelo ω pleno que é o conjunto usual de números naturais com sua estrutura usual e todos seus subconjuntos é chamado o modelo pretendido ou modelo padrão da aritmética de segunda ordem.

Funções definíveis da aritmética de segunda ordem

As funções de primeira ordem, que são totalmente comprovadas aritméticas de segunda ordem são precisamente as mesmas que foram representadas no sistema F (Girard et al., 1987, pp. 122–123). Quase de forma equivalente, sistema F é a teoria de funcionais correspondentes a aritmética de segunda ordem de uma forma paralela à forma como o sistema T de Gödel corresponde a aritmética de primeira ordem na interpretação Dialética.

Subsistemas da aritmética de segunda ordem

Artigo principal : matemática reversa Há muitos subsistemas chamados de aritmética de segunda ordem.

Um índice 0 em nome de um subsistema indica que só inclui uma porção restrita do regime de indução de segunda ordem completa (Friedman, 1976). Essa restrição diminui a força da prova teórica do sistema de forma significativa. Por exemplo, o sistema descrito abaixo ACA0 é equivalente com a aritmética de Peano. A teoria correspondente ACA, consistindo de ACA0 mais o esquema completo da indução de segunda ordem, é mais forte do que a aritmética de Peano.

Compreensão artitmética

Muitos dos subsistemas bem estudados estão relacionados com as propriedades de fecho de modelos. Por exemplo, pode-se mostrar que cada ω-modelo da aritmética de segunda ordem completa é fechada sob salto de Turing, mas nem todo modelo ω fechada sob o salto de Turing é um modelo da aritmética de segunda ordem completa. Podemos perguntar se existe um subsistema da aritmética de segunda ordem satisfeito por cada modelo ω que é fechado sob o salto de Turing e que satisfaz algumas outras, mais leves, condições de fechamento. O subsistema que acabamos de descrever é chamado $\mathrm {ACA} _{0}$.

$\mathrm {ACA} _{0}$ é definido como uma teoria que consiste nos axiomas básicos, o esquema do axioma da compreensão aritmética, em outras palavras, o axioma da compreensão para cada fórmula φ aritmética, e o axioma da indução de segunda ordem normal; novamente, nós também podemos optar por incluir o esquema do axioma da indução aritmética, em outras palavras, o axioma da indução para cada fórmula φ aritmética, sem fazer diferença.

Pode-se observar que uma coleção S de subconjuntos de ω determina um modelo de ω $\mathrm {ACA} _{0}$ se e somente se S é fechado sob o salto de Turing, redutibilidade de Turing, e a inicialização de Turing.

O subscrito 0 em $\mathrm {ACA} _{0}$ indica que não incluímos todas as instâncias do axioma da indução neste subsistema. Isso não faz diferença quando estudamos apenas para modelos ω, que satisfazem automaticamente a cada instância do axioma da indução. É de crucial importância, no entanto, quando estudamos os modelos que não são ω-modelos. O sistema consiste de $\mathrm {ACA} _{0}$ além da indução para todas as fórmulas é às vezes chamado $\mathrm {ACA}$.

O sistema $\mathrm {ACA} _{0}$ é uma extensão conservadora da aritmética de primeira ordem (ou axiomas de Peano de primeira ordem), definido como os axiomas básicos, mais o esquema de axioma de indução de primeira ordem (para todas as fórmulas φ envolvendo não variáveis de classe em tudo , vinculado ou não), na linguagem aritmética de primeira ordem(que não permite variáveis de classe em tudo). Em particular, tem as mesmas provas teóricas ε₀ como a aritmética de primeira ordem, devido ao esquema de indução limitado.

A hierarquia aritmética para fórmulas

Para definir um segundo subsistema, vamos precisar de um pouco mais de terminologia.

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

$\forall n<t(\cdots )$

significa

$\forall n(n<t\rightarrow \cdots )$

e

$\exists n<t(\cdots )$

significa

$\exists n(n<t\land \cdots )$.

Uma fórmula é chamada de Σ⁰₁ (ou, por vezes, Σ₁), respectivamente Π⁰₁(ou, por vezes, Π₁) quando a forma de ∃m_•(φ), respectivamente ∀m_•(φ onde φ é uma fórmula aritmética limitada e m é uma variável individual (que é livre em φ). De modo mais geral, uma fórmula é chamada Σ⁰_n, respectivamente Π⁰_n quando ele é obtido através da adição de existenciais, respectivamente, quantificadores universais individuais para um Π⁰_n−1, respectivamente Σ⁰_n−1 fórmula (e Σ⁰₀ e Π⁰₀ são todas equivalentes Δ⁰₀). Observe que, por construção todas essas fórmulas são aritmética (não variáveis de classe são sempre ligada) e, de fato, ao colocar a fórmula em forma prenex Skolem pode-se ver que cada fórmula aritmética é equivalente a uma fórmula Σ⁰_n ou Π⁰_n para todos suficientemente grande n .

Compreensão Recursiva

O subsistema $\mathrm {RCA} _{0}$ é um sistema ainda mais fraca do $\mathrm {ACA} _{0}$ que e é freqüentemente usado como o sistema básico em matemática reversa. É constituída por: os axiomas básicos, o esquema Σ⁰₁ indução, e o esquema de compreensão Δ⁰₁. O primeiro termo é claro: o esquema de indução Σ⁰₁ é o axioma de indução para cada Σ⁰₁ fórmula φ. O termo "compreensão Δ⁰₁" requer um pouco mais de explicação, no entanto: não há tal coisa como uma fórmula Δ⁰₁ (o significado pretendido é uma fórmula que seja Σ⁰₁ e Π⁰₁), mas em vez disso estão postulando o axioma de compreensão para cada Σ⁰₁ fórmula sujeita à condição de que é equivalente a uma fórmula Π⁰₁, em outras palavras, para cada Σ⁰₁ fórmula φ e cada Π⁰₁ fórmula ψ que postulamos.

$\forall m\forall X((\forall n(\varphi (n)\leftrightarrow \psi (n)))\rightarrow \exists Z\forall n(n\in Z\leftrightarrow \varphi (n)))$

O conjunto de consequências de primeira ordem de $\mathrm {RCA} _{0}$ é a mesma que os da IΣ₁ subsistema da aritmética de Peano em que a indução é restrita a Σ⁰₁ fórmulas. Por sua vez, IΣ₁ é conservador em relação à aritmética recursiva primitiva (PRA) para sentenças $\Pi _{2}^{0}$. Além disso, o ordinal prova teórica de $\mathrm {RCA} _{0}$ é ω^ω, a mesma que a do PRA. Pode-se observar que uma coleção S de subconjuntos de ω determina um modelo ω de se e somente se S é fechado sob a redutibilidade de Turing. Em particular, a coleção de todos os subconjuntos de ω computáveis dá um modelo ω de $\mathrm {RCA} _{0}$. Esta é a motivação por trás do nome deste sistema – se pode ser provada a existência de um conjunto usando $\mathrm {RCA} _{0}$ , então o conjunto é computável (ou seja recursivo).

Sistemas mais fracos

Às vezes, um sistema ainda mais fraca do que $\mathrm {RCA} _{0}$ é desejado. Um tal sistema é definida como se segue: um primeiro deve aumentar o idioma de aritmética com uma função exponencial (em sistemas mais fortes o exponencial pode ser definida em termos de adição e multiplicação pelo truque habitual, mas quando o sistema torna-se muito fraca isto não é mais possível) e os axiomas básicos por parte dos axiomas evidentes definem exponenciação indutivamente da multiplicação; em seguida, o sistema é composto pelos (enriquecidos) axiomas básicos, além de Δ⁰₁ compreensão mais indução de Δ⁰₀.

Sistemas mais fortes

Por mais que nós definimos Σ_n e Π_n (ou, mais precisamente, Σ⁰_n e Π⁰_n) fórmulas, podemos definir fórmulas Σ¹_n e Π¹_n da seguinte maneira: a fórmula Δ¹₀ (ou Σ¹₀ ou Π¹₀) é apenas uma fórmula aritmética e a fórmula Σ¹_n , respectivamente Π¹_n, é obtida pela adição de, respectivamente existenciais universais, quantificadores de classe em frente de um Π¹_n−1, respectivamente Σ¹_n−1.

Não é muito difícil ver que mais de um sistema não muito fraco, qualquer fórmula aritmética de segunda ordem é equivalente a uma fórmula Σ¹_n or Π¹_n para todo n suficientemente grande. O sistema Π¹₁-compreensão é o sistema que consiste nos axiomas básicos, além da indução axioma segunda ordem ordinário e o axioma compreensão para cada Π¹₁ fórmula φ. É um exercício fácil mostrar que isso é realmente equivalente a Σ¹₁-compreensão (por outro lado, Δ¹₁-compreensão, definida pelo mesmo truque como apresentado anteriormente para Δ⁰₁-compreensão, é realmente mais fraca).

Determinância Projetiva

Determinância Projetiva é a afirmação de que todo jogo perfeito de informações entre dois jogadores, com movimentos sendo inteiros, tamanho de jogo ω e um conjunto de payoffs projetivos é determinado, ou seja, um dos jogadores tem uma estratégia vencedora. (O primeiro jogador ganha o jogo se a jogada pertence ao conjunto de payoffs; de outra forma, o segundo jogador ganha). Um conjunto é projetivo se e somente se (como um predicado) ele é expressível por uma fórmula na linguagem da aritmética de segunda ordem, permitindo números reais como parâmetros, assim a determinância projetiva é expressível como um esquema na linguagem de Z₂

Muitar proposições naturais expressíveis na linguagem da aritmética de segunda ordem são independentes de Z₂ e ainda ZFC, mas podem ser provadas pela determinância projetiva. Exemplos incluem a coanalítica propriedade do conjunto perfeito, mensurabilidade e a Teorema da categoria de Baire para os conjuntos $\Sigma _{2}^{1}$, uniformização $\Pi _{3}^{1}$, etc. Sobre uma fraca base teórica (assim como RCA₀), determinância projetiva implica compreensão e provê uma teoria completa da aritmética de segunda ordem — Sentenças naturais na linguagem de Z₂ que são independentes de Z₂ com determinância projetiva são difíceis de encontrar.

ZFC + {onde existe cardinais Woddin n: n é um número natural} é uma conservação sobre Z₂ com determinância projetiva, que é uma declaração na linguagem da aritmética de segunda ordem que é provável em Z₂ com determinância projetiva se e somente se ele é uma interpretação na linguagem da teoria dos conjuntos que é provável em ZFC + {onde existe cardinais Woddin n n∈N}.

Codificando matemática na aritmética de segunda ordem

A aritmética de segunda ordem nos permite falar diretamente (sem codificar) de números naturais e conjuntos de números naturais. Pares de números naturais podem ser codificados da maneira usual como números naturais, então inteiros arbitrários ou números racionais são os habitantes de primeira-classe da mesma forma que números naturais. Funções entre esses conjuntos podem ser codificadas como conjuntos de pares, e portanto, como subconjuntos dos números naturais, sem dificuldade. Números reais podem ser definidos como sequências de cauchy de números racionais, mas por razões técnicas não discutidas aqui, é preferível (no axioma fraco de sistemas acima) constranger a taxa de convergência (ou seja, dizer que a distância entre o n-ésimo e (n+1)-ésimo termo seja menor que 2⁻ⁿ). Esses sistemas não podem se referir à funções reais, ou subconjuntos dos reais. Não obstante, funções contínuas reais são legítimos objetos de estudo, desde que elas são definidas pelos seus valores nos racionais. Além disso, um truque relacionado faz isso se possível se referir à subconjuntos abertos dos reais. Mesmo o Conjunto de Borel dos reais podem ser codificados na linguagem da aritmética de segunda ordem, embora seja um pouco complicado fazê-lo.

Ver também

• Teorema de Paris-Harrington
• Matemática Reversa
• Aritmética de Presburger
• Axiomas de Peano
• Aritmética de Robinson
• Lógica de segunda ordem

Referências

• Burgess, John P., 2005. Fixing Frege. Princeton University Press.
• Buss, S. R., Handbook of proof theory ISBN 0-444-89840-9
• Friedman, Harvey. "Systems of second order arithmetic with restricted induction," I, II (Abstracts). Journal of Symbolic Logic, v.41, pp. 557– 559, 1976. JStor
• Girard, Lafont and Taylor, 1987. Proofs and Types. Cambridge University Press.
• Hilbert, David; Bernays, Paul (1934), Grundlagen der Mathematik, Die Grundlehren der mathematischen Wissenschaften, Band 40, 50, Berlin, New York: Springer-Verlag, MR0237246 
• Simpson, Stephen G. (2009), Subsystems of second order arithmetic, ISBN 978-0-521-88439-6, Perspectives in Logic 2nd ed. , Cambridge University Press, MR2517689 
• Gaisi Takeuti (1975) Proof theory ISBN 0-444-10492-5