전제를 한 번 더 써도 된다는 규칙을 막으면, 커리 역설을 피할 수 있을까요?

순진한 포괄(naive comprehension)은 식 A(x)가 주어지면 그 식을 만족하는 대상들의 집합 {x : A(x)}이 존재한다고 둡니다. 원전은 이를 x∈{x : A(x)} ↔ A(x)라는 도식으로 적습니다. 왼쪽은 x가 그 집합에 속한다는 문장이고, 오른쪽은 x가 조건 A를 만족한다는 문장입니다.

이 도식은 모든 식 A에 적용됩니다. 따라서 A 안에 소속 관계와 조건문, 자기 자신을 가리키는 표현이 들어가도 같은 방식으로 집합을 만들 수 있습니다. 커리 역설은 이 넓은 허용 범위와 조건문의 추론 규칙이 만나는 지점에서 생깁니다.

임의의 문장 A를 하나 고릅니다. 교육용 사례에서는 A를 “경보가 울린다”라고 읽겠습니다. 이제 R={x : x∈x → A}로 둡니다. R은 “자기 자신에 속한다면 A가 성립한다”라는 조건을 만족하는 모든 x의 집합입니다.

여기에서 A의 내용은 특별하지 않습니다. 논증이 임의의 A까지 도달하면 논리 체계가 무너집니다. 경보 문장은 구조를 읽기 위한 치환일 뿐이며, 원전의 정리는 특정 경보 장치에 관한 주장이 아닙니다.

포괄 도식 x∈R ↔ (x∈x→A)에 x=R을 넣습니다. 그러면 R∈R ↔ (R∈R→A)를 얻습니다. R의 자기소속 문장이 자기소속을 전건으로 삼는 조건문과 서로 연결됩니다.

이 등가는 두 방향을 줍니다. 첫 방향은 R∈R에서 R∈R→A로 갑니다. 둘째 방향은 R∈R→A에서 R∈R로 갑니다. 커리 논증은 이 두 방향, 조건문의 modus ponens, 축약을 연결합니다.

modus ponens(MP)는 B와 B→C가 주어지면 C를 얻는 규칙입니다. 커리 고리에서 B를 R∈R, C를 A로 두면 R∈R과 R∈R→A가 함께 있을 때 A를 얻습니다.

포괄 등가 때문에 R∈R은 R∈R→A를 낳고, R∈R→A도 R∈R을 낳습니다. 한쪽 문장을 얻으면 MP에 필요한 두 전제를 마련할 수 있습니다. 축약은 이 반복되는 전제 사용을 하나의 조건문 안에서 압축하는 역할을 합니다.

축약(contraction)은 같은 전제를 여러 번 요구하는 증명을 한 번의 전제로 줄이는 구조 규칙입니다. 조건문 형태로는 B→(B→C)에서 B→C로 가는 추론이 대표적입니다. B가 두 번 나타나는 안쪽 조건을 한 번의 B 조건으로 줄입니다.

커리 구성에서는 자기소속 문장 B가 바깥 조건과 안쪽 조건에 반복됩니다. 축약이 유효하면 이 두 층을 접어 B→A를 얻고, 포괄 등가가 다시 B를 공급합니다. MP가 A까지 연결됩니다. 따라서 축약의 허용 여부가 붕괴 경로의 핵심 점검 대상입니다.

현재 언어에서 B→(B→A) ⊢ B→A가 성립하지 않는다는 사실은 중요한 출발점입니다. 하지만 새 기호나 새 진리값, 새 조건문을 보수적으로 더했을 때 같은 추론이 생길 수 있습니다. 순진한 집합 이론을 해석하는 과정 자체가 원래 언어를 확장할 수 있기 때문입니다.

레스털은 이 확장 뒤의 움직임을 확인합니다. 기본 언어에서 보이지 않던 중간값이나 조건문이 추가되어 축약 경로가 생기면, 원래 체계의 “축약 없음”만으로는 커리 붕괴를 막았다고 결론 내릴 수 없습니다.

확장 L⁺가 L에 대해 보수적이라는 말은, L의 언어로 적은 문장에 관해 L⁺가 새 정리를 만들어 내지 않는다는 뜻입니다. 새 기호와 구조를 사용하더라도 원래 언어의 증명 가능 관계를 함부로 늘리지 않습니다.

그래도 확장 언어 안에서는 새 식을 만들 수 있습니다. 축약의 안정성을 묻는 이유가 여기에 있습니다. 원래 언어의 결과를 보존하는 확장에서도 축약이 생기지 않아야, 언어를 넓히는 과정까지 포함해 축약에 견딘다고 말할 수 있습니다.

원문의 정의 3은 modus ponens와 A→A를 타당하게 하는 논리 L을 대상으로 합니다. 관련 조건을 만족하는 모든 보수적 확장에서 축약이 타당해지지 않을 때 L을 robustly contraction free라고 부릅니다. 이 글에서는 “확장에도 견디는 축약 없음”이라고 풀어 읽겠습니다.

정의에는 조건이 붙습니다. 원문은 A→(A→B)가 항상 최상값 T로 뭉개지지 않는 확장을 구별합니다. 축약의 전건 자체가 언제나 무의미하게 참이 되는 퇴화한 경우를 제외하고 실제 규칙의 안정성을 묻습니다.

원문은 기본 체계에서 축약이 타당하지 않아도, 보수적 확장에 수정된 물질조건문과 같은 표현을 넣으면 축약 경로가 생기는 무한 진리값 사례를 검토합니다. 표면적으로 축약이 없는 것과 확장에도 견디는 성질이 다르다는 점을 보여 줍니다.

따라서 평가 단위는 “현재 공리표에 축약 규칙이 적혀 있는가”에서 끝나지 않습니다. 조건문이 어떤 값을 돌려주는지, 지정된 진리값이 어떻게 보존되는지, 새 연산을 더한 보수적 확장에서 같은 추론이 생기는지까지 확인합니다.

정리 1은 유한한 드 모르간 격자에 기반한 값 의미론과 조건문을 다룹니다. 논문이 제시한 대수 조건, A→A의 타당성, modus ponens의 값 보존을 만족하는 비자명한 체계에서는 순진한 포괄을 지지하는 모형을 만들 수 없다는 방향의 결과를 제시합니다.

핵심은 진리값 수가 유한하다는 사실 하나가 아닙니다. 격자의 순서·부정·논리곱·논리합과 지정된 값들의 필터, 조건문의 값 조건이 함께 쓰입니다. 이 조건을 빼고 “모든 유한 다치논리는 실패한다”라고 넓히면 원문의 양화 범위를 넘어섭니다.

축약 실패는 커리 붕괴를 막기 위한 중요한 조건입니다. 하지만 집합의 동일성, 원소 관계, 포괄 도식 전체, 조건문의 추론, 비자명성이 함께 작동하는 모형을 따로 구성해야 합니다. 한 규칙이 실패한다는 정보만으로 필요한 모든 구조가 생기지는 않습니다.

원문은 관련 논리 RM과 진리 이론의 모형을 이용해 순진한 집합 이론 모형을 구성할 수 있는 방향을 설명합니다. 동시에 동일성의 성질과 배중·배제 관련 조건을 추가로 검토합니다. “축약 제거”와 “충분한 집합 이론 모형 존재”는 서로 다른 검수 항목입니다.

레스털은 RM에 기초한 산술적 진리 이론과 특정 물질조건문을 이용해 순진한 포괄을 해석하는 모형을 제시합니다. 이 예는 적절한 비고전 논리 구조에서 포괄 도식을 비자명하게 다룰 수 있음을 보여 줍니다.

원문은 그 모형이 곧바로 우리가 원하는 모든 집합론적 원리를 충족한다고 말하지 않습니다. 동일성에 관한 라이프니츠 법칙과 배제 성질을 함께 살피며, 어떤 추가 조건이 필요한지 구분합니다. 모형 존재와 강한 집합 이론 전체의 완성을 같은 결과로 세지 않습니다.

집합의 동일성을 정의하려면 두 대상이 같은 원소를 가지는지 비교합니다. 원문은 이렇게 정의한 동일성이 라이프니츠 법칙, 곧 동일한 대상을 식 안에서 서로 바꾸어도 진리값이 보존되는 성질을 갖는지 묻습니다.

이 단계에는 원소 관계에 관한 배제 성질이 추가로 필요할 수 있습니다. 포괄 도식의 모형이 존재한다는 사실과 동일성이 기대한 방식으로 작동한다는 사실을 나누어 확인해야 합니다. 독자는 “모형이 있다”라는 말의 범위를 이 두 층으로 읽어야 합니다.

추측 4는 “논리가 비자명한 순진한 집합 이론을 지지할 수 있는 것과 robustly contraction free인 것이 정확히 대응한다”라는 충분조건 방향까지 제안했습니다. 논문은 이 명제를 증명된 정리와 구분해 추측으로 표시합니다.

저자는 자신의 공개 페이지에서 이 추측이 1997년 모나시대학교 대학원생 샘 부카트와 수 로저슨의 연구로 틀렸음이 밝혀졌다고 정정합니다. 따라서 현재 글은 추측 4를 결론으로 사용하지 않습니다. 1993년의 문제 제기와 1997년의 반례를 같은 시간표에 놓습니다.

먼저 포괄 도식과 조건문의 정확한 범위를 적습니다. 다음으로 A→A, modus ponens, 축약의 성립 여부를 확인하고 커리 구성의 어느 단계가 멈추는지 표시합니다. 그 뒤 보수적 확장에서 같은 경로가 다시 생기는지 검사합니다.

마지막에는 실제 비자명한 모형, 동일성, 필요한 집합론 원리를 따로 확인합니다. robustly contraction free라는 성질만으로 충분조건을 선언하지 않습니다. 1993년 추측의 후속 반례가 이 마지막 경계를 분명하게 보여 줍니다.