컷을 직접 지우지 않고도, 컷 없는 증명이 있다고 보일 수 있을까요?

유형은 대상이 어떤 종류의 입력을 받고 어떤 층에 놓이는지 구분합니다. 형 0에는 개체식이 놓이고, 명제 수준에는 참과 거짓을 가르는 식이 놓입니다. 더 높은 형의 식은 더 낮은 형의 대상들을 받아 관계나 함수처럼 작동합니다.

이 구분이 필요한 이유는 자기 자신을 제한 없이 논항으로 받는 식을 막으면서도, 개체에 관한 성질·성질에 관한 성질을 표현하기 위해서입니다. 논문은 유형을 자연수와 괄호의 재귀적 구조로 다루며, 각 높은 유형의 의미 대상을 바로 아래 유형의 대상들로부터 만듭니다.

다카하시의 V-complex는 대략 [식, 의미 대상]의 두 칸으로 이루어집니다. 첫째 칸은 어떤 식에서 왔는지를 보존하고, 둘째 칸은 그 식이 의미론에서 가리키는 값을 담습니다. 형 0에서는 [e⁰,0] 같은 쌍을 만들고, 명제 수준에서는 반가치와 맞는 참·거짓 표지를 붙입니다.

높은 형에서는 둘째 칸이 단순한 참·거짓이 아닙니다. 낮은 형의 V-complex들로 만든 집합이나 관계가 들어갑니다. 그래서 람다 추상처럼 함수를 만드는 식도, 논항을 넣었을 때 어떤 값이 나오는지 의미론적으로 추적할 수 있습니다.

아래 실험은 원문의 재귀 정의를 세 층으로 단순화해 보여 줍니다. 형 0에서는 개체식과 고정 표지 0을 짝짓고, 명제 수준에서는 진리 표지를 붙이며, 높은 형에서는 낮은 층의 복합체들 사이 관계를 둘째 부분에 둡니다.

버튼을 누를 때마다 위층이 아래층을 재료로 삼는다는 점을 확인해 보세요. 실제 논문은 각 유형마다 허용되는 복합체가 존재한다는 보조정리 1.5를 따로 증명합니다.

논문이 쓰는 semi-valuation, 곧 반가치는 모든 복합식의 값을 처음부터 완전히 정하는 표가 아닙니다. 증명 규칙과 양립하도록 필요한 원자적·부분적 정보를 주고, 그 위에서 식의 의미를 재귀적으로 확장하는 장치입니다.

이 장치는 마지막 반증법에서 결정적입니다. 어떤 끝식을 컷 없이 유도할 수 없다면, 슈테의 결과를 이용해 그 식을 거짓으로 만드는 반가치를 얻습니다. 다카하시는 그 반가치 위에 V-complex와 대응을 쌓아, 유도 가능한 식은 반드시 참이어야 한다는 보조정리와 충돌시킵니다.

V-correspondence는 자유변수 각각에 같은 유형의 V-complex를 대응시킵니다. 다카하시는 이 대응을 모든 식으로 재귀적으로 확장합니다. 확장된 값의 첫째 부분은 변수 자리에 해당 복합체의 식을 넣은 결과이고, 둘째 부분은 그렇게 얻은 식의 의미 값입니다.

변수·논리상수·적용·부정·선언·존재양화·람다 추상마다 재귀 절이 따로 있습니다. 따라서 “치환한 문법 결과”와 “그 결과의 의미”가 같은 계산 안에서 함께 움직입니다. 이 두 부분을 분리하지 않으면 높은 형의 치환과 의미 평가가 서로 맞는지 증명하기 어렵습니다.

부정은 안쪽 식의 값을 뒤집고, 선언은 두 식 가운데 적어도 하나가 참일 때 참으로 읽습니다. 존재양화는 적절한 유형의 V-complex를 변수에 대응했을 때 본문 식이 참이 되는 경우가 하나라도 있는지를 묻습니다.

중요한 점은 이 절들이 단순한 진리표 나열이 아니라는 사실입니다. 각 절은 첫째 부분에서 식을 치환하고, 둘째 부분에서 그 치환이 반가치와 일치하도록 만듭니다. 특히 양화는 모든 가능한 낮은 유형 복합체를 순회하는 조건이므로, 높은 유형의 의미 영역이 제대로 준비되어 있어야 합니다.

λ α₁…αₙ . A는 논항을 받아 A를 만드는 함수식입니다. 다카하시는 이 식의 둘째 부분을, 각 논항 위치에 낮은 형의 V-complex를 넣었을 때 A가 어떤 값을 갖는지를 모은 관계로 정의합니다. 높은 형의 의미를 막연한 “함수”라고 부르지 않고, 낮은 층의 복합체 위에서 실제로 작동하는 관계로 펼친 셈입니다.

보조정리 3.5의 핵심 귀결은 람다 추상에 논항을 적용한 값이, 본문 A에 그 논항을 치환해 얻은 값과 맞는다는 것입니다. 이 합치가 있어야 높은 형의 식을 의미론으로 옮긴 뒤에도 치환 규칙이 흔들리지 않습니다.

그렇지 않습니다. 비구성적이라는 말은 결론이 약하다는 뜻이 아니라, 결론에 도달하는 방식이 특정 산출물을 직접 만들어 주지 않는다는 뜻입니다. 이 논문은 “유도 가능한 식에는 컷 없는 유도가 존재한다”는 정리를 증명합니다.

다만 입력으로 컷이 있는 증명 하나를 받아 어떤 국소 변환을 순서대로 적용해야 하는지 알려 주지는 않습니다. 아래 비교에서 다카하시 방식을 선택하면, 반모형이 생길 수 없다는 논증으로 존재를 확보하는 구조가 나타납니다.

보조정리 3.2는 한 식의 값이 그 식에 실제로 나타나는 유한한 자유변수들의 대응에만 의존함을 보입니다. 식 밖의 변수에 어떤 복합체를 붙이든 결과는 달라지지 않습니다. 이는 의미 평가가 통제 가능한 국소 계산임을 뜻합니다.

이어지는 보조정리 3.4와 3.5는 대응을 바꾸는 일과 식에 직접 치환하는 일이 서로 맞는다는 점을 밝힙니다. 이 유한 의존성은 부록 2에서도 다시 쓰입니다. 전체 함수를 하나의 집합으로 갖지 않아도, 특정 식을 평가하는 데 필요한 유한한 부분만 집합으로 다루면 충분하기 때문입니다.

다카하시는 식 안에서 어떤 부분식이 양의 위치에, 어떤 부분식이 음의 위치에 나타나는지를 재귀적으로 정의합니다. 부정 안으로 들어가면 극성이 뒤집히고, 선언이나 양화 안에서는 해당 위치의 극성이 이어집니다.

보조정리 3.7과 3.8은 이 극성 정보와 진리값 사이의 전달 규칙을 줍니다. 양의 명시적 부분이 참이거나 음의 명시적 부분이 거짓인 조건이 전체 식의 값과 어떻게 연결되는지 보여, 뒤의 유도 규칙별 건전성 검사를 가능하게 합니다.

보조정리 4.1은 식 F가 체계에서 유도 가능하다면, 어떤 V-correspondence와 허용된 반가치 아래에서도 F의 둘째 의미 성분이 참이라고 말합니다. 다카하시는 유도의 길이에 대한 귀납법으로 이를 증명하며, 시작식과 각 추론 규칙이 참을 보존하는지 차례로 확인합니다.

이 명제는 컷 제거 자체가 아닙니다. 구문 쪽의 “유도 가능”을 의미 쪽의 “모든 해석에서 참”으로 옮기는 건전성 다리입니다. 마지막 단계에서는 이 다리와, 컷 없는 유도가 없을 때 얻는 거짓 반해석이 정면으로 충돌합니다.

식 F가 유도 가능하지만 엄격 유도, 곧 컷 없는 유도는 없다고 가정합니다. 슈테의 결과를 적용하면 F를 거짓으로 만드는 반가치를 얻습니다. 이어 각 자유변수의 첫째 부분이 그 변수 자신이 되도록 V-correspondence를 잡으면, F의 둘째 부분도 거짓이 됩니다.

하지만 F가 유도 가능하다는 첫 가정에 보조정리 4.1을 적용하면 같은 둘째 부분은 참이어야 합니다. 하나의 값이 동시에 참과 거짓이어야 하는 모순이 생기므로, “유도 가능하지만 컷 없는 유도는 없다”는 조합은 불가능합니다. 따라서 유도 가능한 모든 F에는 컷 없는 유도가 존재합니다.

부록 1에서 다카하시는 같은 방법이 GLC나 다른 단순 유형 이론의 수정 체계에도 직접 적용된다고 적습니다. 본문의 형식화 대상은 단순 유형 이론이며, 국가나 시대 전체의 논리 성향을 대표하는 주장은 아닙니다. 이 회차의 ‘일본편’ 표지는 일본 수학계에서 발표된 이 연구의 기관·출판 맥락을 가리킵니다.

부록 2는 증명이 선택공리나 대체공리 없이 체르멜로 집합론 안에서 형식화될 수 있다고 설명합니다. 특정 식은 유한한 자유변수 대응값에만 의존하므로 필요한 대응의 유한 부분을 집합으로 취급할 수 있습니다. 동시에 괴델의 결과를 근거로, 이 핵심 논증 전체가 지나치게 약한 유한주의적 틀로 환원될 수는 없다고 한계를 긋습니다.

따라서 이 논문의 힘은 높은 형의 컷 제거를 의미론적 존재 정리로 세운 데 있습니다. 후속 과제는 컷 없는 증명을 실제로 산출하는 변환, 증명 길이와 계산 복잡도, 더 강한 체계에서 필요한 증명론적 강도를 따로 분석하는 일입니다.