제도 (논리학)

수리논리학과 컴퓨터 과학에서 제도(制度, 영어: institution 인스티튜션^[*])는 문법과 모형 이론이 부여된 논리 체계의 추상화이다.

정의

작은 범주의 범주의 반대 범주 ${\displaystyle \operatorname {Cat} ^{\operatorname {op} }}$에서 집합의 범주의 반대 범주로 가는, 사상을 잊는 망각 함자

${\displaystyle \operatorname {Ob} ^{\operatorname {op} }\colon \operatorname {Cat} ^{\operatorname {op} }\to \operatorname {Set} ^{\operatorname {op} }}$

와 멱집합 함자

${\displaystyle {\mathcal {P}}\colon \operatorname {Set} \to \operatorname {Set} ^{\operatorname {op} }}$

${\displaystyle {\mathcal {P}}\colon X\mapsto {\mathcal {P}}(X)}$

${\displaystyle {\mathcal {P}}\colon (f\colon X\to Y)\mapsto (f^{-1}\colon {\mathcal {P}}(Y)\to {\mathcal {P}}(X))}$

를 생각하자. 그렇다면 쉼표 범주

${\displaystyle {\mathcal {I}}=\operatorname {Ob} ^{\operatorname {op} }\downarrow {\mathcal {P}}}$

를 생각할 수 있다. 즉, ${\displaystyle {\mathcal {I}}}$는 구체적으로 다음과 같다.

• ${\displaystyle {\mathcal {I}}}$의 대상 ${\displaystyle (S,{\mathcal {M}},\models )}$은 다음과 같은 순서쌍이다.
  • 집합 ${\displaystyle S}$. ${\displaystyle S}$를 문장의 집합이라고 한다.
  • 작은 범주 ${\displaystyle {\mathcal {M}}}$. ${\displaystyle {\mathcal {M}}}$의 원소를 모형이라고 한다.
  • 함수 ${\displaystyle {\models }\colon \operatorname {Ob} ({\mathcal {M}})\to {\mathcal {P}}(S)}$. 이를 만족 관계(영어: satisfaction relation)라고 한다. 보통, ${\displaystyle \phi \in S}$ 및 ${\displaystyle M\in {\mathcal {M}}}$에 대하여, ${\displaystyle \phi \in \operatorname {\models } (M)}$를 이항 관계 ${\displaystyle M\models \phi }$로 표기한다.
• ${\displaystyle {\mathcal {I}}}$의 사상 ${\displaystyle (f,G)\colon (S,{\mathcal {M}},\models )\to (S',{\mathcal {M}}',\models ')}$은 다음과 같은 데이터로 구성된다.
  • ${\displaystyle f\colon S\to S'}$는 함수이다.
  • ${\displaystyle G\colon {\mathcal {M}}'\to {\mathcal {M}}}$는 함자이다.
  • 이들은 다음 조건을 만족시켜야 한다.

    임의의 모형 ${\displaystyle M'\in {\mathcal {M}}'}$ 및 문장 ${\displaystyle \phi \in S}$에 대하여, ${\displaystyle M'\models 'f_{S}(\phi )\iff G(M')\models \phi }$이다. 즉, 다음 그림이 가환 그림이다.

    ${\displaystyle {\begin{matrix}\operatorname {Ob} ({\mathcal {M}}')&{\overset {\operatorname {Ob} (G)}{\to }}&\operatorname {Ob} ({\mathcal {M}})\\{\scriptstyle \models '}\downarrow {}{\color {White}\scriptstyle \models '}&&{\color {White}\scriptstyle \models }\downarrow {}\scriptstyle \models \\{\mathcal {P}}(S')&{\underset {f_{S}^{-1}}{\to }}&{\mathcal {P}}(S)\\\end{matrix}}}$

범주 ${\displaystyle {\mathcal {L}}}$에 대하여, ${\displaystyle {\mathcal {L}}}$ 위의 제도(영어: institution)는 함자 ${\displaystyle I\colon {\mathcal {L}}\to {\mathcal {I}}}$이다. 이 경우, ${\displaystyle {\mathcal {L}}}$을 제도 ${\displaystyle I}$의 언어들의 범주라고 한다. 같은 언어 위의 두 제도 사이의 사상은 자연 변환이다.

종류

불 제도

제도 ${\displaystyle I\colon {\mathcal {L}}\to {\mathcal {I}}}$가 다음 두 성질을 만족시킨다면, ${\displaystyle (S,\models )}$가 불 제도(영어: Boolean institution)라고 한다.

• (부정의 존재) 임의의 언어 ${\displaystyle L\in {\mathcal {L}}}$ 및 모형 ${\displaystyle M\in {\mathcal {M}}(L)}$ 및 문장 ${\displaystyle \phi \in S(L)}$에 대하여, ${\displaystyle M\models \phi \iff M\not \models \chi }$가 되는 문장 ${\displaystyle \chi \in S(L)}$이 존재한다.
• (논리곱의 존재) 임의의 언어 ${\displaystyle L\in {\mathcal {L}}}$ 및 모형 ${\displaystyle M\in \operatorname {Model} (L)}$ 및 두 문장 ${\displaystyle \phi ,\chi \in S(L)}$에 대하여, ${\displaystyle M\models \psi \iff (M\models \phi \land M\models \psi )}$가 되는 문장 ${\displaystyle \psi \in S(L)}$이 존재한다.

이 경우, 부정과 논리곱을 사용하여 고전 명제 논리의 연산(논리합, 함의, 동치 등)들을 정의할 수 있다.

콤팩트성

기수 ${\displaystyle \kappa }$가 주어졌다고 하자. 제도 ${\displaystyle I\colon {\mathcal {L}}\to {\mathcal {I}}}$가 다음 조건을 만족시킨다면, ${\displaystyle \kappa }$-콤팩트 제도(영어: compact institution)라고 한다.

• 임의의 언어 ${\displaystyle L\in {\mathcal {L}}}$ 및 임의의 부분 집합 ${\displaystyle A\subseteq S(L)}$에 대하여, 다음이 성립한다.

  ${\displaystyle \left(\exists M\in {\mathcal {M}}(L)\colon M\models A\right)\iff \left(\forall A'\in {\mathcal {P}}_{<\kappa }(A)\exists M\in {\mathcal {M}}(L)\colon M\models A'\right)}$

여기서, 문장들의 집합 ${\displaystyle A}$ 및 모형 ${\displaystyle M}$에 대하여 ${\displaystyle M\models A}$는

${\displaystyle \forall \phi \in A\colon M\models \phi }$

를 뜻한다. ${\displaystyle {\mathcal {P}}_{<\kappa }(A)}$는 ${\displaystyle A}$의, 크기가 ${\displaystyle \kappa }$ 미만의 부분 집합들의 족이다.

예

1차 논리와 그 표준적 모형은 제도를 이룬다. 이 밖에도, 다른 많은 논리 체계들을 제도로 나타낼 수 있다.

역사

제도의 개념은 1970년대에 조지프 애머디 고겐(영어: Joseph Amadee Goguen, 1941~2006)과 로드니 마티노 버스톨(영어: Rodney Martineau Burstall, 1934~)이 도입하였다.^[1][2]