Mostrar código-fonte de Aritmética de segunda ordem

{{Mais notas|data=agosto de 2014}}
Na [[Lógica matemática]], '''aritmética de segunda ordem''' é uma coleção de sistemas [[Axioma | axiomáticos]] que formalizam os [[números naturais]] e seus subconjuntos. É uma alternativa para a [[teoria dos conjuntos#4 |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<sub>2</sub>.

Aritmética de segunda ordem inclui, mas é significativamente mais forte do que, a [[Axiomas de Peano | 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 ([[Conjunto finito|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 matemática|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 a[[Axiomas de Zermelo-Fraenkel|xiomá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<sub>2</sub>). 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-[[Demonstração construtiva|construtiva]].

==Definição==

===Sintaxe===

A linguagem da aritmética de segunda ordem é dividida em duas partes. A primeira parte de [[Termo (lógica)|termos]] e [[Variável (matemática)|variáveis]], geralmente indicados por letras minúsculas, é composta por [[indivíduo]]s, 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 [[Variáveis livres e ligadas|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, <math>\forall n (n\in X \rightarrow Sn \in X)</math>, é 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 <math>\exists X \forall n(n\in X \leftrightarrow n < SSSSSS0\cdot SSSSSSS0)</math> é 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 [[Axiomas de Peano|aritmética de Peano]] sem indução. O [[universo de discurso]] para as variáveis [[Quantificação|quantificadas]] são os [[números naturais]], denotado coletivamente por '''N''', e incluindo o membro destacado <math>\ 0</math>, chamado de "zero".

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

Axiomas que regem a [[função sucessor]] e [[zero]]:
:1. <math>\forall m [Sm=0 \rightarrow \bot].</math> (“o sucessor de um número natural nunca é zero”)
:2. <math>\forall m \forall n [Sm=Sn \rightarrow m=n].</math> (“a função sucessor é injetora”)
:3. <math>\forall n [0=n \lor \exists m [Sm=n] ].</math> (“cada número natural é zero ou um sucessor”)

[[Adição]] definida [[Recursividade|recursivamente]]:

:4. <math>\forall m [m+0=m].</math>
: 5. <math>\forall m \forall n [m+Sn = S(m+n)].</math>

[[Multiplicação]] definida [[Recursividade|recursivamente]]:

:6. <math>\forall m [m\cdot 0 = 0].</math>
: 7. <math>\forall m \forall n [m \cdot Sn = (m\cdot n)+m].</math>

Axiomas que regem a [[Teoria da ordem|relação de ordem]] "<":
:8. <math>\forall m [m<0 \rightarrow \bot].</math> (“nenhum número natural é menor do que zero”)
: 9. <math>\forall m [m<Sn \leftrightarrow (m<n \lor m=n)].</math>
: 10. <math>\forall n [0=n \lor 0<n].</math> (“todo número natural é zero ou maior do que zero”)
: 11. <math>\forall m \forall n [(Sm<n \lor Sm=n) \leftrightarrow m<n].</math>

Estes axiomas são todos enunciados de [[lógica de primeira ordem|primeira ordem]]. Ou seja, todas as variáveis são definidas sobre os [[números naturais]] e não [[Teoria dos conjuntos|conjuntos]] do mesmo, um fato ainda mais forte do que ser aritmético. Além disso, há apenas um [[Quantificação existencial|quantificador existencial]], em axioma 3. Axiomas 1 e 2, juntamente com um [[Axiomas de Peano|esquema de axioma de indução]] compõem a definição [[Axiomas de Peano|Peano-Dedekind]] usual de '''N'''. Somando-se a estes axiomas qualquer tipo de [[Axiomas de Peano|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:

:<math>\forall m_\bullet \forall X_\bullet ((\varphi(0) \land \forall n (\varphi(n) \rightarrow \varphi(Sn)) \rightarrow \forall n \varphi(n))</math>

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 "<math>n \in X</math>" 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 φ é:

:<math>\forall X ((0\in X \land \forall n (n\in X \rightarrow Sn\in X)) \rightarrow \forall n (n\in X))</math>

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:

:<math>\forall m_\bullet \forall X_\bullet \exists Z \forall n (n\in Z \leftrightarrow \varphi(n))</math>

Essencialmente, isso nos permite formar o conjunto <math>Z = \{ n | \varphi(n) \}</math> 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 <math>n \not \in Z</math> levaria ao axioma da compreensão :<math>\exists Z \forall n ( n \in Z \leftrightarrow n \not \in Z)</math> , 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''' <math>\mathcal{M}</math> 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 <math>\mathcal{M}</math> é 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.&nbsp;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 <math>\mathrm{ACA}_0</math>.

<math>\mathrm{ACA}_0</math> é 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 ω <math>\mathrm{ACA}_0</math> se e somente se S é fechado sob o salto de Turing, redutibilidade de Turing, e a inicialização de Turing.

O subscrito 0 em <math>\mathrm{ACA}_0</math> 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 <math>\mathrm{ACA}_0</math> além da indução para todas as fórmulas é às vezes chamado <math>\mathrm{ACA}</math>.

O sistema <math>\mathrm{ACA}_0</math> é 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 ε<sub>0</sub> 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 Δ<sup>0</sup><sub style="margin-left:-0.65em">0</sub>, 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

:<math>\forall n<t(\cdots)</math>

significa

:<math>\forall n(n<t \rightarrow \cdots)</math>

e

:<math>\exists n<t(\cdots)</math>

significa

:<math>\exists n(n<t \land \cdots)</math>.

Uma fórmula é chamada de Σ<sup>0</sup><sub style="margin-left:-0.65em">1</sub> (ou, por vezes, Σ<sub>1</sub>), respectivamente Π<sup>0</sup><sub style="margin-left:-0.65em">1</sub>(ou, por vezes, Π<sub>1</sub>) quando a forma de ∃''m''<sub>•</sub>(φ), respectivamente ∀''m''<sub>•</sub>(φ onde φ é uma fórmula aritmética limitada e ''m'' é uma variável individual (que é livre em φ). De modo mais geral, uma fórmula é chamada Σ<sup>0</sup><sub style="margin-left:-0.65em">''n''</sub>, respectivamente Π<sup>0</sup><sub style="margin-left:-0.65em">''n''</sub> quando ele é obtido através da adição de existenciais, respectivamente, quantificadores universais individuais para um Π<sup>0</sup><sub style="margin-left:-0.65em">''n''&minus;1</sub>, respectivamente Σ<sup>0</sup><sub style="margin-left:-0.65em">''n''&minus;1</sub> fórmula (e Σ<sup>0</sup><sub style="margin-left:-0.65em">0</sub> e Π<sup>0</sup><sub style="margin-left:-0.65em">0</sub> são todas equivalentes Δ<sup>0</sup><sub style="margin-left:-0.65em">0</sub>). 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 Σ<sup>0</sup><sub style="margin-left:-0.65em">''n''</sub> ou Π<sup>0</sup><sub style="margin-left:-0.65em">''n''</sub> para todos suficientemente grande ''n'' .
===Compreensão Recursiva===

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

:<math>\forall m \forall X ((\forall n (\varphi(n) \leftrightarrow \psi(n))) \rightarrow \exists Z \forall n (n\in Z \leftrightarrow \varphi(n)))</math>

O conjunto de consequências de primeira ordem de <math>\mathrm{RCA}_0</math> é a mesma que os da I&Sigma;<sub>1</sub> subsistema da aritmética de Peano em que a indução é restrita a Σ<sup>0</sup><sub style="margin-left:-0.65em">1</sub> fórmulas. Por sua vez, I&Sigma;<sub>1</sub> é conservador em relação à aritmética recursiva primitiva (PRA) para sentenças <math>\Pi^0_2</math>.
Além disso, o ordinal prova teórica de <math>\mathrm{RCA}_0</math> é ω<sup>ω</sup>, 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 <math>\mathrm{RCA}_0</math>. Esta é a motivação por trás do nome deste sistema – se pode ser provada a existência de um conjunto usando <math>\mathrm{RCA}_0</math> , então o conjunto é computável (ou seja recursivo).

===Sistemas mais fracos ===
Às vezes, um sistema ainda mais fraca do que <math>\mathrm{RCA}_0</math> é 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 Δ<sup>0</sup><sub style="margin-left:-0.65em">1</sub> compreensão mais indução de Δ<sup>0</sup><sub style="margin-left:-0.65em">0</sub>.

===Sistemas mais fortes ===
Por mais que nós definimos Σ<sub>''n''</sub> e Π<sub>''n''</sub> (ou, mais precisamente, Σ<sup>0</sup><sub style="margin-left:-0.65em">''n''</sub> e Π<sup>0</sup><sub style="margin-left:-0.65em">''n''</sub>) fórmulas, podemos definir fórmulas Σ<sup>1</sup><sub style="margin-left:-0.6em">''n''</sub> e Π<sup>1</sup><sub style="margin-left:-0.6em">''n''</sub> da seguinte maneira: a fórmula Δ<sup>1</sup><sub style="margin-left:-0.6em">0</sub> (ou Σ<sup>1</sup><sub style="margin-left:-0.6em">0</sub> ou Π<sup>1</sup><sub style="margin-left:-0.6em">0</sub>) é apenas uma fórmula aritmética e a fórmula Σ<sup>1</sup><sub style="margin-left:-0.6em">''n''</sub> , respectivamente Π<sup>1</sup><sub style="margin-left:-0.6em">''n''</sub>, é obtida pela adição de, respectivamente existenciais universais, quantificadores de classe em frente de um Π<sup>1</sup><sub style="margin-left:-0.6em">''n''&minus;1</sub>, respectivamente Σ<sup>1</sup><sub style="margin-left:-0.6em">''n''&minus;1</sub>.

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 Σ<sup>1</sup><sub style="margin-left:-0.6em">''n''</sub> or Π<sup>1</sup><sub style="margin-left:-0.6em">''n''</sub> para todo n suficientemente grande. O sistema '''Π<sup>1</sup><sub style="margin-left:-0.6em">1</sub>-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 Π<sup>1</sup><sub style="margin-left:-0.6em">1</sub> fórmula φ. É um exercício fácil mostrar que isso é realmente equivalente a Σ<sup>1</sup><sub style="margin-left:-0.6em">1</sub>-compreensão (por outro lado, Δ<sup>1</sup><sub style="margin-left:-0.6em">1</sub>-compreensão, definida pelo mesmo truque como apresentado anteriormente para Δ<sup>0</sup><sub style="margin-left:-0.65em">1</sub>-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<sub>2</sub>

Muitar proposições naturais expressíveis na linguagem da aritmética de segunda ordem são independentes de Z<sub>2</sub> e ainda [[ZFC]], mas podem ser provadas pela determinância projetiva. Exemplos incluem a coanalítica [[Conjunto|propriedade do conjunto perfeito]], mensurabilidade e a [[Teorema da categoria de Baire]] para os conjuntos <math>\Sigma^1_2</math>, [[Uniformização (teoria dos conjuntos)|uniformização]] <math>\Pi^1_3</math>, etc. Sobre uma fraca base teórica (assim como RCA<sub>0</sub>), determinância projetiva implica compreensão e provê uma teoria completa da aritmética de segunda ordem — Sentenças naturais na linguagem de Z<sub>2</sub> que são independentes de Z<sub>2</sub> com determinância projetiva são difíceis de encontrar.<ref>{{citar periódico|autor = W. Hugh Woodin |título= The Continuum Hypothesis, Part I |periódico= Notices of the American Mathematical Society | volume = 48 |número= 6 |ano= 2001}}</ref>

ZFC + {onde existe [[Woodin cardinal | cardinais Woddin]] ''n'': ''n'' é um número natural} é uma conservação sobre Z<sub>2</sub> com determinância projetiva, que é uma declaração na linguagem da aritmética de segunda ordem que é provável em Z<sub>2</sub> 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 [[Número inteiro | inteiro]]s arbitrários ou [[Número racional | números racionais]] são os habitantes de primeira-classe da mesma forma que números naturais. [[Função (matemática) | Funções]] entre esses conjuntos podem ser codificadas como conjuntos de pares, e portanto, como [[subconjunto]]s dos números naturais, sem dificuldade. [[Número real | Números reais]] podem ser definidos como [[Sucessão de Cauchy| 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<sup>&minus;''n''</sup>). Esses sistemas não podem se referir à funções reais, ou subconjuntos dos reais. Não obstante, [[Função contínua | 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 à [[Conjunto aberto | 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]]
*[[Teoria da computabilidade#Matemática reversa | Matemática Reversa]]
*[[Aritmética de Presburger]]
*[[Axiomas de Peano]]
*[[Aritmética de Robinson]]
*[[Lógica de segunda ordem]]

{{Referências|Notas}}

==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.&nbsp;557– 559, 1976. [http://www.jstor.org/stable/2272259 JStor]
*Girard, Lafont and Taylor, 1987. [https://web.archive.org/web/20080418044121/http://www.monad.me.uk/stable/Proofs+Types.html Proofs and Types].  Cambridge University Press.
*{{Citation |último1 =Hilbert |primeiro1 =David |autorlink1 =David Hilbert |último2 =Bernays |primeiro2 =Paul |título=Grundlagen der Mathematik |publicado=[[Springer-Verlag]] |local=Berlin, New York | series=Die Grundlehren der mathematischen Wissenschaften, Band 40, 50 | id={{MathSciNet | id = 0237246}} |ano=1934}}
*{{Citation |último1 =Simpson |primeiro1 =Stephen G. |título=Subsystems of second order arithmetic | url=http://www.math.psu.edu/simpson/sosoa/ |publicado=[[Cambridge University Press]] |edição=2nd | series=Perspectives in Logic | isbn=978-0-521-88439-6 | id={{MathSciNet | id = 2517689}} |ano=2009}}
*[[Gaisi Takeuti]] (1975) ''Proof theory'' ISBN 0-444-10492-5

[[Categoria:Lógica matemática]]
[[Categoria:Aritmética]]