페아노 공리계_(비교)

다만 페아노 공리계와 ZFC 공리계가 분리되어 있는 이유는, 당연히 공리의 의존성을 줄이고 순도를 높이기 위해서이다. ZFC에 대부분의 도구가 정의되어 있으니 '~가 존재한다는 걸 공리로 가정(assume)'할 필요 없이 '~가 존재한다는 걸 증명(prove)'하기만 하면 되는 건 편하지만, ZFC는 ZFC고 이와 호환되지 않는 다른 well-defined된 다른 공리계들도 존재한다. 그런 공리계에서조차 '자연수'라는 개념을 공리적으로든, 구성적으로든 하여간 어떠한 방법으로든 '구현'하기 위해서 필요한 게 페아노 공리계, 즉 일종의 '<자연수 만들기 레시피> [재료는 알아서 구하셈 ㅇㅇ]'와 같다.

일례로 람다 대수에서는 0을 False로 가정하고, successor를 [math(\lambda n.\lambda f.\lambda x.f((n f) x))]로 정의한 다음 처치 부호화를 사용해 자연수를 정의하지만, 0과 successor가 존재하기 때문에 람다 함수의 합성이라는 뇌내에 떠올리기조차 힘든 괴랄한 구조(?)임에도 불구하고 람다 대수에서 자연수 집합에 작용하는 모든 명제가 성립한다는 것을 증명할 수 있다.