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.
As regras lógicas da APR são modus ponens e substituição de variáveis e equações recursivamente definidas para cada função primitiva recursiva desejada, especialmente: A APR substitui o sistema axiomático da indução da lógica de primeira ordem pela regra da indução (livre de quantificadores): 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.
É 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 A regra de indução no sistema de Curry era incomum. Posteriormente, um refinamento foi feito por Reuben Goodstein. A regra de indução no sistema de Goodstein é: F ( 0 ) = G ( 0 ) F ( S ( x ) ) = H ( x , F ( x ) ) G ( S ( x ) ) = H ( x , G ( x ) ) F ( x ) = G ( x ) . {\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:
