Aritmética primitiva recursiva

A Aritmética Primitiva Recursiva(APR), é uma formalização dos números naturais, livre de quantificadores. Foi primeiramente proposta por Skolem como uma formalização de sua concepção finitista das fundações da aritmética, e é amplamente acordado que todo raciocínio da APR é finitista. Muitos acreditam que todo o finitismo é englobado pela APR, mas outros acreditam que o finitismo pode ser estendido à formas de recursão além da primitiva, como ε₀, que é a prova teórica ordinal da Aritmética de Peano. A prova teórica ordinar da ARP é ω^ω, onde ω é o menor ordinal transfinito. APR é geralmente chamada de Aritmética de Skolem.

A linguagem da APR pode expressar proposições aritméticas envolvendo números naturais e qualquer forma primitiva de função recursiva, incluindo as operações de adição, multiplicação e exponenciação. A APR não pode quantificar explicitamente sobre o domínio dos números naturais. A APR é geralmente tomada como o sistema matemático formal para teoria de provas, em particular para provas de consistência, como a prova de consistência de Gentzen da aritmética de primeira ordem.

Linguagem e axiomas

A linguagem da APR consiste de:

• Um número contável e infinito de variáveis x, y, z... cada um variando sobre os números naturais.
• Conectivos proposicionais
• O símbolo de igualdade =, o símbolo de constante 0 e o símbolo de sucessor S (significando adicionar um)
• Um símbolo para cada função recursiva primitiva

Os axiomas lógicos da APR são:

• Tautologias da lógica proposicional
• Axiomatização usual da igualdade como uma relação de equivalência

As regras lógicas da APR são modus ponens e substituição de variáveis

Os axiomas não-lógicos são:

• ${\displaystyle S(x)\neq 0}$;
• ${\displaystyle S(x)=S(y)~\to ~x=y,}$

e equações recursivamente definidas para cada função primitiva recursiva desejada, especialmente:

• ${\displaystyle x+0=x\ }$
• ${\displaystyle x+S(y)=S(x+y)\ }$
• ${\displaystyle x\cdot 0=0\ }$
• ${\displaystyle x\cdot S(y)=xy+x\ }$

A APR substitui o sistema axiomático da indução da lógica de primeira ordem pela regra da indução (livre de quantificadores):

• From ${\displaystyle \varphi (0)}$ and ${\displaystyle \varphi (x)\to \varphi (S(x))}$, deduce ${\displaystyle \varphi (y)}$, for any predicate ${\displaystyle \varphi .}$

Na aritmética de primeira ordem, as únicas funções primitivas recursivas que precisam ser explicitamente axiomatizadas são a adição e a multiplicação. Todos os outros predicados primitivos recursivos podem ser definidos usando essas duas funções primitivas recursivas e quantificação sobre os números naturais. Definir funções primitivas recursivas desta maneira não é possível na APR, pois ela não possui quantificadores.

Cálculo livre de conectivos lógicos

É possível formalizar a APR de uma maneira na qual ela não possui nenhum conectivo lógico - a sentença da APR é simplesmente uma equação entre dois termos. Desse modo, um termo é uma função primitiva recursiva de zero ou mais variáveis. Em 1941, Haskell Curry criou o primeiro sistema da APR livre de conectivos lógicos^[1] A regra de indução no sistema de Curry era incomum. Posteriormente, um refinamento foi feito por Reuben Goodstein.^[2] A regra de indução no sistema de Goodstein é:

${\displaystyle {F(0)=G(0)\quad F(S(x))=H(x,F(x))\quad G(S(x))=H(x,G(x)) \over F(x)=G(x)}.}$

Aqui, x é uma variável, S é a operação de sucessor e F, G e H são qualquer função primitiva recursiva que podem possuir parâmetros diferentes dos aqui mostrados. A outra regra de inferência do sistema de Goodstein são as regras de substituição a seguir:

${\displaystyle {F(x)=G(x) \over F(A)=G(A)}\qquad {A=B \over F(A)=F(B)}\qquad {A=B\quad A=C \over B=C}.}$

Onde A, B e C são quaisquer termos(funções primitivas recursivas de zero ou mais variáveis). Finalmente, temos símbolos para qualquer função primitiva recursiva com equações correspondentes, assim como no sistema de Skolem.

Desse modo, a lógica proposicional pode ser inteiramente descartada, os operadores lógicos podem ser expressos aritmeticamente e, por exemplo, o valor absoluto da diferença de dois números pode ser definido pela seguinte recursão primitiva:

${\displaystyle {\begin{aligned}P(0)=0\quad &\quad P(S(x))=x\\x{\dot {-}}0=x\quad &\quad x{\dot {-}}S(y)=P(x{\dot {-}}y)\\|x-y|=&(x{\dot {-}}y)+(y{\dot {-}}x).\\\end{aligned}}}$

Assim, as equações x=y e |x-y|=0 são equivalentes. Portanto, as equações ${\displaystyle |x-y|+|u-v|=0\!}$ e ${\displaystyle |x-y|\cdot |u-v|=0\!}$ expressam a conjunção e disjunção lógica, respectivamente, das equações x=y e u=v. A negação pode ser expressa como ${\displaystyle 1{\dot {-}}|x-y|=0}$.

Ver também

• Aritmética recursiva elementar
• Aritmética de Heyting
• Axiomas de Peano
• Aritmética de segunda ordem
• Função recursiva primitiva

Referencias

Ligações externas

• Feferman, S (1992) What rests on what? The proof-theoretic analysis of mathematics.