Definição Axiomática dos Números Naturais

Na teoria dos conjuntos ZFC (Zermelo-Fraenkel com o Axioma da Escolha), os números naturais podem ser construídos de diversas formas. A teoria ZFC fornece uma base axiomática para a matemática moderna, com axiomas específicos para existência de conjuntos, operações entre conjuntos e propriedades fundamentais como extensionalidade e fundação.

Uma construção comum na teoria ZFC define os números naturais como:

• $0$ é representado pelo conjunto vazio: $0 = \emptyset$;
• Cada número sucessor é definido como: $n+1 = n \cup {n}$.

Assim:

• $0 = \emptyset$;
• $1 = {0} = {\emptyset}$;
• $2 = {0,1} = {\emptyset, {\emptyset}}$;
• $3 = {0,1,2} = {\emptyset, {\emptyset}, {\emptyset, {\emptyset}}}$.

Uma abordagem formal alternativa é através dos axiomas de Peano, que caracterizam os números naturais através de cinco axiomas fundamentais:

1. $0$ é um número natural;
2. para cada número natural $n$, existe um único sucessor $s(n)$;
3. não existe nenhum número natural cujo sucessor seja $0$;
4. se $s(m) = s(n)$, então $m = n$ (a função sucessor é injetiva);
5. se um conjunto contém $0$ e o sucessor de cada elemento do conjunto, então o conjunto contém todos os números naturais (princípio da indução).

Estes axiomas podem ser diretamente implementados em Prolog usando lógica de primeira ordem:

% Definição de números naturais (seguindo axiomas de Peano)
natural(zero).                % Base: 0 é um número natural
natural(s(X)) :- natural(X).  % Indução: Se X é natural, s(X) também é

Neste caso, a amável leitora deve observar que $zero$ representa o número natural $0$, e $s(X)$ representa o sucessor de $X$. Por exemplo, $s(zero)$ representa $1$, $s(s(zero))$ representa $2$, e assim por diante. O terceiro axioma (nenhum número tem $0$ como sucessor) é implicitamente satisfeito, pois não existe regra em que $zero$ apareça como resultado de $s/1$. O quarto axioma (injetividade do sucessor) é garantido pela unificação do Prolog, onde $s(X) = s(Y)$ implica $X = Y$. Finalmente, o quinto axioma (indução) é capturado pela natureza recursiva da segunda cláusula.

Propriedades e Operações nos Números Naturais

Adição

A adição é definida recursivamente seguindo os axiomas:

% Definição da operação de adição
add(zero, Y, Y) :- natural(Y).          % Base: 0 + Y = Y
add(s(X), Y, s(Z)) :- add(X, Y, Z).     % Indução: s(X) + Y = s(X + Y)

Esta definição captura as propriedades essenciais da adição:

• o elemento neutro: $0 + n = n$;
• a recursão sobre o primeiro argumento: $s(m) + n = s(m + n)$.

Definição de Números Específicos

Para facilitar o uso, podemos definir constantes para números específicos:

% Definição de números específicos
dois(s(s(zero))).
quatro(s(s(s(s(zero))))).

3. Verificação de $2 + 2 = 4$

Podemos verificar que $2 + 2 = 4$ usando o predicado add/3:

% Predicado para calcular 2+2
dois_mais_dois(Resultado) :-
    dois(Dois),
    add(Dois, Dois, Resultado).

% Verificação formal de 2+2=4
verifica_dois_mais_dois :-
    dois_mais_dois(Resultado),
    quatro(Quatro),
    Resultado = Quatro.

A execução deste predicado segue estes passos:

1. dois_mais_dois(Resultado) instancia Dois = s(s(zero)) e invoca add(s(s(zero)), s(s(zero)), Resultado)
2. Pela regra de add/3, ocorrem as seguintes deduções:
   • add(s(s(zero)), s(s(zero)), Resultado) implica Resultado = s(Z1) e chama add(s(zero), s(s(zero)), Z1)
   • add(s(zero), s(s(zero)), Z1) implica Z1 = s(Z2) e chama add(zero, s(s(zero)), Z2)
   • add(zero, s(s(zero)), Z2) pela regra base retorna Z2 = s(s(zero))
   • Substituindo, temos Z1 = s(s(s(zero))) e Resultado = s(s(s(s(zero))))
3. quatro(Quatro) instancia Quatro = s(s(s(s(zero))))
4. A unificação Resultado = Quatro verifica com sucesso, provando que $2 + 2 = 4$

Implementação Prática para Consultas Numéricas

Para facilitar o uso de consultas com números inteiros comuns, implementamos:

% Mapeamento entre números e sua representação em termos de sucessores
num(0, zero).
num(1, s(zero)).
num(2, s(s(zero))).
num(3, s(s(s(zero)))).
num(4, s(s(s(s(zero))))).
% Esta definição pode ser estendida para mais números ou gerada recursivamente

% Predicado genérico para soma
soma(A, B, Resultado) :-
    num(A, TermA),             % Converte número A para representação de Peano
    num(B, TermB),             % Converte número B para representação de Peano
    add(TermA, TermB, TermR),  % Realiza a adição usando a definição axiomática
    num(Resultado, TermR).     % Converte o resultado de volta para número

% Consulta para verificação
verifica_soma :-
    soma(2, 2, Resultado),
    Resultado = 4.

Extensões Possíveis

Esta abordagem pode ser estendida para definir outras operações aritméticas:

% Multiplicação
mult(zero, _, zero).                       % Base: 0 * Y = 0
mult(s(X), Y, Z) :-                        % Indução: s(X) * Y = Y + (X * Y)
    mult(X, Y, XY),
    add(Y, XY, Z).

% Potenciação
pot(_, zero, s(zero)).                     % Base: X^0 = 1
pot(X, s(Y), Z) :-                         % Indução: X^s(Y) = X * X^Y
    pot(X, Y, XY),
    mult(X, XY, Z).

As outras ficam por conta da esforçada leitora.