분지 유형 이론

"오늘의AI위키"는 AI 기술로 일관성 있고 체계적인 최신 지식을 제공하는 혁신 플랫폼입니다.
"오늘의AI위키"의 AI를 통해 더욱 풍부하고 폭넓은 지식 경험을 누리세요.

1. 개요

분지 유형 이론은 러셀이 《수학 원리》에서 제시한 것으로, 가산 무한 정렬 전순서 집합, 개체 집합, 관계 집합, 항수 함수를 기반으로 한다. 분지 유형 이론은 분지 유형과 차수를 정의하며, 술어적 분지 유형을 특별히 다룬다. 문맥, 유사 논리식, 논리식, 자유 변수, 매개 변수, 치환, α-동치 등의 개념을 포함하며, 논리식의 분지 유형을 결정하는 규칙들을 제시한다.

분지 유형 이론

개요

분야	수리논리학, 형식논리학, 유형 이론, 논리철학
유형	유형 이론

역사적 맥락

제안자	버트런드 러셀
영향	수학 원리 술어 논리

주요 개념

설명	유형은 계층적으로 배열되어 있음. 유형은 자신의 계층보다 높은 수준의 유형을 수량화할 수 없음. 유형은 자신의 계층보다 높은 수준의 총체성을 구성할 수 없음.
목표	역설 회피
다른 유형 이론	단순 유형 이론 구성적 유형 이론 의존적 유형 이론

📚 더 읽어볼만한 페이지

유형 이론 - 형 변환
형 변환은 프로그래밍에서 변수의 데이터 타입을 변경하는 것으로, 암시적 형 변환과 명시적 형 변환으로 나뉘며, 객체 지향 프로그래밍에서는 업캐스팅과 다운캐스팅이 발생하고, 각 언어는 고유한 규칙과 방법을 제공하며 잘못된 형 변환은 오류를 유발할 수 있다.
유형 이론 - 대수적 자료형
대수적 자료형은 합 타입과 곱 타입을 조합하여 새로운 자료형을 정의하는 방법으로, 단일 연결 리스트나 이진 트리와 같은 자료 구조를 표현하고 패턴 매칭을 통해 자료형의 구조를 분해 및 처리하는 데 유용하며, 함수형 프로그래밍 언어에서 널리 사용된다.

1. 개요
2. 정의
3. 연산
4. 역사

2. 정의

분지 유형 이론을 정의하기 위해 다음과 같은 기본 요소들을 먼저 설정한다. (여기서 $\mathbb N$ 은 음이 아닌 정수의 집합이다.)

* 변수(variable^영어): 최대 원소를 갖지 않는 가산 무한 정렬 전순서 집합 $(\mathcal V,\le_{\mathcal V})$ 의 원소이다.
* 개체(individual^영어): 집합 $\mathcal A$ 의 원소이다.
* 관계(relation^영어): 집합 $\mathcal R$ 과 각 관계의 항수(arity)를 나타내는 함수 $\operatorname{arity}_{\mathcal R}\colon\mathcal R\to\mathbb N$ 로 정의된다. 각 자연수 $n\in \mathbb N$ 에 대하여, $\operatorname{arity}_{\mathcal R}^{-1}(n)$ 의 원소를 $n$ 항 관계( $n$ -ary relation^영어)라고 부른다.

이러한 요소들 $(\mathcal V,\le_{\mathcal V},\mathcal A,\mathcal R,\operatorname{arity}_{\mathcal R})$ 을 바탕으로 분지 유형 이론의 구체적인 내용, 즉 분지 유형, 문맥, 논리식 등이 정의된다.

2.1. 분지 유형

분지 유형 이론에서 사용되는 분지 유형(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)$ 으로 쓸 수 있다.

2.2. 문맥

분지 유형 이론에서 문맥(文脈, context^영어)은 유한한 개수의 변수들과 그 변수들에 해당하는 분지 유형들을 짝지어 놓은 것을 의미한다. 좀 더 정확히는, 변수들의 유한 집합과 분지 유형들의 집합 사이의 함수로 정의할 수 있다.

문맥은 보통 변수 $x$ 와 그 변수의 분지 유형 $\tau^d$ 를 콜론( $:$ )으로 연결한 순서쌍 $x:\tau^d$ 들의 유한 집합으로 표현한다. 예를 들어, $\Gamma = \{x_1:\tau_1^{d_1}, x_2:\tau_2^{d_2}, \dots, x_n:\tau_n^{d_n}\}$ 와 같이 나타낼 수 있다.

이때, 문맥 $\Gamma$ 에 포함된 모든 변수들의 집합을 문맥 $\Gamma$ 의 정의역(定義域, domain^영어)이라고 부르며, 다음과 같이 수식으로 표현할 수 있다.
: $\operatorname{dom}(\Gamma)=\{x|x:\tau^d\in\Gamma\}$
이는 문맥 $\Gamma$ 안에서 어떤 변수들이 사용되고 있는지를 나타낸다.

2.3. 논리식

분지 유형 이론의 유사 논리식(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 <_{\mathcal V} \cdots <_{\mathcal V} x_$

👆

좌우로 밀어서 보기

^\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_m^{d_m})^d, (\tau_1'^{d_1'}, \dots, \tau_n'^{d_n'})^{d'}

에 대해, 만약

\Gamma \vdash \phi{:}(\tau_1^{d_1}, \dots, \tau_m^{d_m})^d

이고

\Delta \vdash \psi{:}(\tau_1'^{d_1'}, \dots, \tau_n'^{d_n'})^{d'}

이며

\max\operatorname{dom}(\Gamma) < \min\operatorname{dom}(\Delta)

라면, 다음이 성립한다.
:

\Gamma \cup \Delta \vdash \phi \lor \psi{:}(\tau_1^{d_1}, \dots, \tau_m^{d_m}, \tau_1'^{d_1'}, \dots, \tau_n'^{d_n'})^{\max\{d, d'\}}

\Gamma \vdash \lnot\phi{:}(\tau_1^{d_1}, \dots, \tau_m^{d_m})^d

* 한정: 문맥

\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

라면, 다음이 성립한다.
:

\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

* 매개 변수에 대한 추상화: 문맥

\Gamma

, 유사 논리식

\phi

\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{:}\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

이라면, 다음이 성립한다.
:

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

: (이 경우 반드시

👆

좌우로 밀어서 보기

=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}

이라면, 다음이 성립한다.
:

\{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

라면, 다음이 성립한다.
:

\{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^영어)이라고 부른다.

3. 연산

분지 유형 이론에서는 논리식과 변수를 다루기 위한 여러 가지 기본적인 연산을 정의한다. 이러한 연산은 논리식의 구조를 분석하고 변형하는 데 필수적이며, 이론의 형식 체계를 구성하는 기초가 된다. 주요 연산으로는 자유 변수, 매개 변수, 재귀 매개 변수의 개념 정의, 논리식 내 변수를 다른 값으로 바꾸는 치환, 그리고 변수 이름 변경에 따른 논리식의 동등성을 다루는 α-동치 등이 있다. 각 연산의 구체적인 정의와 규칙은 이어지는 하위 섹션에서 자세히 설명한다.

3.1. 자유 변수, 매개 변수, 재귀 매개 변수

분지 유형 이론에서 다루는 각 유사 논리식 $\phi$ 에 대해, 그 안에 포함된 자유 변수(free variable^영어)의 집합 $\operatorname{FVar}(\phi)$ , 매개 변수(parameter^영어)의 집합 $\operatorname{Par}(\phi)$ , 그리고 재귀 매개 변수(recursive parameter^영어)의 집합 $\operatorname{RPar}(\phi)$ 은 다음과 같이 재귀적으로 정의된다. 여기서 주의할 점은, 매개 변수와 재귀 매개 변수는 이름과 달리 반드시 변수만을 의미하는 것은 아니며, 개체나 다른 유사 논리식을 포함할 수도 있다는 것이다.

* $n$ 개의 항을 가지는 관계 $R$ 과 변수 또는 개체 $p_1, \dots, p_n$ 에 대하여, 원자 논리식 $R(p_1, \dots, p_n)$ 의 각 집합은 다음과 같다.
: $\operatorname{FVar}(R(p_1,\dots,p_n))=\mathcal V\cap\{p_1,\dots,p_n\}$ (자유 변수는 $p_1, \dots, p_n$ 중 변수인 것들의 집합)
: $\operatorname{Par}(R(p_1,\dots,p_n))=\{p_1,\dots,p_n\}$ (매개 변수는 $p_1, \dots, p_n$ 전체 집합)
: $\operatorname{RPar}(R(p_1,\dots,p_n))=\{p_1,\dots,p_n\}$ (재귀 매개 변수도 $p_1, \dots, p_n$ 전체 집합)
* 변수 $x$ 와 유한 개의 변수, 개체, 또는 유사 논리식 $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\}$ (자유 변수는 $x, p_1, \dots, p_n$ 중 변수인 것들의 집합)
: $\operatorname{Par}(x(p_1,\dots,p_n))=\{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)$ (재귀 매개 변수는 $p_1, \dots, p_n$ 과, $p_i$ 중 유사 논리식인 것들의 재귀 매개 변수 집합의 합집합)
* 두 유사 논리식 $\phi, \psi$ 에 대하여, 논리합( $\lor$ )과 부정( $\lnot$ ) 연산이 적용된 경우 각 집합은 다음과 같다.
: $\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)$ 에 대하여, 전체 한정 기호( $\forall$ )가 적용된 $\forall x \phi$ 의 각 집합은 다음과 같다.
: $\operatorname{FVar}(\forall x\phi)=\operatorname{FVar}(\phi)\setminus\{x\}$ (자유 변수 집합에서 $x$ 가 제외됨)
: $\operatorname{Par}(\forall x\phi)=\operatorname{Par}(\phi)$ (매개 변수 집합은 변하지 않음)
: $\operatorname{RPar}(\forall x\phi)=\operatorname{RPar}(\phi)$ (재귀 매개 변수 집합도 변하지 않음)

3.2. 치환

변수 또는 개체 또는 유사 논리식 $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$ 에 대하여,
: $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}$
* 유사 논리식 $\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]$ 는 정의되지 않는다.

3.3. α-동치

두 유사 논리식 $\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$

4. 역사

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

분야	수리논리학, 형식논리학, 유형 이론, 논리철학
유형	유형 이론

역사적 맥락

제안자	버트런드 러셀
영향	수학 원리 술어 논리

주요 개념

설명	유형은 계층적으로 배열되어 있음. 유형은 자신의 계층보다 높은 수준의 유형을 수량화할 수 없음. 유형은 자신의 계층보다 높은 수준의 총체성을 구성할 수 없음.
목표	역설 회피
다른 유형 이론	단순 유형 이론 구성적 유형 이론 의존적 유형 이론