제도 (논리학) 문서 원본 보기

{{위키데이터 속성 추적}}
[[수리논리학]]과 [[컴퓨터 과학]]에서 '''제도'''(制度, {{llang|en|institution|인스티튜션}})는 문법과 [[모형 이론]]이 부여된 논리 체계의 추상화이다.

== 정의 ==
[[작은 범주]]의 범주의 [[반대 범주]] <math>\operatorname{Cat}^{\operatorname{op}}</math>에서 집합의 범주의 [[반대 범주]]로 가는, 사상을 잊는 망각 함자
:<math>\operatorname{Ob}^{\operatorname{op}}\colon\operatorname{Cat}^{\operatorname{op}}\to\operatorname{Set}^{\operatorname{op}}</math>
와 [[멱집합]] 함자
:<math>\mathcal P\colon\operatorname{Set}\to\operatorname{Set}^{\operatorname{op}}</math>
:<math>\mathcal P\colon X\mapsto\mathcal P(X)</math>
:<math>\mathcal P\colon (f\colon X\to Y)\mapsto(f^{-1}\colon\mathcal P(Y)\to\mathcal P(X))</math>
를 생각하자. 그렇다면 [[쉼표 범주]]
:<math>\mathcal I=\operatorname{Ob}^{\operatorname{op}}\downarrow\mathcal P</math>
를 생각할 수 있다. 즉, <math>\mathcal I</math>는 구체적으로 다음과 같다.
* <math>\mathcal I</math>의 대상 <math>(S,\mathcal M,\models)</math>은 다음과 같은 [[순서쌍]]이다.
** [[집합]] <math>S</math>. <math>S</math>를 '''문장'''의 집합이라고 한다.
** [[작은 범주]] <math>\mathcal M</math>. <math>\mathcal M</math>의 원소를 '''모형'''이라고 한다.
** [[함수]] <math>{\models}\colon\operatorname{Ob}(\mathcal M)\to\mathcal P(S)</math>. 이를 '''만족 관계'''({{llang|en|satisfaction relation}})라고 한다. 보통, <math>\phi\in S</math> 및 <math>M\in\mathcal M</math>에 대하여, <math>\phi\in \operatorname\models(M)</math>를 [[이항 관계]] <math>M\models\phi</math>로 표기한다.
* <math>\mathcal I</math>의 사상 <math>(f,G)\colon (S,\mathcal M,\models)\to(S',\mathcal M',\models')</math>은 다음과 같은 데이터로 구성된다.
** <math>f\colon S\to S'</math>는 [[함수]]이다.
** <math>G\colon\mathcal M'\to\mathcal M</math>는 [[함자 (수학)|함자]]이다.
** 이들은 다음 조건을 만족시켜야 한다.
**: 임의의 모형 <math>M'\in\mathcal M'</math> 및 문장 <math>\phi\in S</math>에 대하여, <math>M'\models' f_S(\phi)\iff G(M')\models\phi</math>이다. 즉, 다음 그림이 가환 그림이다.
**: <math>\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}</math>

[[범주 (수학)|범주]] <math>\mathcal L</math>에 대하여, <math>\mathcal L</math> 위의 '''제도'''({{llang|en|institution}})는 [[함자 (수학)|함자]] <math>I\colon\mathcal L\to\mathcal I</math>이다. 이 경우, <math>\mathcal L</math>을 제도 <math>I</math>의 '''언어'''들의 범주라고 한다.
같은 언어 위의 두 제도 사이의 사상은 [[자연 변환]]이다.

== 종류 ==
=== 불 제도 ===
제도 <math>I\colon\mathcal L\to\mathcal I</math>가 다음 두 성질을 만족시킨다면, <math>(S,\models)</math>가 '''불 제도'''({{llang|en|Boolean institution}})라고 한다.
* ([[부정]]의 존재) 임의의 언어 <math>L\in\mathcal L</math> 및 모형 <math>M\in\mathcal M(L)</math> 및 문장 <math>\phi\in S(L)</math>에 대하여, <math>M\models\phi\iff M\not\models\chi</math>가 되는 문장 <math>\chi\in S(L)</math>이 존재한다.
* ([[논리곱]]의 존재) 임의의 언어 <math>L\in\mathcal L</math> 및 모형 <math>M\in\operatorname{Model}(L)</math> 및 두 문장 <math>\phi,\chi\in S(L)</math>에 대하여, <math>M\models\psi\iff(M\models\phi\land M\models\psi)</math>가 되는 문장 <math>\psi\in S(L)</math>이 존재한다.
이 경우, 부정과 논리곱을 사용하여 고전 [[명제 논리]]의 연산([[논리합]], [[함의]], [[동치]] 등)들을 정의할 수 있다.

=== 콤팩트성 ===
[[기수 (수학)|기수]] <math>\kappa</math>가 주어졌다고 하자.
제도 <math>I\colon\mathcal L\to\mathcal I</math>가 다음 조건을 만족시킨다면, <math>\kappa</math>-'''[[콤팩트성 정리|콤팩트]] 제도'''({{llang|en|compact institution}})라고 한다.
* 임의의 언어 <math>L\in\mathcal L</math> 및 임의의 부분 집합 <math>A\subseteq S(L)</math>에 대하여, 다음이 성립한다.
*: <math>\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)</math>
여기서, 문장들의 집합 <math>A</math> 및 모형 <math>M</math>에 대하여 <math>M\models A</math>는
:<math>\forall\phi\in A\colon M\models\phi</math>
를 뜻한다. <math>\mathcal P_{<\kappa}(A)</math>는 <math>A</math>의, 크기가 <math>\kappa</math> 미만의 [[부분 집합]]들의 족이다.

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

== 역사 ==
제도의 개념은 1970년대에 조지프 애머디 고겐({{llang|en|Joseph Amadee Goguen}}, 1941~2006)과 로드니 마티노 버스톨({{llang|en|Rodney Martineau Burstall}}, 1934~)이 도입하였다.<ref>{{서적 인용|이름=Joseph|성=Goguen|이름2=Rodney M.|성2=Burstall|장=Introducing institutions|editor1-first=Edmund|editor1-last=Clarke|editor2-first=Dexter|editor2-last=Kozen|제목=Logics of programs: workshop, Carnegie Mellon University, Pittsburgh, PA, June 6–8, 1983|권=164|총서=Lecture Notes in Computer Science|쪽=221–256|출판사=Springer-Verlag|날짜=1984|doi=10.1007/3-540-12896-4_366|zbl=0543.68021|isbn= 978-3-540-12896-0|issn=0302-9743|언어=en}}</ref><ref>{{저널 인용|이름=J. A.|성=Goguen|이름2=R. M.|성2=Burstall|제목=Institutions: abstract model theory for specification and programming|저널=Journal of the Association for Computing Machinery|권=39|호=1|쪽=95–146|날짜=1992-01|doi=10.1145/147508.147524|zbl=0799.68134|언어=en}}</ref>

== 각주 ==
{{각주}}
* {{서적 인용|이름=Răzvan|성=Diaconescu|제목=Institution-independent model theory|url=https://archive.org/details/institutionindep0000diac|출판사=Birkhäuser|날짜=2008|doi=10.1007/978-3-7643-8708-2|isbn=978-3-7643-8707-5|총서=Studies in Universal Logic|issn=2297-0282|zbl=1144.03001|언어=en}}
* {{서적 인용|이름=Răzvan|성=Diaconescu|장=Institutions, Madhyamaka, and universal model theory|제목=Perspectives on universal logic|날짜=2007|쪽=41–65|url=http://www.imar.ro/~diacon/PDF/insmad_pul.pdf|editor1-first=Jean-Yves|editor1-last=Béziau|editor2-first=Alexandre|editor2-last=Costa-Leite|출판사=Polimetrica International Scientific Publisher|언어=en|확인날짜=2016-07-31|보존url=https://web.archive.org/web/20120209022831/http://www.imar.ro/~diacon/PDF/insmad_pul.pdf|보존날짜=2012-02-09|url-status=dead}}

== 외부 링크 ==
* {{nlab|id=abstract model theory|title=Abstract model theory}}
* {{웹 인용|url=http://www.iep.utm.edu/insti-th/|제목=Institution theory|웹사이트=Internet Encyclopedia of Philosophy|이름=Răzvan|성=Diaconescu|issn=2161-0002|언어=en}}
* {{웹 인용|url=http://cseweb.ucsd.edu/~goguen/projs/inst.html|제목=Institutions|이름=Joseph A.|성=Goguen|날짜=2006-01-06|언어=en}}
* {{웹 인용|url=http://cseweb.ucsd.edu/~goguen/projs/inst-sidebar.html|제목=Institutions and Peirce's triadic semiotics|이름=Joseph A.|성=Goguen|언어=en}}

[[분류:수리논리학]]
[[분류:이론 컴퓨터 과학]]