분지 유형 이론

논리학에서 **분지 유형 이론**(分枝類型理論, ramified type theory, 약자 RTT) 또는 **복잡 유형 이론**(複雜類型理論)은 단순 유형 이론보다 더 세분된 유형을 사용하는 논리 체계이다.jstor=20015876doi=10.1007/1-4020-2335-9Chapter 2
# 정의
다음과 같은 데이터가 주어졌다고 하자. (여기서 \mathbb N은 음이 아닌 정수의 집합이다.) * 최대 원소를 갖지 않는 가산 무한 정렬 전순서 집합 (\mathcal V,\le_{\mathcal V}). 그 원소를 **변수**(變數, variable)라고 한다. * 집합 \mathcal A. 그 원소를 **개체**(個體, individual)라고 한다. * 집합 \mathcal R 및 함수 \operatorname{arity}_{\mathcal R}\colon\mathcal R\to\mathbb N. 각 n\in \mathbb N에 대하여, \operatorname{arity}_{\mathcal R}^{-1}(n)의 원소를 **n항 관계**(n項關係, n-ary relation)라고 한다. 그렇다면, (\mathcal V,\le_{\mathcal V},\mathcal A,\mathcal R,\operatorname{arity}_{\mathcal R})에 대한 분지 유형 이론은 다음과 같다.
## 분지 유형
분지 유형 이론에서 사용되는 **분지 유형**(分枝類型, ramified type)과 이들의 **차수**(次數, order)는 다음과 같다. * \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차 분지 유형이다. 이들 가운데, **술어적 분지 유형**(述語的分枝類型, predicative ramified type)은 다음과 같다. * \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)으로 쓸 수 있다. 분지 유형 이론의 **문맥**(文脈, context)은 유한 개의 변수의 집합과 분지 유형의 집합 사이의 함수이다. 문맥은 변수 x와 분지 유형 \tau^d의 순서쌍 x{:}\tau^d들의 유한 집합으로 여길 수 있다. 이 경우, 문맥 \Gamma의 **정의역**(定義域, domain)은 다음과 같이 나타낼 수 있다. :\operatorname{dom}(\Gamma)=\\{x|x{:}\tau^d\in\Gamma\\}
## 논리식
분지 유형 이론의 **유사 논리식**(類似論理式, pseudoformula)은 다음과 같다. * 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\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이라면,mindent| \\{x{:}\tau^d\in\Gamma\cup\\{y{:}\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이라면,mindent| \\{x{:}\tau^d\in\Gamma\cup\\{y{:}(\tau_1^{d_1},\dots,\tau_n^{d_n})^d\\}|x\in\operatorname{FVar}(\phi)\cup\\{y\\}\\} \vdash y(x_1^\phi,\dots,x_n^\phi){:}(\tau_1^{d_1},\dots,\tau_n^{d_n},(\tau_1^{d_1},\dots,\tau_n^{d_n})^d)^{d+1} 이다. (이 경우 반드시 {|{\operatorname{FVar}(\phi)}|}=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}라면,mindent| \\{x{:}\tau^d\in\Gamma\cup\\{x_1^\phi{:}\tau_1^{d_1}\\}|x\in\operatorname{Var}(\phi[\psi/x_1^\phi])\\} \vdash \phi[\psi/x_1^\phi]{:}(\tau_2^{d_2},\dots,\tau_n^{d_n})^{ \max(\\{d_2,\dots,d_n\\}\cup\\{e|\phi[\psi/x_1^\phi]=\cdots\forall x{:}\tau^e\cdots\\})+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라면,mindent| \\{x{:}\tau^d\in\Gamma\cup\\{x_i^\phi{:}\tau_i^{d_i},y{:}\tau_i^{d_i}\\}|x\in\operatorname{Var}(\phi[y/x_i^\phi])\\} \vdash \phi[y/x_i^\phi]{:}(\tau_1^{d_1},\dots,\tau_{i-1}^{d_{i-1,\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를 **논리식**(論理式, formula)이라고 한다.
# 연산

## 자유 변수, 매개 변수, 재귀 매개 변수
분지 유형 이론의 각 유사 논리식 \phi의 **자유 변수**(自由變數, free variable)의 집합 \operatorname{FVar}(\phi), **매개 변수**(媒介變數, parameter)의 집합 \operatorname{Par}(\phi), **재귀 매개 변수**(再歸媒介變數, recursive parameter)의 집합 \operatorname{RPar}(\phi)은 다음과 같이 재귀적으로 정의된다. (매개 변수와 재귀 매개 변수는 이름과 달리 변수가 아닐 수 있다.) * n항 관계 R 및 변수 또는 개체 p_1,\dots,p_n에 대하여,\operatorname{FVar}(R(p_1,\dots,p_n))=\mathcal V\cap\\{p_1,\dots,p_n\\}\operatorname{Par}(R(p_1,\dots,p_n))=\\{p_1,\dots,p_n\\}\operatorname{RPar}(R(p_1,\dots,p_n))=\\{p_1,\dots,p_n\\} * 변수 x 및 유한 개의 변수 또는 개체 또는 유사 논리식 p_1,\dots,p_n에 대하여,\operatorname{FVar}(x(p_1,\dots,p_n))=\mathcal V\cap\\{x,p_1,\dots,p_n\\}\operatorname{Par}(x(p_1,\dots,p_n))=\\{p_1,\dots,p_n\\}\operatorname{RPar}(x(p_1,\dots,p_n))=\\{p_1,\dots,p_n\\}\cup\bigcup_{\phi\in\mathcal P\cap\\{p_1,\dots,p_n\\\operatorname{RPar}(\phi) * 유사 논리식 \phi,\psi에 대하여,\operatorname{FVar}(\phi\lor\psi)=\operatorname{FVar}(\phi)\cup\operatorname{FVar}(\psi)\operatorname{Par}(\phi\lor\psi)=\operatorname{Par}(\phi)\cup\operatorname{Par}(\psi)\operatorname{RPar}(\phi\lor\psi)=\operatorname{RPar}(\phi)\cup\operatorname{RPar}(\psi)\operatorname{FVar}(\lnot\phi)=\operatorname{FVar}(\phi)\operatorname{Par}(\lnot\phi)=\operatorname{Par}(\phi)\operatorname{RPar}(\lnot\phi)=\operatorname{RPar}(\phi) * 유사 논리식 \phi 및 그 자유 변수 x\in\operatorname{FVar}(\phi)에 대하여,\operatorname{FVar}(\forall x\phi)=\operatorname{FVar}(\phi)\setminus\\{x\\}\operatorname{Par}(\forall x\phi)=\operatorname{Par}(\phi)\operatorname{RPar}(\forall x\phi)=\operatorname{RPar}(\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에 대하여, **치환 실례**(置換實例, substitutional instance) \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에 대하여,R(p_1,\dots,p_n)[q_1/x_1,\dots,q_k/x_k]=R(p_1\langle q_1/x_1,\dots,q_k/x_k\rangle,\dots,p_n\langle q_1/x_1,\dots,q_k/x_k\rangle) * 변수 x 및 및 변수 또는 개체 또는 유사 논리식 p_1,\dots,p_n,q_1,\dots,q_k 및 서로 다른 변수 x_1,\dots,x_k에 대하여,=n \end{cases} * 유사 논리식 \phi,\psi 및 변수 또는 개체 또는 유사 논리식 q_1,\dots,q_k 및 서로 다른 변수 x_1,\dots,x_k에 대하여,(\phi\lor\psi)[q_1/x_1,\dots,q_k/x_k]=\phi[q_1/x_1,\dots,q_k/x_k]\lor\psi[q_1/x_1,\dots,q_k/x_k](\lnot\phi)[q_1/x_1,\dots,q_k/x_k]=\lnot(\phi[q_1/x_1,\dots,q_k/x_k]) * 유사 논리식 \phi 및 그 자유 변수 x\in\operatorname{FVar}(\phi) 및 분지 유형 \tau^d 및 변수 또는 개체 또는 유사 논리식 q_1,\dots,q_k 및 서로 다른 변수 x_1,\dots,x_k에 대하여,(\forall x{:}\tau^d\phi)[q_1/x_1,\dots,q_k/x_k]=\begin{cases} \forall x{:}\tau^d(\phi[q_1/x_1,\dots,q_k/x_k]) & x\not\in\\{x_1,\dots,x_n\\} \\\ \forall x{:}\tau^d(\phi[q_1/x_1,\dots,q_{i-1}/x_{i-1},q_{i+1}/x_{i+1},\dots,q_k/x_k]) & x=x_i \end{cases} 위 경우에 속하지 않는 치환 실례는 정의되지 않는다. 예를 들어, 변수 또는 개체 또는 유사 논리식 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가 서로 **α-순열 동치**(α-順列同値, α-equivalent modulo permutation)라고 한다. * \psi는 \phi에 등장하는 각 변수 x를 f(x)로 대체하여 얻는다. (특히, f(\operatorname{Var}(\phi))=\operatorname{Var}(\psi)이다.) 두 유사 논리식 \phi,\psi에 대하여, 다음 두 조건을 만족시키는 전단사 함수 f\colon\mathcal V\to\mathcal V가 존재한다면, \phi,\psi가 서로 **α-동치**(α-同値, α-equivalent)라고 한다. * \psi는 \phi에 등장하는 각 변수 x를 f(x)로 대체하여 얻는다. (특히, f(\operatorname{Var}(\phi))=\operatorname{Var}(\psi)이다.) * f|_{\operatorname{Var}(\phi)}는 증가 함수이다. 즉, 임의의 x,y\in\operatorname{Var}(\phi)에 대하여, x<_{\mathcal V}y\iff f(x)<_{\mathcal V}f(y) 두 유사 논리식 \phi,\psi 및 문맥 \Gamma에 대하여, 다음 세 조건을 만족시키는 전단사 함수 f\colon\mathcal V\to\mathcal V가 존재한다면, \phi,\psi가 서로 **αΓ-동치**(αΓ-同値, αΓ-equivalent)라고 한다. * \psi는 \phi에 등장하는 각 변수 x를 f(x)로 대체하여 얻는다. (특히, f(\operatorname{Var}(\phi))=\operatorname{Var}(\psi)이다.) * f|_{\operatorname{Var}(\phi)}는 증가 함수이다. 즉, 임의의 x,y\in\operatorname{Var}(\phi)에 대하여, x<_{\mathcal V}y\iff f(x)<_{\mathcal V}f(y) * 임의의 x\in\mathcal V 및 분지 유형 \tau^d에 대하여, x{:}\tau^d\in\Gamma\iff f(x){:}\tau^d\in\Gamma
# 역사
버트런드 러셀이 《수학 원리》에서 제시하였다.