필요한 함수만 낮은 층으로 옮길 수 있을까요?

러셀식 ramified type theory는 어떤 정의가 자신과 같은 높이 또는 더 높은 전체를 다시 양화해 불러들이는 일을 제한합니다. 팔름그렌의 IRTT는 단위원 1, 자연수 N, 곱 A×B, 제한된 멱집합 Pₙ(A)로 타입을 만듭니다.

Pₙ(A)는 A 위의 level-n 명제함수, 곧 level-n 부분집합을 담습니다. {x:A | φ}가 Pₖ(A)의 항이 되려면 φ∈Form(k)여야 합니다. Pₙ(S)에 대한 양화를 φ 안에 넣으려면 |Pₙ(S)|=max(n+1,|S|)≤k가 필요합니다. 따라서 n<k는 필요하지만 그것만으로 충분하지 않고, 바탕 타입 S의 level도 k 이하이어야 합니다. 한편 b:Pₙ(A)에 대한 membership a∈b는 n≤k이면 level k에서 쓸 수 있습니다.

원문은 타입 A에 두 수치 |A|와 ||A||를 둡니다. |A|는 타입을 해석할 universe의 높이이고, ||A||는 그 타입의 동일성을 표현하는 공식의 높이입니다. 재귀식은 다음과 같습니다.

• |1|=|N|=0, |A×B|=max(|A|,|B|), |Pₙ(A)|=max(n+1,|A|).
• ||1||=||N||=0, ||A×B||=max(||A||,||B||), ||Pₙ(A)||=max(n,|A|).

두 눈금이 실제로 갈리는 예를 계산해 봅시다. C=N×P₀(1)이면 |C|=max(0,1)=1, ||C||=max(0,0)=0입니다. 여기에 P₂를 한 번 더 씌우면 |P₂(C)|=max(3,1)=3, ||P₂(C)||=max(2,1)=2가 됩니다. 같은 타입에서도 “타입이 사는 높이”와 “동일성을 말하는 높이”가 다를 수 있습니다.

공식 φ∈Form(k)에 타입 A의 변수 x가 자유롭게 나타날 수 있을 때, set abstraction {x:A | φ}는 그 자유로운 x들을 결속해 Pₖ(A)의 항을 만듭니다. 정의 공리의 φ[z/x]는 자유로운 x만 같은 타입의 항 z로 바꾸며, 다른 결속 변수에 포획되지 않게 치환합니다.

Form(k) 판정에는 구체적인 층 조건이 있습니다. a =_A b를 쓰려면 |A|≤k, a∈b에서 b:Pₙ(A)이면 n≤k, ∀x:A나 ∃x:A를 쓰려면 |A|≤k여야 합니다. 연결사로 묶는 두 공식도 같은 Form(k) 안에 있어야 합니다. 따라서 “어떤 문장도 원하는 낮은 층에서 집합을 만든다”는 규칙이 아닙니다. 공식의 equality·membership·양화 범위를 먼저 계산한 뒤 k가 정해집니다.

full reducibility는 높은 층의 임의 부분집합과 외연적으로 같은 0층 부분집합이 존재한다고 말합니다. 이렇게 되면 부분집합이 어느 층에서 정의되었는지 외연적으로 구별할 수 없게 되고, 역설을 막으려고 만든 층화가 무너집니다.

러셀은 실수 체계 같은 수학 구성을 위해 reducibility를 도입했지만, 팔름그렌은 이 조치가 체계를 impredicative하게 만든다고 설명합니다. 논문의 목표는 필요한 수학적 함수 구성을 확보하면서 모든 층을 붕괴시키지 않는 제한된 원리를 찾는 것입니다.

바탕 타입은 A=B=N이고, 정의역 부분집합은 X={0,1,2}, 공역 부분집합은 Y={0,2,4}입니다. 동일성은 자연수의 보통 동일성입니다. 따라서 (3,4)도 바탕 타입 N×N의 쌍으로는 적법하며, 아래에서는 이 쌍이 X×Y의 범위에 들어가는지를 따로 검사합니다.

• 관계 A (0,0),(1,2),(2,4): 모든 쌍이 정의역×공역 안에 있고, 각 입력에 출력이 정확히 하나이므로 map입니다.
• 관계 B (0,0),(2,4): 입력 1의 출력이 없어 totality가 실패합니다.
• 관계 C (0,0),(1,2),(1,4),(2,4): 입력 1에 서로 다른 출력 2와 4가 붙어 functionality가 실패합니다.
• 관계 D (0,0),(1,2),(2,4),(3,4): 3이 정의역 밖이므로 relation의 strictness 가운데 정의역 조건이 실패합니다.

버튼은 판정과 함께 어느 쌍·어느 입력에서 조건이 깨졌는지 보여 줍니다.

local set은 (A,X,n)이라는 세 항으로 적습니다. A는 바탕 타입, X:Pₙ(A)는 A의 어느 원소를 포함할지 정하는 부분집합, n은 X의 층입니다.

자연수 전체의 local set은 ℕ=(N,{x:N | ⊤},0)입니다. 바탕 타입은 자연수이고, 항상 참인 조건이 모든 자연수를 포함하며, 조건은 0층입니다. 같은 바탕 타입 A라도 X와 n이 다르면 다른 local set을 이룹니다.

원문에서 정의역 local set은 (A,X,m), 공역 local set은 (B,Y,n)입니다. IRTT에서는 먼저 R:Pᵣ(A×B)인 relation이 주어집니다. 논리의 equality 공리는 이런 predicate가 타입의 동일성을 존중하도록 요구합니다. 이 relation이 map이 되기 위해 추가로 확인하는 조건은 세 가지입니다. R(⟨a,b⟩)이면 a∈X와 b∈Y가 따라야 하는 strictness, 모든 a∈X에 대해 R(⟨a,b⟩)가 성립하는 어떤 b∈Y가 있어야 하는 totality, R(⟨a,b⟩)와 R(⟨a,c⟩)이면 b=_B c여야 하는 functionality입니다. setoid 모델에서는 F:[A×B→Ωᵣ]라는 표기 자체가 외연성 증명을 포함합니다.

존재와 유일성을 ∃!로 압축할 수 있지만, 화면에서는 세 조건을 나눠 보여 줍니다. 그래야 “쌍이 범위 밖이다”, “입력이 비었다”, “출력이 갈라진다”를 구별할 수 있습니다.

편집부 사례로 d(x)=2x의 그래프 D={⟨x,y⟩:N×N | y=2x}를 생각합니다. 자연수의 산술식은 0층에서 쓸 수 있으므로 D:P₀(N×N)입니다. 화면에 보이는 (0,0),(1,2),(2,4),(3,6)은 이 전체 그래프의 네 표본입니다.

이 예에서 relation 자체가 이미 0층이므로 “높은 relation을 낮췄다”는 비자명한 예는 아닙니다. 대신 map의 전제를 읽는 연습에 쓰입니다. 모든 자연수 x에 2x가 존재해 totality를 얻고, y=2x와 z=2x이면 y=z여서 functionality를 얻습니다. 표의 네 행만으로 전 범위 조건을 증명했다고 말하지 않습니다.

IRTT의 공리와 setoid 모델의 정리는 기호 역할이 다릅니다. IRTT에서는 X:Pₘ(A), Y:Pₙ(B), F:Pᵣ(A×B)가 (A,X,m)에서 (B,Y,n)로 가는 map이면 k=max(||B||,m,n)에 놓인 G:Pₖ(A×B)를 얻고, 모든 a,b에서 F(⟨a,b⟩)↔G(⟨a,b⟩)가 성립합니다. 원래 relation의 층 r은 목표 k의 최대값 항이 아닙니다.

정리 3.3의 모델 표기에서는 A가 (m,n)-setoid, B가 (m′,n′)-setoid이고, X와 Y의 predicate 층을 각각 k,k′라고 둡니다. 이때 목표는 ℓ=max(k,k′,n′)입니다. 여기서 n′은 공역 setoid의 equality universe입니다. 두 표기를 나란히 놓으면 “두 local predicate 층+공역 동일성 층”이라는 같은 구조가 보입니다.

이 활동은 정리 3.3의 모델 표기 ℓ=max(k,k′,n′)를 씁니다.

• k=2,k′=1,n′=0 → ℓ=2. 정의역 predicate 층이 최대이다.
• k=1,k′=3,n′=2 → ℓ=3. 공역 predicate 층이 최대이다.
• k=0,k′=0,n′=2 → ℓ=2. 공역 equality 층을 빼면 안 된다.
• k=0,k′=1,n′=2,r=7 → ℓ=2. 원래 map F의 relation 층 r=7은 목표 최대값에 들어가지 않는다.

각 버튼은 ℓ=max(k,k′,n′)의 계산식과 최대값을 만든 항을 표시합니다. 이어 “F가 정리 3.3의 typed map 전제를 충족한다면, 정리는 모든 a:A, b:B에 대해 F(⟨a,b⟩)↔G(⟨a,b⟩)인 G:[A×B→Ωℓ]의 존재를 보장합니다”라고 조건부 결론을 보여 줍니다. 수치 선택만으로 map 전제나 외연적 동치를 증명하지 않습니다. 네 결과에는 목표 층 계산: ℓ=…이라는 제목, 실제 최대값 계산, F가 정리 3.3의 typed map이어야 한다는 적용 조건과 그때의 존재 결론이 함께 표시됩니다.

논문은 IRTT의 타입과 공식을 무한한 universe 열을 가진 Martin-Löf type theory의 setoid와 타입으로 해석합니다. 각 타입 A는 (|A|,||A||)-setoid로 옮겨지고, level-n 공식은 universe Uₙ의 타입으로 해석됩니다.

정리 3.3은 이 해석 안에서 functional map의 그래프를 계산된 낮은 universe 층으로 옮깁니다. 정리 3.4는 IRTT에 Relativized Dependent Choice를 더한 IRTT+RDC가 그 Martin-Löf type theory 안에서 해석된다고 결론냅니다. 논문의 predicative 정당화는 이 해석 범위에 놓입니다.

§4는 local set과 map으로 범주를 만들고, 실수, 몫, 곱, 지수, equalizer, characteristic function을 구성합니다. Functional Reducibility Axiom은 같은 외연적 함수를 필요 이상으로 높은 층에 계속 복제하지 않게 해 줍니다.

논문은 실수의 여러 표현 층이 끝없이 늘어나는 문제를 다루는 데 이 제한이 충분하다고 설명합니다. 다만 IRTT 자체를 실용적인 형식화 언어로 제시하지는 않습니다. 층 번호가 붙은 표기가 매우 번거롭고, 현대 Martin-Löf형 증명 보조기에 임베드할 수 있는 이론적 전시물로 성격을 밝힙니다.

정리 5.1은 PEM, 곧 φ∨¬φ를 가정하면 full reducibility가 따라온다는 결과입니다. X:Pₖ(A)에 대해 원문은 F(⟨x,n⟩) ↔ (x∈X ∧ n=1) ∨ (¬(x∈X) ∧ n=0)으로 A에서 N으로 가는 관계를 만듭니다.

PEM은 각 x에 대해 x∈X 또는 ¬(x∈X)를 골라 출력 1 또는 0이 존재함을 보이는 totality 단계에 쓰입니다. 두 경우가 동시에 성립할 수 없고 자연수 0과 1이 구별되므로 functionality도 얻습니다. Functional Reducibility Axiom을 적용하면 이 함수와 외연적으로 같은 G:P₀(A×N)를 얻습니다. 마지막으로 Y={x:A | ⟨x,1⟩∈G}를 만들면 Y:P₀(A)이고 x∈X↔x∈Y입니다.

논문이 세운 범위는 IRTT와 Functional Reducibility Axiom, 필요할 때의 RDC를 Martin-Löf type theory의 누적 universe 계층에 해석하는 것입니다. 각 타입 S를 (|S|,||S||)-setoid로 해석하고, level-k 공식을 Uₖ 안의 타입으로 해석한 뒤, 정리 3.3으로 FR의 타당성을 보입니다. 저자는 이 배경 이론을 Feferman–Schütte의 증명론적 의미에서 predicative한 체계로 놓습니다.

따라서 결론은 “이 특정 해석이 IRTT+FR의 predicative 정당화를 준다”입니다. 모든 직관주의 체계가 자동으로 predicative하다는 일반 명제도, 고전논리를 쓰는 모든 체계가 곧 역설적이라는 명제도 아닙니다. PEM을 추가하면 정리 5.1의 full reducibility가 따라온다는 사실은, 이 논문 안에서 구성적 논리 전제가 층화 유지에 실제 역할을 한다는 경계를 보여 줍니다.

앞에서 살펴본 관계표와 층 계산을 함께 적용해 보겠습니다. 관계쌍이 허용된 범위에 있는지, 모든 입력에 출력이 있는지, 그 출력이 유일한지를 확인해야 목표 층 계산을 정리의 결론과 연결할 수 있습니다. 아래 항목은 서로 다른 가정을 놓고 비교한 경우입니다. map의 전제가 실패하는 경우와 배중률을 추가하는 경우, 논문이 후속 과제로 남긴 경우를 각각 구분해 읽습니다.

• 조건 A · typed map: A와 B가 지정된 setoid이고 F:[A×B→Ωᵣ]가 strict·total·functional하며 k=2,k′=1,n′=0이면, 정리 3.3의 전제를 충족하고 ℓ=max(2,1,0)=2입니다.
• 조건 B · 출력 누락: 입력 1의 출력이 없으므로 totality가 실패하고 Functional Reducibility를 적용할 수 없습니다.
• 조건 C · 출력 갈림: 입력 1에 서로 같지 않은 출력 2와 4가 붙어 functionality가 실패합니다.
• 조건 D · 범위 밖 쌍: strictness가 실패합니다. totality와 functionality만 통과해도 map으로 세지 않습니다.
• 조건 E · 외연성 실패: equality로 같은 입력·출력에서 관계값이 보존되지 않아 F:[A×B→Ωᵣ]의 타입 전제부터 충족하지 못합니다.
• 조건 F · PEM 추가: 임의의 X:Pₖ(A)에 대해 정리 5.1의 Y:P₀(A)가 따라오며, PEM은 0/1 관계의 totality 증명에 쓰입니다.
• 조건 G · topos 완성: 원문은 predicative elementary topos를 후속 방향으로 제안하지만 완성된 정리로 제시하지 않습니다.