# Aritmética de função elementar

Em teoria da prova, que é um ramo da lógica matemática, aritmética de função elementar, também chamada de AFE (EFA), aritmética elementar ou aritmética de função exponencial, é o sistema da aritmética com propriedades elementares habituais de 0, 1, +, ×, x$^y$, em conjunto com a indução para fórmulas com quantificadores limitados.
A AFE é um sistema lógico muito fraco, cujo ordinal da prova teórica é ω$^3$, mas ainda parece ser capaz de provar muito da matemática ordinária que pode ser expressa em linguagem aritmética de primeira-ordem.

## Definição

AFE é um sistema em lógica de primeira ordem (com igualdade). Sua linguagem contém:
* duas constantes 0, 1,
* três operações binárias +, ×, exp, com exp(x,y) normalmente escrita como x$^y$,
* um símbolo de relação binária < (Isto não é realmente necessário já que ele pode ser escrito em termo das outras operações e é algumas vezes omitido, mas é conveniente para se definir quantificadores limitados).
Quantificadores limitados são aqueles na forma ∀(x<y) e ∃(x<y) que são abreviações para ∀x(x<y)→,,, e ∃x(x<y)∧... na maneira usual.
Os axiomas de AFE são
* Os axiomas da Aritmética de Robinson para 0, 1, +, ×, <
* Os axiomas para exponenciação: x$^0$ = 1, x$^{y+1}$ = x$^y$×x.
* Indução para fórmulas cujos quantificadores são limitados (mas que podem conter variáveis livres).

## Grande conjectura de Friedman

A grande conjectura de Harvey Friedman implica que muitos teoremas matemáticos, tal como o Último teorema de Fermat, podem ser provados em sistemas muito fracos como o AFE.
A declaração original da conjectura de Friedman (1999) é:
    "Todo teorema publicado nos Anais da Matemática cuja declaração envolve somente objetos matemáticos finitos (por exemplo, o que lógicos chamam de enunciado aritmético) pode ser provado em AFE. AFE é o fragmento fraco da Aritmética de Peano baseado nos usuais axiomas sem quantificadores para 0, 1, +, ×, exp, junto com o esquema de indução para todas as fórmulas na linguagem cujos quantificadores são limitados."
Enquanto é fácil construir enunciados aritméticos artificiais que são verdadeiros mas não têm prova em AFE, o objetivo da conjectura de Friedman é que exemplos naturais de tais enunciados na matemática parecem ser raros. Alguns exemplos naturais incluem enunciados de consistência provenientes da lógica, vários enunciados relacionados à Teoria de Ramsey tais como o lema da regularidade de Szemerédi e o teorema menor dos grafos, e o algoritmo de Tarjan para uma estrutura de dados de subconjuntos-disjuntos.

## Sistemas relacionados

Pode-se omitir o símbolo exp de função binária da linguagem ao se tomar a artimética de Robinson junto com a indução de todas as fórmulas com quantificadores limitados e um axioma enunciando, grosso modo, que exponenciação é uma função definida em todos os lugares. Isto é similar ao AFE e tem a mesma força prova-teórica mas é mais complicado de se trabalhar.
Existem fragmentos fracos da aritmética de segunda ordem chamados RCA* 0 e WKL* 0 que têm a mesma força de consistência da AFE e são conservadores sobre ela por Π0 2 sentenças, o que é às vezes estudado em matemática reversa (Simpson 2009).
Aritmética recursiva elementar (ARE/ERA) é um subsistema da aritmética recursiva primitiva (ARP/PRA) onde a recursão é restrita a somas e produtos limitados. Isto também tem as mesmas Π0 2 sentenças que AFE, no sentido de que sempre que AFE prova ∀x∃y P(x,y), com P sendo livre de quantificadores, ARE prova a fórmula aberta P(x,T(x)), com T um termo definível em ARE.
Assim como PRA, ARE pode ser definida de maneira completamente livre de lógica, somente com as regras de substituição e de indução, e definindo equações para todas as funções recursivas elementares. No entanto, diferente de PRA, as funções recursivas elementares podem ser caracterizadas pelo fecho sob composição e projeção de um número finito de funções básicas, sendo assim, somente um número finito de equações definidoras é necessário.

## Veja também

* ELEMENTARY, uma classe de complexidade computacional relacionada
* Hierarquia de Grzegorczyk
* Matemática reversa
* Problema algébrico colegial de Tarski