correto, mas meio sacana pros leigos coloca-los no nihilismo semiotico sem dizer que eh possivel formalizar sem depender dos simbolos.
hyper simplificando, parte-se da existencia do zero, e de uma funcao sucessor Suc
o proximo numero (chame-o como quiser) é Suc(0)
depois, vem Suc(Suc(0))... , entao Suc(Suc(Suc(0)))
a partir dessas recursoes, pode-se definir adicao, multiplicacao, e a aritmetica. Ate chegar ao ponto onde se mostra que ela existe, funciona, mas nao eh completa, via Godel.
E se pode provar que o sistema de numeracao usual forma uma bijecao correta com o cj abstrato dos naturais definido assim.
a wiki nao eh a melhor referencia, mas eh por ai:
https://en.wikipedia.org/wiki/Peano_axioms