분지 유형 이론

논리학에서 **분지 유형 이론**(分枝類型理論, , 약자 RTT) 또는 **복잡 유형 이론**(複雜類型理論)은 단순 유형 이론보다 더 세분된 유형을 사용하는 논리 체계이다.

## 정의
다음과 같은 데이터가 주어졌다고 하자. (여기서 \mathbb N은 음이 아닌 정수의 집합이다.)
* 최대 원소를 갖지 않는 가산 무한 정렬 전순서 집합 (\mathcal V,\le_{\mathcal V}). 그 원소를 **변수**(變數, )라고 한다.
* 집합 \mathcal A. 그 원소를 **개체**(個體, )라고 한다.
* 집합 \mathcal R 및 함수 \operatorname{arity}_{\mathcal R}\colon\mathcal R\to\mathbb N. 각 n\in \mathbb N에 대하여, \operatorname{arity}_{\mathcal R}^{-1}(n)의 원소를 **<math>n</math>항 관계**(n項關係, )라고 한다.
그렇다면, (\mathcal V,\le_{\mathcal V},\mathcal A,\mathcal R,\operatorname{arity}_{\mathcal R})에 대한 분지 유형 이론은 다음과 같다.

### 분지 유형
분지 유형 이론에서 사용되는 **분지 유형**(分枝類型, )과 이들의 **차수**(次數, )는 다음과 같다.
* \iota^0은 0차 분지 유형이다.
* d_1,\dots,d_n차 분지 유형 \tau_1^{d_1},\dots,\tau_n^{d_n} 및 자연수 d>\max\{d_1,\dots,d_n\}에 대하여, (\tau_1^{d_1},\dots,\tau_n^{d_n})^d는 d차 분지 유형이다.

이들 가운데, **술어적 분지 유형**(述語的分枝類型, )은 다음과 같다.
* \iota^0은 술어적 분지 유형이다.
* d_1,\dots,d_n차 술어적 분지 유형 \tau_1^{d_1},\dots,\tau_n^{d_n}에 대하여, (\tau_1^{d_1},\dots,\tau_n^{d_n})^{\max\{d_1,\dots,d_n\}+1}는 술어적 분지 유형이다. (n=0일 경우, ()^0은 술어적 분지 유형이다.)

술어적 분지 유형은 차수를 생략한 채 \iota와 (\tau_1,\dots,\tau_n)으로 쓸 수 있다.

분지 유형 이론의 **문맥**(文脈, )은 유한 개의 변수의 집합과 분지 유형의 집합 사이의 함수이다. 문맥은 변수 x와 분지 유형 \tau^d의 순서쌍 x{:}\tau^d들의 유한 집합으로 여길 수 있다. 이 경우, 문맥 \Gamma의 **[[정의역]]**(定義域, )은 다음과 같이 나타낼 수 있다.
:\operatorname{dom}(\Gamma)=\{x|x{:}\tau^d\in\Gamma\}

### 논리식
분지 유형 이론의 **유사 논리식**(類似論理式, )은 다음과 같다.
* n항 관계 R 및 변수 또는 개체 p_1,\dots,p_n에 대하여, R(p_1,\dots,p_n)은 유사 논리식이다.
** n=0일 경우 유사 논리식 R()은 0항 관계 R와 구분되어야 한다. 분지 유형 이론에서 n항 관계는 유사 논리식이 아니다.
* 변수 x 및 유한 개의 변수 또는 개체 또는 유사 논리식 p_1,\dots,p_n에 대하여, x(p_1,\dots,p_n)는 유사 논리식이다.
** n=0일 경우 유사 논리식 x()은 변수 x와 구분되어야 한다. 분지 유형 이론에서 변수나 개체는 유사 논리식이 아니다.
* 유사 논리식 \phi,\psi에 대하여, \phi\lor\psi와 \lnot\phi는 유사 논리식이다.
* 유사 논리식 \phi 및 그 자유 변수 x\in\operatorname{FVar}(\phi) 및 분지 유형 \tau^d에 대하여, \forall x{:}\tau^d\phi는 유사 논리식이다.
유사 논리식의 집합을 \mathcal P라고 하자. 또한 각 유사 논리식 \phi에 대하여, \operatorname{Var}(\phi)가 \phi 속에 등장하는 모든 변수의 집합이라고 하고,
:x_1^\phi
가 \phi의 모든 자유 변수라고 하자.

문맥 \Gamma에서 개체 또는 유사 논리식 \phi가 분지 유형 \tau^d를 갖는다는 것은 \Gamma\vdash\phi{:}\tau^d로 표기하며, 다음과 같이 재귀적으로 정의된다. (여기서 \vdash\phi{:}\tau^d는 \varnothing\vdash\phi{:}\tau^d를 뜻한다.)
* 개체 a에 대하여, \vdash a{:}\iota^0이다.
* n항 관계 R 및 개체 a_1,\dots,a_n에 대하여, \vdash R(a_1,\dots,a_n){:}()^1이다.
* (논리 연산) 문맥 \Gamma,\Delta 및 유사 논리식 \phi,\psi 및 분지 유형 (\tau_1^{d_1},\dots,\tau_n^{d_m})^d,({\tau_1'}^{d_1'},\dots,{\tau_n'}^{d_n'})^{d'}에 대하여, 만약 \Gamma\vdash\phi{:}(\tau_1^{d_1},\dots,\tau_n^{d_m})^d이며, \Delta\vdash\psi{:}({\tau_1'}^{d_1'},\dots,{\tau_n'}^{d_n'})^{d'}이며, \max\operatorname{dom}(\Gamma)라면,
}}이다.
* (한정) 문맥 \Gamma 및 유사 논리식 \phi 및 i\in\{1,\dots,|{\operatorname{FVar}(\phi)}|\} 및 분지 유형 (\tau_1^{d_1},\dots,\tau_n^{d_n})^d에 대하여, 만약 \Gamma\cup\{x_i^\phi{:}\tau_i^{d_i}\}\vdash\phi{:}(\tau_1^{d_1},\dots,\tau_n^{d_n})^d라면,,\tau_{i+1}^{d_{i+1}},\dots,\tau_n^{d_n})^d
}}이다.
* (매개 변수에 대한 추상화) 문맥 \Gamma 및 유사 논리식 \phi 및 그 개체이거나 유사 논리식인 매개 변수 \psi\in\operatorname{Par}(\phi)\cap(\mathcal A\cup\mathcal P) 및 분지 유형 (\tau_1^{d_1},\dots,\tau_n^{d_n})^d,\tau_{n+1}^{d_{n+1}} 및 변수 y>\max\operatorname{dom}(\Gamma)에 대하여, 만약 \Gamma\vdash\phi{:}(\tau_1^{d_1},\dots,\tau_n^{d_n})^d이며 \Gamma\vdash\psi{:}\tau_{n+1}^{d_{n+1}}이라면,\}|x\in\operatorname{Var}((\phi)_{\Gamma,\psi,y})\}
\vdash (\phi)_{\Gamma,\psi,y}{:}(\tau_1^{d_1},\dots,\tau_{n+1}^{d_{n+1}})^{\max\{d,d_{n+1}+1\}}
}}이다. 여기서 (\phi)_{\Gamma,\psi,y}는 \phi에 등장하는 \psi와 αΓ-동치인 각 매개 변수 \psi'를 y로 대체하여 얻는 유사 논리식이다. (《수학 원리》에서 이는 (\tau_1^{d_1},\dots,\tau_n^{d_n})^d가 술어적 분지 유형인 경우로 제한된다.)
* (논리식에 대한 추상화) 문맥 \Gamma 및 유사 논리식 \phi 및 분지 유형 (\tau_1^{d_1},\dots,\tau_n^{d_n})^d 및 변수 y>\max\operatorname{dom}(\Gamma)에 대하여, 만약 \Gamma\vdash\phi{:}(\tau_1^{d_1},\dots,\tau_n^{d_n})^d이라면,이다. (이 경우 반드시 =n임을 보일 수 있다.) (《수학 원리》에서 이는 (\tau_1^{d_1},\dots,\tau_n^{d_n})^d가 술어적 분지 유형인 경우로 제한된다.)
* (치환) 문맥 \Gamma 및 자유 변수를 갖는 유사 논리식 \phi 및 개체 또는 유사 논리식 \psi 및 분지 유형 (\tau_1^{d_1},\dots,\tau_n^{d_n})^d에 대하여, 만약 \Gamma\cup\{x_1^\phi{:}\tau_1^{d_1}\}\vdash\phi{:}(\tau_1^{d_1},\dots,\tau_n^{d_n})^d이며, \Gamma\vdash\psi{:}\tau_1^{d_1}라면,이다. (이 경우 \phi[\psi/x_1^\phi]는 반드시 정의됨을 보일 수 있다.)
* (약화) 문맥 \Gamma,\Delta 및 유사 논리식 \phi 및 분지 유형 \tau^d에 대하여, 만약 \Gamma\vdash\phi{:}\tau^d이며, \Gamma\subseteq\Delta라면, \Delta\vdash\phi{:}\tau^d이다.
* (순열) 문맥 \Gamma 및 유사 논리식 \phi 및 i\in\{1,\dots,|{\operatorname{FVar}(\phi)}|\} 및 분지 유형 (\tau_1^{d_1},\dots,\tau_n^{d_n})^d 및 변수 y>\max\operatorname{dom}(\Gamma)에 대하여, 만약 \Gamma\cup\{x_i^\phi{:}\tau_i^{d_i}\}\vdash\phi{:}(\tau_1^{d_1},\dots,\tau_n^{d_n})^d라면,,\tau_{i+1}^{d_{i+1}},\dots,\tau_n^{d_n},\tau_i^{d_i})^d
}}이다.

주어진 문맥 속에서, 유사 논리식의 분지 유형은 존재하지 않을 수 있으나, 만약 존재한다면 이는 유일하다. 주어진 유사 논리식은 서로 다른 문맥 속에서 서로 다른 분지 유형을 가질 수 있다. 유사 논리식 \phi에 대하여, \Gamma\vdash\phi{:}\tau^d인 문맥 \Gamma과 \tau^d가 존재한다면, \phi를 **[[논리식]]**(論理式, )이라고 한다.

## 연산
### 자유 변수, 매개 변수, 재귀 매개 변수
분지 유형 이론의 각 유사 논리식 \phi의 **[[자유 변수]]**(自由變數, )의 집합 \operatorname{FVar}(\phi), **매개 변수**(媒介變數, )의 집합 \operatorname{Par}(\phi), **재귀 매개 변수**(再歸媒介變數, )의 집합 \operatorname{RPar}(\phi)은 다음과 같이 재귀적으로 정의된다. (매개 변수와 재귀 매개 변수는 이름과 달리 변수가 아닐 수 있다.)
* n항 관계 R 및 변수 또는 개체 p_1,\dots,p_n에 대하여,
* 변수 x 및 유한 개의 변수 또는 개체 또는 유사 논리식 p_1,\dots,p_n에 대하여,\operatorname{RPar}(\phi)
}}
* 유사 논리식 \phi,\psi에 대하여,
* 유사 논리식 \phi 및 그 자유 변수 x\in\operatorname{FVar}(\phi)에 대하여,

### 치환
변수 또는 개체 또는 유사 논리식 p,q_1,\dots,q_k 및 서로 다른 변수 x_1,\dots,x_k에 대하여,
:p\langle q_1/x_1,\dots,q_k/x_k\rangle=\begin{cases}
p&p\not\in\{x_1,\dots,x_k\} \\
q_j&p=x_j
\end{cases}
이라고 하자.

유사 논리식 \phi 및 변수 또는 개체 또는 유사 논리식 q_1,\dots,q_k 및 서로 다른 변수 x_1,\dots,x_k에 대하여, **[[치환 실례]]**(置換實例, ) \phi[q_1/x_1,\dots,q_k/x_k]는 다음과 같이 재귀적으로 정의된다.
* n항 관계 R 및 변수 또는 개체 p_1,\dots,p_n,q_1,\dots,q_k 및 서로 다른 변수 x_1,\dots,x_k에 대하여,
* 변수 x 및 및 변수 또는 개체 또는 유사 논리식 p_1,\dots,p_n,q_1,\dots,q_k 및 서로 다른 변수 x_1,\dots,x_k에 대하여,
* 유사 논리식 \phi,\psi 및 변수 또는 개체 또는 유사 논리식 q_1,\dots,q_k 및 서로 다른 변수 x_1,\dots,x_k에 대하여,
* 유사 논리식 \phi 및 그 자유 변수 x\in\operatorname{FVar}(\phi) 및 분지 유형 \tau^d 및 변수 또는 개체 또는 유사 논리식 q_1,\dots,q_k 및 서로 다른 변수 x_1,\dots,x_k에 대하여,
위 경우에 속하지 않는 치환 실례는 정의되지 않는다. 예를 들어, 변수 또는 개체 또는 유사 논리식 p_1,\dots,p_n,q_1,\dots,q_k 및 서로 다른 변수 x_1,\dots,x_k에 대하여, 만약 q_i\in\mathcal A이거나, q_i\in\mathcal P이며 q_i의 자유 변수가 정확히 n개가 아닐 경우, x_i(p_1,\dots,p_n)[q_1/x_1,\dots,q_k/x_k]는 정의되지 않는다.

### α-동치
두 유사 논리식 \phi,\psi에 대하여, 다음 조건을 만족시키는 전단사 함수 f\colon\mathcal V\to\mathcal V가 존재한다면, \phi,\psi가 서로 **α-순열 동치**(α-順列同値, )라고 한다.
* \psi는 \phi에 등장하는 각 변수 x를 f(x)로 대체하여 얻는다. (특히, f(\operatorname{Var}(\phi))=\operatorname{Var}(\psi)이다.)

두 유사 논리식 \phi,\psi에 대하여, 다음 두 조건을 만족시키는 전단사 함수 f\colon\mathcal V\to\mathcal V가 존재한다면, \phi,\psi가 서로 **α-동치**(α-同値, )라고 한다.
* \psi는 \phi에 등장하는 각 변수 x를 f(x)로 대체하여 얻는다. (특히, f(\operatorname{Var}(\phi))=\operatorname{Var}(\psi)이다.)
* f|_{\operatorname{Var}(\phi)}는 증가 함수이다. 즉, 임의의 x,y\in\operatorname{Var}(\phi)에 대하여, x

두 유사 논리식 \phi,\psi 및 문맥 \Gamma에 대하여, 다음 세 조건을 만족시키는 전단사 함수 f\colon\mathcal V\to\mathcal V가 존재한다면, \phi,\psi가 서로 **α<sub>Γ</sub>-동치**(αΓ-同値, )라고 한다.
* \psi는 \phi에 등장하는 각 변수 x를 f(x)로 대체하여 얻는다. (특히, f(\operatorname{Var}(\phi))=\operatorname{Var}(\psi)이다.)
* f|_{\operatorname{Var}(\phi)}는 증가 함수이다. 즉, 임의의 x,y\in\operatorname{Var}(\phi)에 대하여, x
* 임의의 x\in\mathcal V 및 분지 유형 \tau^d에 대하여, x{:}\tau^d\in\Gamma\iff f(x){:}\tau^d\in\Gamma

## 역사
버트런드 러셀이 《수학 원리》에서 제시하였다.

## 각주

* 
* 
* 

분류:유형 이론