그냥 한 번 복습용으로 적어보는 글입니다. 말 그대로 간략한 소개이기 때문에 내용이 엄밀하지는 않습니다.
페아노 산술 (1차 이론)
산술의 표준 해석 N은 페아노 산술의 모델이며, 다음과 같은 구조(structure)를 갖는다.
N = (ℕ;0,s,+,⋅)
여기서 ℕ은 0을 포함한 자연수 집합이다.
공리
페아노 산술은 기초적인 산술을 수행할 수 있기 때문에 괴델의 불완전성 정리가 적용되는 대표적인 형식 이론입니다. 마지막 귀납 공리 schema에서 나타난 φ(0)은 0이 등장하는 임의의 논리식을 나타내는 메타기호입니다. 1차 논리는 술어를 양화할 수 없기 때문에 귀납 공리를 한 문장으로 나타내지 못하고 무한 개로 나타내야 합니다.
<1+1=2, Fitch 스타일 증명>
<0+x=x, Fitch 스타일 증명>
위 공리에서 8번 귀납 공리 schema를 제거하면 Robinson arithmetic을 얻게 됩니다. 이 이론 또한 불완전성 정리가 적용되는 표준 산술 이론입니다. 예를 들어 Robinson arithmetic에서는 덧셈 교환 법칙 ∀x∀y(x+y=y+x)이 증명 또는 반증이 불가능합니다.
페아노 공리에서 6, 7 공리를 제거하면 Presburger arithmetic을 얻게 되며, 이 이론은 비록 페아노 산술과 로빈슨 산술보다 훨씬 약한 이론이지만 일관성과 완전성을 만족합니다(불완전성 정리가 적용되지 않음). 프레스버거 산술 외에도 불완전성 정리가 적용되지 않는 흥미로운 수학 이론이 여럿 존재합니다.
2차 논리부터는 8번 schema를
∀X(X(0)∧∀x(X(x)→X(s(x)))→∀xX(x))
로 바꾸면 페아노 산술을 유한 공리로 나타낼 수 있고, 이를 2차 페아노 산술이라 부릅니다. 2차 산술에서는 표현 강도가 증가함에 따라 1, 2번 공리 그리고 2차 귀납 공리만 있으면 덧셈과 곱셈이 정의 가능합니다. 하지만 편의상 그냥 8개로 사용하는 것이 보통인 듯합니다. (교재마다 공리나 기호 몇 개가 생략되거나 추가되는 등 조금씩 차이가 있음)
페아노 산술은 무한 공리가 없는 ZFC 집합론에서 해석 가능(interpretable)하며, 2차 페아노 산술은 멱집합 공리가 없는 ZFC 집합론에서 해석 가능하다고 합니다. 2차 페아노 산술 정도만 해도 매우 강력한 이론으로서 일반적인 해석학이나 대수학을 다루는 데 있어서는 큰 무리가 없습니다.
2차 페아노 산술로부터 수학을 전개하는 대략적인 스케치를 설명해 보겠습니다. 이 방식은 집합론에서 수학을 전개하는 방식과 비슷한 점이 많습니다.
2차 논리식 ∀x(X(x)↔Y(x)), ∀x(X(x)→Y(x))를 각각 집합론에서의
- X=Y
- X⊆Y
로 생각할 수 있습니다. 술어 변수를 집합으로 생각하시면 이해가 더 수월하실 것 같습니다.
자연수 집합 ℕ을 다음과 같이 정의합니다.
∃X∀x(X(x)↔x=x)
우리가 고려하는 모델의 domain은 자연수 집합이기 때문에 ∀x가 지정하는 범위가 곧 모든 자연수입니다. 2차 논리의 comprehension 공리를 사용하여 “모든 x를 만족하는 술어 X가 존재한다”라는 의미의 위 논리식을 만들 수 있습니다. 이때 이 어떤 X를 자연수 집합으로 간주합니다.
순서쌍 개념을 다루기 위해 pairing function을 정의합니다.
⟨x,y⟩ := (x+y)⋅(x+y)+x
그리고 이론 내에서 다음이 증명 가능합니다
⟨x,y⟩=⟨z,w⟩ ⟺ x=z ∧ y=w
집합론에서 순서쌍을 {{x},{x,y}}로 정의하는 것을 2차 산술에서는 (x+y)²+x 형태의 2항 함수로 정의합니다. 그리고 집합론에서 X,Y⊆ℕ에 대해 x∈X이고 y∈Y인 모든 ⟨x,y⟩들로 이루어진 집합 X×Y⊆ℕ이 존재함을 증명하는 과정 또한 2차 페아노 산술에서 가능합니다. 계속 나아가 집합론에서 순서쌍과 곱집합 개념을 설명한 뒤 함수를 정의하는 것처럼 2차 산술에서도 함수를 정의할 수 있습니다. (개인적인 사견으로는 이미 s나 + 같은 함수 기호가 있는데 또 새롭게 함수라는 개념을 정의하는 게 조금 신기하네요.)
comprehension 공리와 2차 귀납 공리를 통해 특정 함수들의 존재를 증명할 수 있으며, 이로부터 원시 재귀(primitive recursion) 개념 또한 다룰 수 있게 됩니다. 지수 함수도 표현할 수 있으며, 지수 함수의 일반적 성질들 또한 2차 산술에서 증명할 수 있습니다.
집합론에서 자연수를 바탕으로 정수, 유리수, 실수 개념을 만들어 내는 과정이 2차 산술에서도 비슷하게 수행됩니다. 원래는 이 과정을 주로 쓰고 싶었는데, 아무래도 수식이 너무 많이 나오다 보니 너무 고된 작업이 될 것 같아 포기했습니다. S. G. Simpson의 Subsystems of Second Order Arithmetic에서 이 과정이 아주 잘 설명되어 있으니 관심 있으신 분은 읽어 보시는 것을 매우 추천드립니다.
사실 이 글에서 설명한 과정은 2차 산술보다 약한 체계인 ACA₀(comprehension 공리와 2차 귀납 공리에 부분적으로 제약을 둔 체계)에서도 충분히 수행될 수 있습니다. 이 정도 체계에서도 대수학의 기본 정리, 한–바나흐 정리, 바나흐–슈타인하우스 정리처럼 수학 교재에 등장하는 정리들의 상당 부분을 (적절한 정식화 하에서) 증명할 수 있습니다. 이 부분도 방금 말한 Simpson의 글에서 잘 설명되어 있습니다.
여담으로 방금 언급한 정리들을 자연연역이나 힐베르트 스타일로 증명한다면 그 내용이 얼마나 길어질지 두렵네요...