분지 유형 이론

논리학에서 분지 유형 이론(分枝類型理論, 영어: ramified type theory, 약자 RTT) 또는 복잡 유형 이론(複雜類型理論)은 단순 유형 이론보다 더 세분된 유형을 사용하는 논리 체계이다.^{[1][2]:Chapter 2}

다음과 같은 데이터가 주어졌다고 하자. (여기서 ${\displaystyle \mathbb {N} }$은 음이 아닌 정수의 집합이다.)

• 최대 원소를 갖지 않는 가산 무한 정렬 전순서 집합 ${\displaystyle ({\mathcal {V}},\leq _{\mathcal {V}})}$. 그 원소를 변수(變數, 영어: variable)라고 한다.
• 집합 ${\displaystyle {\mathcal {A}}}$. 그 원소를 개체(個體, 영어: individual)라고 한다.
• 집합 ${\displaystyle {\mathcal {R}}}$ 및 함수 ${\displaystyle \operatorname {arity} _{\mathcal {R}}\colon {\mathcal {R}}\to \mathbb {N} }$. 각 ${\displaystyle n\in \mathbb {N} }$에 대하여, ${\displaystyle \operatorname {arity} _{\mathcal {R}}^{-1}(n)}$의 원소를 ${\displaystyle n}$항 관계(${\displaystyle n}$項關係, 영어: ${\displaystyle n}$-ary relation)라고 한다.

그렇다면, ${\displaystyle ({\mathcal {V}},\leq _{\mathcal {V}},{\mathcal {A}},{\mathcal {R}},\operatorname {arity} _{\mathcal {R}})}$에 대한 분지 유형 이론은 다음과 같다.

분지 유형 이론에서 사용되는 분지 유형(分枝類型, 영어: ramified type)과 이들의 차수(次數, 영어: order)는 다음과 같다.

• ${\displaystyle \iota ^{0}}$은 0차 분지 유형이다.
• ${\displaystyle d_{1},\dots ,d_{n}}$차 분지 유형 ${\displaystyle \tau _{1}^{d_{1}},\dots ,\tau _{n}^{d_{n}}}$ 및 자연수 ${\displaystyle d>\max\{d_{1},\dots ,d_{n}\}}$에 대하여, ${\displaystyle (\tau _{1}^{d_{1}},\dots ,\tau _{n}^{d_{n}})^{d}}$는 ${\displaystyle d}$차 분지 유형이다.

이들 가운데, 술어적 분지 유형(述語的分枝類型, 영어: predicative ramified type)은 다음과 같다.

• ${\displaystyle \iota ^{0}}$은 술어적 분지 유형이다.
• ${\displaystyle d_{1},\dots ,d_{n}}$차 술어적 분지 유형 ${\displaystyle \tau _{1}^{d_{1}},\dots ,\tau _{n}^{d_{n}}}$에 대하여, ${\displaystyle (\tau _{1}^{d_{1}},\dots ,\tau _{n}^{d_{n}})^{\max\{d_{1},\dots ,d_{n}\}+1}}$는 술어적 분지 유형이다. (${\displaystyle n=0}$일 경우, ${\displaystyle ()^{0}}$은 술어적 분지 유형이다.)

술어적 분지 유형은 차수를 생략한 채 ${\displaystyle \iota }$와 ${\displaystyle (\tau _{1},\dots ,\tau _{n})}$으로 쓸 수 있다.

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

${\displaystyle \operatorname {dom} (\Gamma )=\{x|x{:}\tau ^{d}\in \Gamma \}}$

분지 유형 이론의 유사 논리식(類似論理式, 영어: pseudoformula)은 다음과 같다.

• ${\displaystyle n}$항 관계 ${\displaystyle R}$ 및 변수 또는 개체 ${\displaystyle p_{1},\dots ,p_{n}}$에 대하여, ${\displaystyle R(p_{1},\dots ,p_{n})}$은 유사 논리식이다.
  • ${\displaystyle n=0}$일 경우 유사 논리식 ${\displaystyle R()}$은 0항 관계 ${\displaystyle R}$와 구분되어야 한다. 분지 유형 이론에서 ${\displaystyle n}$항 관계는 유사 논리식이 아니다.
• 변수 ${\displaystyle x}$ 및 유한 개의 변수 또는 개체 또는 유사 논리식 ${\displaystyle p_{1},\dots ,p_{n}}$에 대하여, ${\displaystyle x(p_{1},\dots ,p_{n})}$는 유사 논리식이다.
  • ${\displaystyle n=0}$일 경우 유사 논리식 ${\displaystyle x()}$은 변수 ${\displaystyle x}$와 구분되어야 한다. 분지 유형 이론에서 변수나 개체는 유사 논리식이 아니다.
• 유사 논리식 ${\displaystyle \phi ,\psi }$에 대하여, ${\displaystyle \phi \lor \psi }$와 ${\displaystyle \lnot \phi }$는 유사 논리식이다.
• 유사 논리식 ${\displaystyle \phi }$ 및 그 자유 변수 ${\displaystyle x\in \operatorname {FVar} (\phi )}$ 및 분지 유형 ${\displaystyle \tau ^{d}}$에 대하여, ${\displaystyle \forall x{:}\tau ^{d}\phi }$는 유사 논리식이다.

유사 논리식의 집합을 ${\displaystyle {\mathcal {P}}}$라고 하자. 또한 각 유사 논리식 ${\displaystyle \phi }$에 대하여, ${\displaystyle \operatorname {Var} (\phi )}$가 ${\displaystyle \phi }$ 속에 등장하는 모든 변수의 집합이라고 하고,

${\displaystyle x_{1}^{\phi }<_{\mathcal {V}}\cdots <_{\mathcal {V}}x_{|{\operatorname {FVar} (\phi )}|}^{\phi }}$

가 ${\displaystyle \phi }$의 모든 자유 변수라고 하자.

문맥 ${\displaystyle \Gamma }$에서 개체 또는 유사 논리식 ${\displaystyle \phi }$가 분지 유형 ${\displaystyle \tau ^{d}}$를 갖는다는 것은 ${\displaystyle \Gamma \vdash \phi {:}\tau ^{d}}$로 표기하며, 다음과 같이 재귀적으로 정의된다. (여기서 ${\displaystyle \vdash \phi {:}\tau ^{d}}$는 ${\displaystyle \varnothing \vdash \phi {:}\tau ^{d}}$를 뜻한다.)

• 개체 ${\displaystyle a}$에 대하여, ${\displaystyle \vdash a{:}\iota ^{0}}$이다.
• ${\displaystyle n}$항 관계 ${\displaystyle R}$ 및 개체 ${\displaystyle a_{1},\dots ,a_{n}}$에 대하여, ${\displaystyle \vdash R(a_{1},\dots ,a_{n}){:}()^{1}}$이다.
• (논리 연산) 문맥 ${\displaystyle \Gamma ,\Delta }$ 및 유사 논리식 ${\displaystyle \phi ,\psi }$ 및 분지 유형 ${\displaystyle (\tau _{1}^{d_{1}},\dots ,\tau _{n}^{d_{m}})^{d},({\tau _{1}'}^{d_{1}'},\dots ,{\tau _{n}'}^{d_{n}'})^{d'}}$에 대하여, 만약 ${\displaystyle \Gamma \vdash \phi {:}(\tau _{1}^{d_{1}},\dots ,\tau _{n}^{d_{m}})^{d}}$이며, ${\displaystyle \Delta \vdash \psi {:}({\tau _{1}'}^{d_{1}'},\dots ,{\tau _{n}'}^{d_{n}'})^{d'}}$이며, ${\displaystyle \max \operatorname {dom} (\Gamma )<\min \operatorname {dom} (\Delta )}$라면,
  ${\displaystyle \Gamma \cup \Delta \vdash \phi \lor \psi {:}(\tau _{1}^{d_{1}},\dots ,\tau _{n}^{d_{m}},{\tau _{1}'}^{d_{1}'},\dots ,{\tau _{n}'}^{d_{n}'})^{\max\{d,d'\}}}$
  ${\displaystyle \Gamma \vdash \lnot \phi {:}(\tau _{1}^{d_{1}},\dots ,\tau _{n}^{d_{m}})^{d}}$
  이다.
• (한정) 문맥 ${\displaystyle \Gamma }$ 및 유사 논리식 ${\displaystyle \phi }$ 및 ${\displaystyle i\in \{1,\dots ,|{\operatorname {FVar} (\phi )}|\}}$ 및 분지 유형 ${\displaystyle (\tau _{1}^{d_{1}},\dots ,\tau _{n}^{d_{n}})^{d}}$에 대하여, 만약 ${\displaystyle \Gamma \cup \{x_{i}^{\phi }{:}\tau _{i}^{d_{i}}\}\vdash \phi {:}(\tau _{1}^{d_{1}},\dots ,\tau _{n}^{d_{n}})^{d}}$라면,
  ${\displaystyle \Gamma \vdash \forall x_{i}^{\phi }{:}\tau _{i}^{d_{i}}\phi {:}(\tau _{1}^{d_{1}},\dots ,\tau _{i-1}^{d_{i-1}},\tau _{i+1}^{d_{i+1}},\dots ,\tau _{n}^{d_{n}})^{d}}$
  이다.
• (매개 변수에 대한 추상화) 문맥 ${\displaystyle \Gamma }$ 및 유사 논리식 ${\displaystyle \phi }$ 및 그 개체이거나 유사 논리식인 매개 변수 ${\displaystyle \psi \in \operatorname {Par} (\phi )\cap ({\mathcal {A}}\cup {\mathcal {P}})}$ 및 분지 유형 ${\displaystyle (\tau _{1}^{d_{1}},\dots ,\tau _{n}^{d_{n}})^{d},\tau _{n+1}^{d_{n+1}}}$ 및 변수 ${\displaystyle y>\max \operatorname {dom} (\Gamma )}$에 대하여, 만약 ${\displaystyle \Gamma \vdash \phi {:}(\tau _{1}^{d_{1}},\dots ,\tau _{n}^{d_{n}})^{d}}$이며 ${\displaystyle \Gamma \vdash \psi {:}\tau _{n+1}^{d_{n+1}}}$이라면,
  ${\displaystyle \{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\}}}$
  이다. 여기서 ${\displaystyle (\phi )_{\Gamma ,\psi ,y}}$는 ${\displaystyle \phi }$에 등장하는 ${\displaystyle \psi }$와 α_Γ-동치인 각 매개 변수 ${\displaystyle \psi '}$를 ${\displaystyle y}$로 대체하여 얻는 유사 논리식이다. (《수학 원리》에서 이는 ${\displaystyle (\tau _{1}^{d_{1}},\dots ,\tau _{n}^{d_{n}})^{d}}$가 술어적 분지 유형인 경우로 제한된다.)
• (논리식에 대한 추상화) 문맥 ${\displaystyle \Gamma }$ 및 유사 논리식 ${\displaystyle \phi }$ 및 분지 유형 ${\displaystyle (\tau _{1}^{d_{1}},\dots ,\tau _{n}^{d_{n}})^{d}}$ 및 변수 ${\displaystyle y>\max \operatorname {dom} (\Gamma )}$에 대하여, 만약 ${\displaystyle \Gamma \vdash \phi {:}(\tau _{1}^{d_{1}},\dots ,\tau _{n}^{d_{n}})^{d}}$이라면,
  ${\displaystyle \{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}}$
  이다. (이 경우 반드시 ${\displaystyle {|{\operatorname {FVar} (\phi )}|}=n}$임을 보일 수 있다.) (《수학 원리》에서 이는 ${\displaystyle (\tau _{1}^{d_{1}},\dots ,\tau _{n}^{d_{n}})^{d}}$가 술어적 분지 유형인 경우로 제한된다.)
• (치환) 문맥 ${\displaystyle \Gamma }$ 및 자유 변수를 갖는 유사 논리식 ${\displaystyle \phi }$ 및 개체 또는 유사 논리식 ${\displaystyle \psi }$ 및 분지 유형 ${\displaystyle (\tau _{1}^{d_{1}},\dots ,\tau _{n}^{d_{n}})^{d}}$에 대하여, 만약 ${\displaystyle \Gamma \cup \{x_{1}^{\phi }{:}\tau _{1}^{d_{1}}\}\vdash \phi {:}(\tau _{1}^{d_{1}},\dots ,\tau _{n}^{d_{n}})^{d}}$이며, ${\displaystyle \Gamma \vdash \psi {:}\tau _{1}^{d_{1}}}$라면,
  ${\displaystyle \{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}}$
  이다. (이 경우 ${\displaystyle \phi [\psi /x_{1}^{\phi }]}$는 반드시 정의됨을 보일 수 있다.)
• (약화) 문맥 ${\displaystyle \Gamma ,\Delta }$ 및 유사 논리식 ${\displaystyle \phi }$ 및 분지 유형 ${\displaystyle \tau ^{d}}$에 대하여, 만약 ${\displaystyle \Gamma \vdash \phi {:}\tau ^{d}}$이며, ${\displaystyle \Gamma \subseteq \Delta }$라면, ${\displaystyle \Delta \vdash \phi {:}\tau ^{d}}$이다.
• (순열) 문맥 ${\displaystyle \Gamma }$ 및 유사 논리식 ${\displaystyle \phi }$ 및 ${\displaystyle i\in \{1,\dots ,|{\operatorname {FVar} (\phi )}|\}}$ 및 분지 유형 ${\displaystyle (\tau _{1}^{d_{1}},\dots ,\tau _{n}^{d_{n}})^{d}}$ 및 변수 ${\displaystyle y>\max \operatorname {dom} (\Gamma )}$에 대하여, 만약 ${\displaystyle \Gamma \cup \{x_{i}^{\phi }{:}\tau _{i}^{d_{i}}\}\vdash \phi {:}(\tau _{1}^{d_{1}},\dots ,\tau _{n}^{d_{n}})^{d}}$라면,
  ${\displaystyle \{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}}$
  이다.

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

분지 유형 이론의 각 유사 논리식 ${\displaystyle \phi }$의 자유 변수(自由變數, 영어: free variable)의 집합 ${\displaystyle \operatorname {FVar} (\phi )}$, 매개 변수(媒介變數, 영어: parameter)의 집합 ${\displaystyle \operatorname {Par} (\phi )}$, 재귀 매개 변수(再歸媒介變數, 영어: recursive parameter)의 집합 ${\displaystyle \operatorname {RPar} (\phi )}$은 다음과 같이 재귀적으로 정의된다. (매개 변수와 재귀 매개 변수는 이름과 달리 변수가 아닐 수 있다.)

• ${\displaystyle n}$항 관계 ${\displaystyle R}$ 및 변수 또는 개체 ${\displaystyle p_{1},\dots ,p_{n}}$에 대하여,
  ${\displaystyle \operatorname {FVar} (R(p_{1},\dots ,p_{n}))={\mathcal {V}}\cap \{p_{1},\dots ,p_{n}\}}$
  ${\displaystyle \operatorname {Par} (R(p_{1},\dots ,p_{n}))=\{p_{1},\dots ,p_{n}\}}$
  ${\displaystyle \operatorname {RPar} (R(p_{1},\dots ,p_{n}))=\{p_{1},\dots ,p_{n}\}}$
• 변수 ${\displaystyle x}$ 및 유한 개의 변수 또는 개체 또는 유사 논리식 ${\displaystyle p_{1},\dots ,p_{n}}$에 대하여,
  ${\displaystyle \operatorname {FVar} (x(p_{1},\dots ,p_{n}))={\mathcal {V}}\cap \{x,p_{1},\dots ,p_{n}\}}$
  ${\displaystyle \operatorname {Par} (x(p_{1},\dots ,p_{n}))=\{p_{1},\dots ,p_{n}\}}$
  ${\displaystyle \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 )}$
• 유사 논리식 ${\displaystyle \phi ,\psi }$에 대하여,
  ${\displaystyle \operatorname {FVar} (\phi \lor \psi )=\operatorname {FVar} (\phi )\cup \operatorname {FVar} (\psi )}$
  ${\displaystyle \operatorname {Par} (\phi \lor \psi )=\operatorname {Par} (\phi )\cup \operatorname {Par} (\psi )}$
  ${\displaystyle \operatorname {RPar} (\phi \lor \psi )=\operatorname {RPar} (\phi )\cup \operatorname {RPar} (\psi )}$
  ${\displaystyle \operatorname {FVar} (\lnot \phi )=\operatorname {FVar} (\phi )}$
  ${\displaystyle \operatorname {Par} (\lnot \phi )=\operatorname {Par} (\phi )}$
  ${\displaystyle \operatorname {RPar} (\lnot \phi )=\operatorname {RPar} (\phi )}$
• 유사 논리식 ${\displaystyle \phi }$ 및 그 자유 변수 ${\displaystyle x\in \operatorname {FVar} (\phi )}$에 대하여,
  ${\displaystyle \operatorname {FVar} (\forall x\phi )=\operatorname {FVar} (\phi )\setminus \{x\}}$
  ${\displaystyle \operatorname {Par} (\forall x\phi )=\operatorname {Par} (\phi )}$
  ${\displaystyle \operatorname {RPar} (\forall x\phi )=\operatorname {RPar} (\phi )}$

변수 또는 개체 또는 유사 논리식 ${\displaystyle p,q_{1},\dots ,q_{k}}$ 및 서로 다른 변수 ${\displaystyle x_{1},\dots ,x_{k}}$에 대하여,

${\displaystyle 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}}}$

이라고 하자.

유사 논리식 ${\displaystyle \phi }$ 및 변수 또는 개체 또는 유사 논리식 ${\displaystyle q_{1},\dots ,q_{k}}$ 및 서로 다른 변수 ${\displaystyle x_{1},\dots ,x_{k}}$에 대하여, 치환 실례(置換實例, 영어: substitutional instance) ${\displaystyle \phi [q_{1}/x_{1},\dots ,q_{k}/x_{k}]}$는 다음과 같이 재귀적으로 정의된다.

• ${\displaystyle n}$항 관계 ${\displaystyle R}$ 및 변수 또는 개체 ${\displaystyle p_{1},\dots ,p_{n},q_{1},\dots ,q_{k}}$ 및 서로 다른 변수 ${\displaystyle x_{1},\dots ,x_{k}}$에 대하여,
  ${\displaystyle 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 )}$
• 변수 ${\displaystyle x}$ 및 및 변수 또는 개체 또는 유사 논리식 ${\displaystyle p_{1},\dots ,p_{n},q_{1},\dots ,q_{k}}$ 및 서로 다른 변수 ${\displaystyle x_{1},\dots ,x_{k}}$에 대하여,
  ${\displaystyle x(p_{1},\dots ,p_{n})[q_{1}/x_{1},\dots ,q_{k}/x_{k}]={\begin{cases}x(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\not \in \{x_{1},\dots ,x_{k}\}\\q_{i}(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=x_{i},\;q_{i}\in {\mathcal {V}}\\q_{i}[p_{1}\langle q_{1}/x_{1},\dots ,q_{k}/x_{k}\rangle /x_{1}^{q_{i}},\dots ,p_{n}\langle q_{1}/x_{1},\dots ,q_{k}/x_{k}\rangle /x_{n}^{q_{i}}]&x=x_{i},\;q_{i}\in {\mathcal {P}},\;|{\operatorname {FVar} (q_{i})}|=n\end{cases}}}$
• 유사 논리식 ${\displaystyle \phi ,\psi }$ 및 변수 또는 개체 또는 유사 논리식 ${\displaystyle q_{1},\dots ,q_{k}}$ 및 서로 다른 변수 ${\displaystyle x_{1},\dots ,x_{k}}$에 대하여,
  ${\displaystyle (\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}]}$
  ${\displaystyle (\lnot \phi )[q_{1}/x_{1},\dots ,q_{k}/x_{k}]=\lnot (\phi [q_{1}/x_{1},\dots ,q_{k}/x_{k}])}$
• 유사 논리식 ${\displaystyle \phi }$ 및 그 자유 변수 ${\displaystyle x\in \operatorname {FVar} (\phi )}$ 및 분지 유형 ${\displaystyle \tau ^{d}}$ 및 변수 또는 개체 또는 유사 논리식 ${\displaystyle q_{1},\dots ,q_{k}}$ 및 서로 다른 변수 ${\displaystyle x_{1},\dots ,x_{k}}$에 대하여,
  ${\displaystyle (\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}}}$

위 경우에 속하지 않는 치환 실례는 정의되지 않는다. 예를 들어, 변수 또는 개체 또는 유사 논리식 ${\displaystyle p_{1},\dots ,p_{n},q_{1},\dots ,q_{k}}$ 및 서로 다른 변수 ${\displaystyle x_{1},\dots ,x_{k}}$에 대하여, 만약 ${\displaystyle q_{i}\in {\mathcal {A}}}$이거나, ${\displaystyle q_{i}\in {\mathcal {P}}}$이며 ${\displaystyle q_{i}}$의 자유 변수가 정확히 ${\displaystyle n}$개가 아닐 경우, ${\displaystyle x_{i}(p_{1},\dots ,p_{n})[q_{1}/x_{1},\dots ,q_{k}/x_{k}]}$는 정의되지 않는다.

두 유사 논리식 ${\displaystyle \phi ,\psi }$에 대하여, 다음 조건을 만족시키는 전단사 함수 ${\displaystyle f\colon {\mathcal {V}}\to {\mathcal {V}}}$가 존재한다면, ${\displaystyle \phi ,\psi }$가 서로 α-순열 동치(α-順列同値, 영어: α-equivalent modulo permutation)라고 한다.

• ${\displaystyle \psi }$는 ${\displaystyle \phi }$에 등장하는 각 변수 ${\displaystyle x}$를 ${\displaystyle f(x)}$로 대체하여 얻는다. (특히, ${\displaystyle f(\operatorname {Var} (\phi ))=\operatorname {Var} (\psi )}$이다.)

두 유사 논리식 ${\displaystyle \phi ,\psi }$에 대하여, 다음 두 조건을 만족시키는 전단사 함수 ${\displaystyle f\colon {\mathcal {V}}\to {\mathcal {V}}}$가 존재한다면, ${\displaystyle \phi ,\psi }$가 서로 α-동치(α-同値, 영어: α-equivalent)라고 한다.

• ${\displaystyle \psi }$는 ${\displaystyle \phi }$에 등장하는 각 변수 ${\displaystyle x}$를 ${\displaystyle f(x)}$로 대체하여 얻는다. (특히, ${\displaystyle f(\operatorname {Var} (\phi ))=\operatorname {Var} (\psi )}$이다.)
• ${\displaystyle f|_{\operatorname {Var} (\phi )}}$는 증가 함수이다. 즉, 임의의 ${\displaystyle x,y\in \operatorname {Var} (\phi )}$에 대하여, ${\displaystyle x<_{\mathcal {V}}y\iff f(x)<_{\mathcal {V}}f(y)}$

두 유사 논리식 ${\displaystyle \phi ,\psi }$ 및 문맥 ${\displaystyle \Gamma }$에 대하여, 다음 세 조건을 만족시키는 전단사 함수 ${\displaystyle f\colon {\mathcal {V}}\to {\mathcal {V}}}$가 존재한다면, ${\displaystyle \phi ,\psi }$가 서로 α_Γ-동치(α_Γ-同値, 영어: α_Γ-equivalent)라고 한다.

• ${\displaystyle \psi }$는 ${\displaystyle \phi }$에 등장하는 각 변수 ${\displaystyle x}$를 ${\displaystyle f(x)}$로 대체하여 얻는다. (특히, ${\displaystyle f(\operatorname {Var} (\phi ))=\operatorname {Var} (\psi )}$이다.)
• ${\displaystyle f|_{\operatorname {Var} (\phi )}}$는 증가 함수이다. 즉, 임의의 ${\displaystyle x,y\in \operatorname {Var} (\phi )}$에 대하여, ${\displaystyle x<_{\mathcal {V}}y\iff f(x)<_{\mathcal {V}}f(y)}$
• 임의의 ${\displaystyle x\in {\mathcal {V}}}$ 및 분지 유형 ${\displaystyle \tau ^{d}}$에 대하여, ${\displaystyle x{:}\tau ^{d}\in \Gamma \iff f(x){:}\tau ^{d}\in \Gamma }$

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

• 박정일 (2017). “비트겐슈타인과 환원 가능성 공리” (PDF). 《논리연구》 20 (1): 69–96. ISSN 1598-7493. 2019년 5월 8일에 원본 문서 (PDF)에서 보존된 문서. 2020년 4월 12일에 확인함. 
• 박정일 (2018). “전기 비트겐슈타인과 유형 이론” (PDF). 《논리연구》 21 (1): 1–37. ISSN 1598-7493. 2019년 5월 7일에 원본 문서 (PDF)에서 보존된 문서. 2020년 4월 12일에 확인함. 
• 오은영 (1987). “러셀의 유형 이론” (PDF). 《철학논집》 5: 166–207. ISSN 1738-8104. ^{[깨진 링크(과거 내용 찾기)]}