“그런 수가 있다”는 말을 증명하려면 무엇을 보여 줘야 할까요?

“어떤 자연수 n에 1을 더하면 3이 된다”는 문제를 받았다고 합시다. n으로 2를 고를 수 있습니다. 이어 2+1을 계산해 3이 되는지 확인해야 합니다. 답으로 고른 수와 그 수가 조건에 맞는다는 근거가 함께 있어야 증명이 됩니다.

유형론은 이런 증거의 구성을 기호로 기록합니다. 유형은 어떤 대상을 허용하며 그 대상을 어떻게 만들고 사용할지 정한 것입니다. 자연수 유형 ℕ에는 0, 1, 2 같은 수가 들어갑니다. 2 : ℕ은 “2는 자연수 유형의 대상이다”라는 판단입니다. 콜론 :는 이 글에서 소속을 나타냅니다.

P(n)을 “n+1=3”이라는 조건의 이름으로 쓰겠습니다. P(2)를 유형으로 읽으면, 그 안에 들어갈 대상은 2+1=3임을 보이는 증거입니다. 증거를 e라고 부르면 e : P(2)라고 적습니다.

이 방식에서는 증명을 검사할 때 “무엇을 주장하는가”와 “그 주장에 맞는 증거를 제시했는가”를 함께 봅니다. 수 2 자체는 자연수의 대상이고, e는 2가 해당 조건을 만족한다는 증거입니다. 두 역할을 구별해야 다음의 존재 증명을 구성할 수 있습니다.

유형 자체를 정하는 판단과, 그 유형의 대상을 제시하는 판단이 있습니다. 여기에 각각 두 유형 또는 두 대상이 같다는 판단이 더해집니다. 아래 표는 현대적인 콜론 표기로 읽은 예입니다. 원전은 소속을 ∈로 쓰고 집합을 뜻하는 set이라는 표현도 사용합니다.

판단은 규칙을 따라 확인하는 주장입니다. 어떤 조건을 명제로 만들어 부정하거나 양화할 때는 그에 대응하는 유형을 별도로 구성합니다. 9번 문답에서 같음을 명제로 만드는 방법을 살펴보겠습니다.

유형 A를 안다는 것은 그 유형의 정준 대상이 어떤 꼴인지, 두 정준 대상이 언제 같은지 아는 일입니다. 계산되는 표현은 정준형으로 환원해 판단합니다.

아래 활동은 결과 모양과 동일성 조건이 함께 주어져야 유형 설명이 완성된다는 점을 보여 줍니다.

f(n)=n+1로 함수를 정해 봅시다. f(2)는 먼저 2+1로 풀리고, 덧셈 계산을 거쳐 3이 됩니다. 이 계산을 알면 f(2)와 3이 자연수에서 같은 값임을 판단할 수 있습니다.

원전은 표현을 약속으로 정의하는 일, 두 대상이 같다고 판단하는 일, 같음을 하나의 명제로 만드는 일을 구별합니다. 이 글에서는 계산 예로 대상의 같음을 먼저 익힙니다. “같음은 오직 자동 계산으로만 확인된다”는 일반 원칙을 이 1984년 체계에 붙이지 않도록 주의해야 합니다.

어떤 자연수 n을 받아도 “n=n”이라는 증거를 내놓는 방법을 생각해 봅시다. 0을 주면 0=0의 증거, 2를 주면 2=2의 증거를 내놓습니다. 몇 개의 예를 나열하는 데서 더 나아가 임의의 n에 적용할 방법을 제시해야 합니다.

이런 함수의 유형을 Πn:ℕ I(ℕ,n,n)으로 적을 수 있습니다. Π는 각 입력에 맞는 출력을 내놓는 함수 유형을 나타내고, I(ℕ,n,n)은 n이 자신과 같다는 명제의 유형입니다. “모든 n”에 대한 증명은 n을 받는 함수로 구성됩니다.

처음 문제로 돌아갑시다. P(n)은 n+1=3입니다. 수 2와 e : P(2)를 함께 묶으면 “어떤 자연수 n이 P(n)을 만족한다”는 증거를 얻습니다. 이 쌍을 (2,e)라고 쓰겠습니다.

그 증거가 속하는 유형은 Σn:ℕ P(n)입니다. Σ는 첫 번째 대상과 그 대상에 맞는 두 번째 증거를 함께 담는 유형입니다. 첫 성분이 2이면 둘째 성분은 P(2)의 증거여야 합니다. 4를 넣으면서 P(2)의 증거를 그대로 붙이면 이 조건을 만족하지 못합니다.

쌍 (2,e)를 받으면 첫 성분에서 수 2를 꺼내고, 둘째 성분에서 2+1=3의 증거 e를 얻습니다. 전칭 증거를 함수로 받았다면 필요한 수를 입력해 그 수에 대한 증거를 얻습니다.

증거를 만드는 규칙을 도입 규칙, 이미 가진 증거를 사용하는 규칙을 제거 규칙이라고 합니다. 버튼을 눌러 같은 주장을 증명할 때와 사용할 때를 구별해 보세요.

I(A,a,b)는 “A의 대상 a와 b가 같다”라는 명제에 대응하는 유형입니다. 이 명제를 증명하면 그 증거를 다른 논리적 구성 안에서도 사용할 수 있습니다.

이 글이 읽는 1984년 원전은 동일성 증거에서 대상의 같음으로 돌아가는 규칙도 둡니다. c : I(A,a,b)를 얻으면 a = b : A를 결론 낼 수 있습니다. 원전의 이 규칙을 생략하면 오늘날의 다른 유형론과 혼동할 수 있습니다. 아래 표는 이 책의 두 규칙을 함께 보여 줍니다.

강의록은 빈 유형, 단위 유형, 두 원소 유형과 자연수 유형을 형성·도입·제거·계산 규칙으로 설명합니다.

대상을 나열하는 것만으로 끝나지 않고, 그 유형에서 함수를 정의하거나 귀납적으로 증명하는 제거 규칙이 핵심입니다.

자연수에서는 0을 만들고, 이미 만든 수 n에서 다음 수 s(n)을 만듭니다. 2는 s(s(0))으로 읽을 수 있습니다. 자연수에 관한 모든 경우를 증명하려면 0에서 성립함과 n에서 성립할 때 s(n)에서도 성립함을 보이는 귀납 규칙을 사용합니다.

x:A라는 가설 아래 B(x) type이나 b(x):B(x)를 판단할 수 있습니다. 실제 a:A가 주어지면 대입을 통해 B(a)와 b(a)를 얻습니다.

의존 유형은 이런 맥락을 앞에 적어 변수의 범위와 의존성을 공개합니다. 가설을 생략하면 어떤 대상에 기대는 판단인지 잃기 쉽습니다.

앞에서 정한 f(x)=x+1에는 “x는 자연수”라는 가설이 붙어 있습니다. x 자리에 2를 넣으면 f(2)=3을 얻습니다. 이 가설과 대입값을 함께 적으면 입력의 유형과 출력의 유형이 맞는지 확인할 수 있습니다.

자연수나 두 원소 유형처럼 여러 유형을 한 규칙에서 다루고 싶을 수 있습니다. 원전은 정해진 유형 구성에 대해 닫혀 있는 모음 U를 도입하고 이를 유니버스라고 부릅니다.

책은 두 구성 방식을 소개합니다. 코드 방식에서는 U의 대상 a가 유형의 이름 역할을 하고, T(a)가 그 코드가 가리키는 유형입니다. 예를 들어 자연수를 가리키는 코드와 실제 자연수 유형을 구별하는 방식입니다. U를 자기 자신을 포함하는 모든 유형의 집합이라고 정하면 이 구성의 조건을 벗어납니다.

“어떤 자연수 n에 대해 n+1=3”의 증거가 맞는지 검사해 봅시다. 첫 성분은 자연수여야 하고, 둘째 성분은 바로 그 수를 넣은 등식의 증거여야 합니다. 두 부분을 함께 읽어야 증명 전체를 판단할 수 있습니다.

아래 세 경우에서 무엇이 갖추어졌고 무엇이 빠졌는지 비교해 보세요.

수 2를 고르고 2+1=3을 확인한 증거 e를 붙이면 (2,e)가 됩니다. 이것이 “그런 수가 있다”는 주장에 맞는 구성입니다. 누군가에게 이 증거를 건네면 그 사람은 어떤 수를 골랐는지와 왜 그 수가 조건에 맞는지를 함께 확인할 수 있습니다.

유형론은 이처럼 증거의 구성과 사용을 논리 규칙으로 다룹니다. 더 깊이 읽을 때는 이 책이 채택한 판단·동일성·유니버스 규칙을 함께 확인해야 합니다. 실제 증명 보조기에 옮길 때도 해당 도구가 어떤 체계를 사용하는지 살펴야 합니다.