분지 유형 이론 문서 원본 보기

{{위키데이터 속성 추적}}
[[논리학]]에서 '''분지 유형 이론'''(分枝類型理論, {{llang|en|ramified type theory}}, 약자 RTT) 또는 '''복잡 유형 이론'''(複雜類型理論)은 [[단순 유형 이론]]보다 더 세분된 [[유형 이론|유형]]을 사용하는 논리 체계이다.<ref name="Laan">{{저널 인용
|성1=Laan
|이름1=Twan
|성2=Nederpelt
|이름2=Rob
|제목=A modern elaboration of the ramified theory of types
|언어=en
|저널=Studia Logica
|권=57
|호=2–3
|쪽=243–278
|날짜=1996-10
|issn=0039-3215
|doi=10.1007/BF00370835
|jstor=20015876
}}</ref><ref name="Kamareddine">{{서적 인용
|성1=Kamareddine
|이름1=Fairouz
|성2=Laan
|이름2=Twan
|성3=Nederpelt
|이름3=Rob
|제목=A Modern Perspective on Type Theory
|언어=en
|총서=Applied Logic Series
|권=29
|출판사=Springer
|위치=Dordrecht
|날짜=2005
|isbn=978-1-4020-2334-7
|doi=10.1007/1-4020-2335-9
}}</ref>{{rp|Chapter 2}}

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

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

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

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

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

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

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

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

== 연산 ==
=== 자유 변수, 매개 변수, 재귀 매개 변수 ===
분지 유형 이론의 각 유사 논리식 <math>\phi</math>의 '''[[자유 변수]]'''(自由變數, {{llang|en|free variable}})의 집합 <math>\operatorname{FVar}(\phi)</math>, '''매개 변수'''(媒介變數, {{llang|en|parameter}})의 집합 <math>\operatorname{Par}(\phi)</math>, '''재귀 매개 변수'''(再歸媒介變數, {{llang|en|recursive parameter}})의 집합 <math>\operatorname{RPar}(\phi)</math>은 다음과 같이 재귀적으로 정의된다. (매개 변수와 [[재귀]] 매개 변수는 이름과 달리 변수가 아닐 수 있다.)
* <math>n</math>항 관계 <math>R</math> 및 변수 또는 개체 <math>p_1,\dots,p_n</math>에 대하여,{{mindent|<math>
\operatorname{FVar}(R(p_1,\dots,p_n))=\mathcal V\cap\{p_1,\dots,p_n\}
</math>}}{{mindent|<math>
\operatorname{Par}(R(p_1,\dots,p_n))=\{p_1,\dots,p_n\}
</math>}}{{mindent|<math>
\operatorname{RPar}(R(p_1,\dots,p_n))=\{p_1,\dots,p_n\}
</math>}}
* 변수 <math>x</math> 및 유한 개의 변수 또는 개체 또는 유사 논리식 <math>p_1,\dots,p_n</math>에 대하여,{{mindent|<math>
\operatorname{FVar}(x(p_1,\dots,p_n))=\mathcal V\cap\{x,p_1,\dots,p_n\}
</math>}}{{mindent|<math>
\operatorname{Par}(x(p_1,\dots,p_n))=\{p_1,\dots,p_n\}
</math>}}{{mindent|<math>
\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)
</math>}}
* 유사 논리식 <math>\phi,\psi</math>에 대하여,{{mindent|<math>
\operatorname{FVar}(\phi\lor\psi)=\operatorname{FVar}(\phi)\cup\operatorname{FVar}(\psi)
</math>}}{{mindent|<math>
\operatorname{Par}(\phi\lor\psi)=\operatorname{Par}(\phi)\cup\operatorname{Par}(\psi)
</math>}}{{mindent|<math>
\operatorname{RPar}(\phi\lor\psi)=\operatorname{RPar}(\phi)\cup\operatorname{RPar}(\psi)
</math>}}{{mindent|<math>
\operatorname{FVar}(\lnot\phi)=\operatorname{FVar}(\phi)
</math>}}{{mindent|<math>
\operatorname{Par}(\lnot\phi)=\operatorname{Par}(\phi)
</math>}}{{mindent|<math>
\operatorname{RPar}(\lnot\phi)=\operatorname{RPar}(\phi)
</math>}}
* 유사 논리식 <math>\phi</math> 및 그 자유 변수 <math>x\in\operatorname{FVar}(\phi)</math>에 대하여,{{mindent|<math>
\operatorname{FVar}(\forall x\phi)=\operatorname{FVar}(\phi)\setminus\{x\}
</math>}}{{mindent|<math>
\operatorname{Par}(\forall x\phi)=\operatorname{Par}(\phi)
</math>}}{{mindent|<math>
\operatorname{RPar}(\forall x\phi)=\operatorname{RPar}(\phi)
</math>}}

=== 치환 ===
변수 또는 개체 또는 유사 논리식 <math>p,q_1,\dots,q_k</math> 및 서로 다른 변수 <math>x_1,\dots,x_k</math>에 대하여,
:<math>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}</math>
이라고 하자.

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

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

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

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

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

== 각주 ==
{{각주}}
* {{저널 인용
|url=http://logicalkorea.com/attach/paper/20-1-JIPark.pdf
|형식=PDF
|저자=박정일
|제목=비트겐슈타인과 환원 가능성 공리
|저널=논리연구
|권=20
|호=1
|쪽=69–96
|날짜=2017
|issn=1598-7493
|확인날짜=2020-04-12
|보존url=https://web.archive.org/web/20190508033144/http://logicalkorea.com/attach/paper/20-1-JIPark.pdf
|보존날짜=2019-05-08
|url-status=dead
}}
* {{저널 인용
|url=http://logicalkorea.com/attach/paper/21-1-JIPark.pdf
|형식=PDF
|저자=박정일
|제목=전기 비트겐슈타인과 유형 이론
|저널=논리연구
|권=21
|호=1
|쪽=1–37
|날짜=2018
|issn=1598-7493
|확인날짜=2020-04-12
|보존url=https://web.archive.org/web/20190507235055/http://logicalkorea.com/attach/paper/21-1-JIPark.pdf
|보존날짜=2019-05-07
|url-status=dead
}}
* {{저널 인용
|url=http://scc.sogang.ac.kr/Download?pathStr=NTEjIzU3IyM1MSMjNTAjIzEyNCMjMTA0IyMxMTYjIzk3IyM4MCMjMTAxIyMxMDgjIzEwNSMjMTAyIyMzNSMjMzMjIzM1IyM1MyMjMTI0IyMxMjAjIzEwMSMjMTAwIyMxMTAjIzEwNSMjMzUjIzMzIyMzNSMjNDgjIzQ4IyM1NiMjNTAjIzUwIyM1NiMjMTI0IyMxMDAjIzEwNSMjMTA3IyMxMTI=&fileName=%EB%9F%AC%EC%85%80%EC%9D%98_%EC%9C%A0%ED%98%95_%EC%9D%B4%EB%A1%A0.pdf&gubun=board
|형식=PDF
|저자=오은영
|제목=러셀의 유형 이론
|저널=철학논집
|권=5
|쪽=166–207
|날짜=1987
|issn=1738-8104
}}{{깨진 링크|url=http://scc.sogang.ac.kr/Download?pathStr=NTEjIzU3IyM1MSMjNTAjIzEyNCMjMTA0IyMxMTYjIzk3IyM4MCMjMTAxIyMxMDgjIzEwNSMjMTAyIyMzNSMjMzMjIzM1IyM1MyMjMTI0IyMxMjAjIzEwMSMjMTAwIyMxMTAjIzEwNSMjMzUjIzMzIyMzNSMjNDgjIzQ4IyM1NiMjNTAjIzUwIyM1NiMjMTI0IyMxMDAjIzEwNSMjMTA3IyMxMTI=&fileName=%EB%9F%AC%EC%85%80%EC%9D%98_%EC%9C%A0%ED%98%95_%EC%9D%B4%EB%A1%A0.pdf&gubun=board }}

[[분류:유형 이론]]