보존적 확장 문서 원본 보기

{{위키데이터 속성 추적}}
[[수리논리학]]에서 '''보존적 확장'''(保存的擴張, {{llang|en|conservative extension}})은 주어진 이론을 확장하되, 원래 이론의 언어로서 나타낼 수 있는 모든 명제의 증명 가능성 여부가 바뀌지 않게 하는 확장이다.

== 정의 ==
다음 데이터가 주어졌다고 하자.
* [[1차 논리]] 언어 <math>\mathcal L</math>과 그 확장 <math>\mathcal L'\supseteq\mathcal L</math>
* <math>\mathcal L</math>-문장들의 집합 <math>\mathcal T</math>와 <math>\mathcal L'</math>-문장들의 집합 <math>\mathcal T'\supseteq\mathcal T</math>
만약 다음 조건이 성립한다면, <math>\mathcal T'</math>이 <math>\mathcal T</math>의 '''(증명 이론적) 보존적 확장'''({{llang|en|proof-theoretic conservative extension}})이라고 한다.<ref>{{서적 인용|title=Set theory: an introduction to independence proofs|url=https://archive.org/details/settheoryintrodu0000kune|성=Kunen|저자링크=케네스 쿠넌|이름=Kenneth|publisher=North-Holland|year=1980|isbn=0-444-85401-0|언어=en}}</ref>{{rp|37, Theorem 1.13.2}}
:<math>\{\phi\in\operatorname{Sent}(\mathcal L)\colon \mathcal T\vdash\phi\}=\{\phi\in\operatorname{Sent}(\mathcal L)\colon \mathcal T'\vdash\phi\}</math>
즉, <math>\mathcal L</math>로 서술할 수 있는 문장에 대하여, <math>\mathcal T</math>-증명 가능성은 <math>\mathcal T'</math>-증명 가능성과 [[동치]]이다.

만약 다음 조건이 성립한다면, <math>\mathcal T'</math>이 <math>\mathcal T</math>의 '''모형 이론적 보존적 확장'''({{llang|en|model-theoretic conservative extension}})이라고 한다.
* 임의의 <math>\mathcal L</math>-[[구조 (논리학)|구조]] <math>M</math>에 대하여 <math>M\models\mathcal T</math>라면, <math>M'|_{\mathcal L}=M</math>이자 <math>M'\models\mathcal T'</math>인 <math>\mathcal L'</math>-[[구조 (논리학)|구조]] <math>M'</math>이 항상 존재한다. (그러나 이는 유일할 필요는 없다.)

== 성질 ==
이론 <math>\mathcal T</math>의 증명 이론적 보존적 확장 <math>\mathcal T'</math>이 주어졌다고 하자. 그렇다면,  <math>\mathcal T</math>가 무모순적인지 여부는 <math>\mathcal T'</math>가 무모순적인지 여부와 [[동치]]이다.
:<math>\operatorname{Con}(\mathcal T)\iff\operatorname{Con}(\mathcal T')</math>
(여기서 <math>\bot</math>은 거짓인 문장이다.)

무모순적 이론 <math>\mathcal T</math>의 확장 <math>\mathcal T'</math>에 대하여, <math>\mathcal T'\vdash\operatorname{Con}(\mathcal T)</math>라면, [[괴델의 불완전성 정리]]에 따라 <math>\mathcal T'</math>은 <math>\mathcal T</math>의 보존적 확장이 아니다.

== 예 ==
언어 <math>\mathcal L</math>의 [[1차 논리]] 문장들의 집합 <math>\mathcal T\subseteq\operatorname{Sent}(\mathcal L)</math>이 주어졌다고 하고, <math>\mathcal T</math>로부터 다음과 같은 꼴의 문장을 증명할 수 있다고 하자.
:<math>\mathcal T\vdash\forall x_1\forall x_2\cdots\forall x_m\exists y_1\exists y_2\cdots\exists y_n\phi(x_1,\dots,x_m,y_n,\dots,y_n)</math>
여기서 [[논리식]] <math>\phi</math>의 자유 변수들은 <math>x_1,\dots,x_m,y_n,\dots,y_n</math>이며, <math>m,n\in\mathbb N</math>은 [[자연수]]이다 (특히, 0일 수 있다).

그렇다면, <math>\mathcal L</math>에 <math>n</math>개의 새 <math>m</math>항 연산 기호 <math>\mathsf f_1,\dots,\mathsf f_n</math>를 추가한 언어를 <math>\mathcal L'</math>이라고 하고,
:<math>\mathcal T'=\mathcal T\cup\{\forall x_1\forall x_2\cdots\forall x_m\phi\left(x_1,\dots,x_m,\mathsf f_1(x_1,\dots,x_m),\dots,\mathsf f_n(x_1,\dots,x_m)\right)\}\subseteq\operatorname{Sent}(\mathcal L')</math>
을 정의하자. 그렇다면, <math>\mathcal T'</math>은 <math>\mathcal T</math>의 모형 이론적 보존적 확장이다.

== 참고 문헌 ==
{{각주}}

[[분류:수리논리학]]