حذف سور

حذف سور (به انگلیسی: Quantifier elimination) یکی از ویژگی‌های «جبری» مورد بررسی در منطق ریاضی (در نظریهٔ مدلها) است. تئوریِ $T$

دارای حذف سور است (یا سورها را حذف می‌کند) هرگاه هر فرمولی به پیمانهٔ آن معادلی بدون سور داشته باشد.

مصداقِ ملموسی از حذف سور، فرمول تعیین‌کنندهٔ ریشه داشتن یا نداشتن یک معادلهٔ درجهٔ ۲ در اعداد حقیقی است: $(\mathbb {R} ,+,.,<,0,1)\models \exists x\quad ax^{2}+bx+c=0\leftrightarrow (a\not =0\wedge b^{2}-4ac\geq 0)\vee (a=0\wedge b\not =0)\vee (a=b=c=0)$

حذف سور به دلایل گوناگون اهمیت دارد که برخی از آن‌ها را در ادامه ذکر کرده‌ایم. نخست، برای این که مطالعهٔ مجموعه‌های تعریف‌شدنی را آسان‌تر می‌کند: اگر تئوری

T

دارای حذف سور باشد، برای بررسی مجموعه‌های تعریف شدنی در مدل‌های آن، تنها کافی است مجموعه‌های تعریف‌شده با ترکیبات بولیِ فرمول‌های اتمی را در نظر بگیریم. دوم این که حذف سور، مطالعهٔ جبری مدل‌ها را ساده می‌کند. اگر

T

دارای حذف سور باشد، آن‌گاه برای هر دو مدلِ

M, N

از آن، اگر

M

زیرساختاری از

N

باشد، آن‌گاه

M

زیرساختاری مقدماتی از

N

است، یعنی هر جملهٔ مرتبهٔ اول با پارامتر در

M

اگر در

N

درست باشد، آن‌گاه در

M

نیز درست است. سوم این که، بررسی کامل بودنِ یک تئوری، در صورت حذف سور پذیرفتن آن، آسان‌تر است. منظور از تئوریِ کامل، تئوری‌ای است که در آن هر جملهٔ داده‌شده یا نقیض آن اثبات شدنی است. از این رو اگر روندی تصمیم‌پذیر برای اثبات حذف سور داشته باشیم، اثبات تصمیم‌پذیر بودن یک تئوری نیز در حالتی که حذف سور داشته باشد، آسان‌تر است. چهارمین اهمیت حذف سور، فراهم آوردن توصیف جبری ملموس برای برخی تئوری‌ها و بدینسان برقرار کردن پیوند میان جبر و نظریهٔ مدل است. برای مثال، بررسی ساختار یا مدل تولید شده توسط یک مجموعهٔ داده شده، یا بررسی بستارِ جبری یک مجموعهٔ داده شده، در تئوری‌ای که حذف سور داشته باشد، به مراتب آسان‌تر است. این نکته در مثال‌های جبری، مانند میدان‌های بستهٔ حقیقی و میدان‌های بستهٔ جبری راحت‌تر به چشم می‌آید.

تعریف

تئوریِ $T$

در زبانِ

L

«دارای حذف سور است»، یا «سورها را حذف می‌کند» هرگاه برای هر فرمولِ

\phi ({\bar {x}})\in L

فرمولی بدون سور مانند

\psi ({\bar {x}})\in L

پیدا شود که

T\models \forall {\bar {x}}\quad \phi ({\bar {x}})\leftrightarrow \psi ({\bar {x}}).

با به روش‌های مقدماتی منطقی، فرمول بدون سورِ

\psi

را می‌توان به صورت

\bigwedge _{i}\bigvee _{j}\psi _{ij}

یا

\bigvee _{i}\bigwedge _{j}\psi _{ij}

در نظر گرفت که در آن هر

\psi _{ij}

فرمولی اتمی یا نقیض یک فرمول اتمی است.
معادلاً تئوری

T

دارای حذف سور است، هرگاه «زیرساختارْکامل» باشد. یعنی برای هر مدلِ

M\models T

و هر زیرساختارِ

A\subseteq M

تئوریِ

Diag(A)\cup T

در زبانِ

L_{A}

(زبانی که با افزودن ثابت برای ازای هر عنصرِ

A

به زبان تئوریِ

T

به دست آمده باشد) یک تئوریِ کامل باشد. منظور از

Diag(A)

مجموعهٔ همهٔ جمله‌های بدون سورِ با پارامتر در

A

است. از این رو، همان‌گونه که در مقدمه اشاره شد، اگر

T

دارای حذف سور باشد و

M,N\models T

و

M\subseteq N

آن‌گاه

M\preceq N

. ولی عکس این گفته برقرار نیست. در واقع این ویژگی، «مدلْ‌کامل» بودن نام دارد. «زیرساختارْکامل بودن» معادل «حذف سور» است و «مدل‌ْ‌کاملْ بودن» با «معادل بودن هر فرمول، با فرمولی فقط دارای سورهای وجودی» معادل است.
نیز تئوریِ

T

حذف سور می‌پذیرد اگروتنهااگر هر تایپ کاملی در آن با فرمول‌های بدون سور آن تایپ کاملاً تعیین شود. به بیان دیگر، برای هر

a, b

در مدل هیولا و هر زیرمجموعهٔ

A

از مدل هیولا، اگر

qftp(a/A)=qftp(b/A)

آن‌گاه

tp(a/A)=tp(b/A)

؛ که منظور از

qftp(a/A)

مجموعهٔ همهٔ فرمول‌های بدون سور با پارامتر در

A

است که

a

آن‌ها را برآورده می‌کند.

مثالها

داشتن حذف سور، تنها در یک «زبان معقول» حائزِ اهمیت است. این زبان عموماً بهینه‌ترین زبانی است که ویژگی‌های جبری یک تئوری را بتواند بیان کند. اگر جز این بخواهد باشد، هر تئوری‌ای با اضافه کردن محمول برای هر فرمول دارای سور به زبان، دارای حذف سور می‌شود. به بیان واضح‌تر اگر برای هر فرمولِ $\phi ({\bar {x}},{\bar {y}})$

محمول

p_{\phi }

را به زبان و جملهٔ

\forall {\bar {x}}[\exists {\bar {y}}\phi ({\bar {x}},{\bar {y}})\leftrightarrow p({\bar {x}})]

را به تئوری بیفزاییم، به یک تئوری دارای حذف سور می‌رسیم.

اعداد طبیعی و حساب پئانو

ساختارِ به‌ظاهرسادهٔ $(\mathbb {N} ,+,.,0,1,<)$

سورها را حذف نمی‌کند. مسئلهٔ حذف سور برای این ساختار، هم‌ارزِ مسئلهٔ ناکامل بودن اصول پئانو برای حساب است که گودل آن را ثابت کرده‌است. نیز به بیان دیگر، این مسئله معادل مسئلهٔ وجود یک زیرمجموعهٔ بازگشتی شمارش‌پذیر (آر. ای) از

\mathbb {N}

است که بازگشتی نباشد. در واقع زیرمجموعه‌های بازگشتی‌ِ شمارش‌پذیرِ

\mathbb {N}

دقیقاً آنهایند که با فرمولهای

\exists {\bar {x}}p(y,x)

تعریف می‌شوند که در آن

p

یک چندجمله‌ای در

\mathbb {N} [{\bar {X}},Y]

باشد.

حساب پِرِسْبِرگِر

برخلافِ حسابِ پئانو، «حسابِ پِرِسْبِرگِر» دارای حذف سور است. حساب پرسبرگر، به بیان ساده حسابی است که از تئوریِ کاملِ ساختار $(\mathbb {Z} ,+,,0,1,p_{n},<)$

به دست می‌آید که در آن تعبیرِ محمولِ

p_{n}

زیرمجموعهٔ

n\mathbb {Z}

از

\mathbb {Z}

است. نتیجهٔ تأمل‌برانگیزِ حذف سور حساب پرسبرگر این است که بر خلاف

(\mathbb {Z} ,+,.)

که گرفتار دشواری‌های قضیهٔ ناتمامیت گودل است، ساختارِ

(\mathbb {Z} ,+,<)

تصمیم‌پذیر است. حساب پرسبرگر دارای یک اصل‌بندی ساده است که ویژگی‌های گروه جمعیِ ترتیبیِ

(\mathbb {Z} ,+,<)

را به همراه تعبیرِ

p_{n}

ها بیان می‌کند.

میدانهای بستهٔ حقیقی

تئوریِ کاملِ ساختارِ $(\mathbb {R} ,+,.,0,1,<)$

سورها را حذف می‌کند (تارسکی). این حذف سور، نتایج جبری و توپولوژیک بااهمیتی در پی دارد. نخست این که تئوریِ کامل این ساختار، دقیقاً تئوری میدان‌های بستهٔ حقیقی است. میدان‌های بستهٔ حقیقی، میدانهایی هستند که در آنها

-1

مجموع مربعات نباشد. و هیچ توسیع جبری‌ای نداشته باشند که در آن

-1

مجموع مربعات باشد.
بنا به حذف سور، اصل‌بندی زیر برای میدان‌های بستهٔ جبری، «کامل» است و از این رو میدان‌های بسته‌جبری دقیقاً مدلهای تئوریِ کاملِ ساختارِ

(\mathbb {R} ,+,.,0,1,<)

هستند. نیز تئوری زیر، «مدل‌کامل» و تصمیم‌پذیر است.

اصولی که بیان کند که $(R,+,.,0,1,<)$ میدانی مرتب است.
مجموعه‌ای از اصول که بیان کنند که چندجمله‌ای‌های با درجهٔ فرد دارای ریشه‌اند.
اصلی که بگوید که $-1$ مجموع مربعات نیست.
اصلی که بیان کند که خودِ هر عنصر یا قرینهٔ آن مجذور عنصر دیگری است.

مجموعه‌های تعریف شدنی با فرمول‌های بدون سور در میدان‌های بستهٔ جبری، دقیقاً «مجموعه‌های شبه‌جبری» هستند. یعنی آن‌هایی که به گونهٔ زیر تعریف شوند: $\{{\bar {x}}|\bigwedge _{i=1,\ldots ,n}f_{i}({\bar {x}})>0\wedge \bigwedge _{i=1,\ldots ,n}g_{i}(x)=0\}$

که در آن

f_{i}

ها و

g_{i}

چندجمله‌هایی در

\mathbb {R} [{\bar {X}}]

هستند. از آنجا که سورهای وجودی تصویر مجموعه‌ها روی محورها را به دست می‌دهند، حذف سورِ میدان‌های بستهٔ جبری در واقع، معادل این گفته‌است که «در میدانهای بستهٔ جبری، هر تصویر هر مجموعهٔ شبه‌جبری، خود نیز مجموعه‌ای شبه‌جبری است. در واقع، حذف سور، راهبردی بود تارسکی برای اثبات این قضیه پیش گرفت.
از دیگر نتیجه‌های حذف سور برای میدانهای بستهٔ جبری، این است که این میدانها «کمینهٔ ترتیبی» هستند (اُمینیمال). یعنی مجموعه‌های تعریف شدنی با یک متغیر در آنها، اجتماعی متناهی از نقطه‌ها و بازه‌های باز هستند (و از این رو بنا به قضیهٔ تقسیم سلولی، مجموعه‌های تعریف شدنی در ابعاد بزرگتر، اجتماعی متناهی از سلول‌ها هستند). ترتیب‌کمینگی این ساختار، ارتباط سودمندی میان نظریهٔ مدل و تویولوژی برقرار می‌کند.

میدانِ ترتیبیِ اعداد حقیقی به همراه جرم توابع تحلیلیِ حقیقی

تئوری میدان بستهٔ حقیقی $\mathbb {R}$

بهمراه «جرم توابع تحلیلی حقیقی» و جمع و ضرب و کمتریِ تحدید شده، مدل‌کامل است، یعنی هر فرمولی در آن معادل فرمولی به صورت

\exists {\bar {x}}\quad \phi ({\bar {x}},{\bar {y}})

است که در آن

\phi

فرمولی بدون سور است. (وَن‌ْ دِنْ دریز) به بیان دیگر، اگر با

F

خانوادهٔ همهٔ توابع تحلیلیِ حقیقیِ محدود شده به بازهٔ بستهٔ

[-1,1]

را نشان دهیم، و با

D

تابع تغییردادهٔ شدهٔ تقسیم را که هر جا

|x/y|\leq 1

باشد تعریف شده‌است، تئوریِ ساختارِ

(\mathbb {R} ,0,1,\{f\}_{f\in F},D)

سورها را حذف می‌کند.
در نتیجهٔ حذف سور به راحتی می‌توان نشان داد که ساختار یادشده، کمینهٔ ترتیبی است. نیز اهمیت دیگر حذف سور در این ساختار این است، که اثباتی نظریهٔ مدلی برای قضیهٔ هندسیِ «گابْرییِلُف» فراهم می‌آورد. بنا بر قضیهٔ گابرییلف، مکمل هر مجموعهٔ زیرْتحلیلی در

\mathbb {R}

مجموعه‌ای زیرْتحلیلی است. مجموعه‌های زیرتحلیلی، با گرفتن تصاویرِ مجموعه‌های شبه‌تحلیلی روی محورها به دست می‌آیند. نیز، مجموعه‌های شبه‌تحلیلی، دقیقاً مجموعه‌هایی هستند که در ساختارِ

\mathbb {R} _{an}=(\mathbb {R} ,0,1,\{f\}_{f\in F})

بدون سور تعریف می‌شوند.

میدانهای بستهٔ جبری

تئوری کاملِ ساختار $(\mathbb {C} ,+,.,-,0,1)$

سورها را حذف می‌کند (رابینسون). تئوری این ساختار، از این رو، معادل با تئوری میدان‌های بستهٔ حقیقی با مشخصهٔ صفر است. در نتیجهٔ حذف سور، تئوری میدان‌های بستهٔ جبری مدلْ‌کامل است و تئوری میدان‌های بستهٔ جبری با مشخصهٔ

p

(که

p

می‌تواند بی‌نهایت نیز باشد) کامل است.
حذف سور در میدان‌های بستهٔ جبری نیز نتایج جبری خوشایندی به دست می‌دهد. در واقع حذف سور در این میدان‌ها معادل قضیهٔ «شُوالی» است که می‌گوید «تصویر هر مجموعهٔ ساخته‌شدنی تحت یک نگاشت چندجمله‌ای مجموعه‌ای ساخته‌شدنی است». مجموعه‌های ساخته‌شدنی در میدان‌های بستهٔ جبری، ترکیبات بولی متناهیِ مجموعه‌های بستهٔ زاریسکی هستند. به بیان دیگر، آن‌ها مجموعه‌های «تعریف‌شدنی» با فرمول‌های بدون سور در یک میدان بستهٔ جبریند. طبیعی است که تصویر آن‌ها تحت نگاشت‌های چندجمله‌ای، دوباره تعریف شدنی، و بنا به حذف سور، بدون‌سورتعریف‌شدنی، و از این رو ساخته‌شدنی است.
نیز حذف سور (در واقع مدل‌کاملی نتیجه‌شونده از آن) اثبات آسانی برای قضیهٔ ریشه‌های هیلبرت (نول‌اِشتِلِنْ‌سَتز) فراهم می‌آورد. بنا به این قضیه، در میدان‌های بستهٔ جبری، مجموعه‌های بستهٔ زاریسکی در تناظر یک‌به‌یکند با ایده‌آل‌های رادیکال در حلقهٔ چندجمله‌ای‌های متناظر.
نتیجهٔ دیگرِ حذف سور در میدان‌های بستهٔ جبری، این است که آن‌ها بسیارکمینه هستند. یعنی اگر

K

یک میدان بستهٔ جبری باشد، هر زیرمجموعهٔ تعریف شدنی از

K

یا خودْ یا مکملش متناهی است (یعنی این مجموعه را می‌توان تنها با نمادِ تساوی تعریف کرد).

میدان ترتیبی اعداد حقیقی به همراه تابعِ نمایی نامحدود

تئوریِ ساختارِ $\mathbb {R} _{\exp }=(\mathbb {R} ,+,.,0,1,\exp )$

یک تئوری مدل‌ْکامل است (ویلکی)؛ یعنی هر فرمول در آن معادلی دارد که تنها دارای سوروجودی است. نکتهٔ تأمل‌برانگیز این است که در این جا تابع نمایی، محدود در نظر گرفته نشده‌است و بنابراین این قضیه از قضیهٔ ون‌دِن‌دریز برای

\mathbb {R} _{an}

نتیجه نمی‌شود. نیز بنا به حذف سور، این تئوری ترتیب‌کمینه است. اگر «حدس شانوئل» درست باشد، این تئوری، تصمیم‌پذیر است. حدس شانوئل این است که اگر

\lambda _{1},\ldots ,\lambda _{n}\in \mathbb {C}

روی

\mathbb {R}

مستقل «خطی» باشند، آن‌گاه مرتبهٔ تعالی میدانِ

\mathbb {Q} (\lambda _{1},\ldots ,\lambda _{n},e^{\lambda _{1}},\ldots ,e^{\lambda _{n}})

حداقل،

n

است. تصمیم‌پذیری تئوریِ

\mathbb {R} _{exp}

موردِ سؤالی از تارسکی بوده‌است.

زوجهای چگال از میدانهای بستهٔ حقیقی

فرض کنید $T$

تئوری «زوجهای چگال از میدانهای بستهٔ حقیقی» باشد (این تئوری، کامل است). به بیان دیگر زوج

(M,N)

مدلی از

T

است اگروتنهااگر

M

و

N

دو میدان بستهٔ حقیقی در زبانِ

L_{or}=\{+,.,-,0,1,<\}

باشند و

N

در

M

چگال باشد؛ یعنی هر بازهٔ باز که دو سر آن عناصرِ

M

باشند، دارای نقطه‌ای در

N

باشد. این تئوری را می‌توان تئوریِ کاملِ ساختارِ

({\overline {\mathbb {R} }},\mathbb {R} _{alg})

دانست که در آن منظور از

\mathbb {R} _{alg}

میدان بستهٔ حقیقی متشکل از همهٔ عناصر جبری روی

\mathbb {Q}

است و خطِ بالایِ

\mathbb {R}

یعنی این میدان به همراه جمع و ضرب و کمتری و صفر و یک. تئوریِ

T

در زبانِ

L_{or}\cup \{p\}

که در آن

p

یک نماد محمولی یک ظرفیتی برای میدانِ کوچکتر (

N

) است، دارای حذف سوری این‌چنین است: هر فرمولی در این زبان، معادل ترکیبی بولی از فرمولهایی به صورت

\exists {\bar {x}}\in p\quad \phi ({\bar {x}},{\bar {y}})

است که در آن

\phi \in L_{or}

.
تئوری یادشده، ترتیب کمینه نیست ولی همچنان از لحاظ توپولوژیک خوش‌رفتار است: هر مجموعهٔ باز از

\mathbb {R}

که در ساختار

({\overline {\mathbb {R} }},\mathbb {R} _{alg})

تعریف شدنی باشد، اجتماعی متناهی از بازه هاست. در واقع هر مجموعهٔ باز تعریف شدنی در این ساختار، در خودِ

{\overline {\mathbb {R} }}

تعریف شدنی است. نیز هر زیرمجموعه از

\mathbb {R} _{alg}^{n}

که در این ساختار تعریف شدنی باشد، اشتراکِ

\mathbb {R} _{alg}

با زیرمجموعه‌ای چون

X^{n}

از

\mathbb {R}

است که با فرمولی در

L_{or}

تعریف شده باشد. نیز هر زیرمجموعه‌ای چون

X

از

\mathbb {R}

که در این ساختار تعریف‌شدنی باشد تجزیه‌ای به‌گونهٔ

I_{1}\cup \ldots \cup I_{n}

دارد که در آن هر

I_{i}

یا یک بازهٔ بازِ زیرمجموعهٔ

X

است یا یک نقطه است، یا یک بازهٔ باز به‌گونه‌ای است که

X\cap I

و

X^{c}\cap I

در

I

چگال است. مشابه این گفته برای مجموعه‌های تعریف شدنی در ابعاد بالاتر نیز برقرار است (تجزیهٔ سلولی چگال و مکمل‌ْچگال). در نتیجه

\mathbb {N}

در این ساختار تعریف شدنی نیست و این امر برای در امان بودن از دشواری‌های ناتمامیت، در ساختارهای نظریهٔ مدلی اهمیت دارد.

میدانهای ارزیابی

تئوری میدان‌های ارزیابی‌ِ بستهٔ جبریِ که در آن مشخصهٔ میدانِ اصلی و میدانِ خارج‌قسمتی تبیین شده‌است، در زبانِ به دست آمده از اجتماع زبان میدان‌ها با محمول دوظرفیتیِ $v(x)\leq v(y)$

، سورها را حذف می‌کند (رابینسون).
در حالت کلی‌تر، میدان‌های ارزیابیِ (نه لزوماً بستهٔ جبری) هنسلیِ دارای مؤلفهٔ زاویه‌ای، به گونهٔ

(K,k,\Gamma ,v,ac)

را در زبان سه‌بخشیِ

L=L_{K}\cup L_{k}\cup L_{\Gamma }\cup \{v,ac\}

مطالعه می‌کنند که حامل سه بخش برای میدان اصلی و میدان خارج‌قسمتی و گروه ارزیابی‌هاست. نگاشت ارزیابی با نماد

v:K\to \Gamma

نشان داده شده‌است. نیز

ac:K\to k

نگاشت مؤلفهٔ زاویه‌ای، یک همومرفیسم گروه ضربی است که نگاشت کانونیِ

res:R\to R/m

، را «روی عناصرِ یکهٔ

R

» گسترش می‌دهد. در این زبان می‌توان نشان داد که میدان‌های ارزیابی هنسلی دارای مؤلفهٔ زاویه‌ای و با مشخصهٔ صفر برای میدان خارج‌قسمتی، سورها را از میدانِ اصلی، یعنی

K

، حذف می‌کنند. به بیان دیگر، اگر دو میدان ارزیابیِ

(K,k,\Gamma ,v,ac)

و

(K',k',\Gamma ',v',ac')

داشته باشیم و بدانیم که

\Gamma \equiv \Gamma '

(به عنوان دو گروه آبلی بخش‌پذیرِ بدونِ تاب) و

k\equiv k'

(به عنوان دو میدان) آنگاه

(K,k,\Gamma ,v,ac)\equiv (K',k',\Gamma ',v,ac)

.
حذف سور تبعات خوشایند زیادی نیز برای میدان‌های ارزیابی دارد. برای مثال، تئوری میدان‌های بستهٔ جبریِ با مشخصهٔ مشخص، سی‌کمینال (سی‌مینیمال) است. یعنی مجموعه‌های تعریف شدنی در آن ساختاری درخت‌مانند دارند.
نیز در میدان‌های ارزیابیِ بستهٔ جبری، گروه ارزیابی‌ها و میدان خارج‌قسمتی، هر یک «ثابت‌ْنشانده» هستند. یعنی زیرمجموعه‌هایی از آن‌ها را که در کل ساختار تعریف‌شدنی باشند می‌توان در خودِ ساختار گروه، یا در خودِ ساختارِ میدان و بدون کمک‌گیری از بقیهٔ زبان تعریف کرد. این نکته دربارهٔ میدان‌های ارزیابیِ هنسلی دارای مشخصهٔ خارج‌قسمتیِ صفر و دارای مؤلفهٔ موضعی نیز درست است.

روش‌های معمول برای بررسی حذف‌سور

پیدا کردن معادل بدون سور به روش مستقیم و با دستکاری فرمولها، برای یک فرمول پیچیدهٔ دارای سور همواره عملی‌ترین راه آزمودن حذف سور نمی‌تواند باشد، به ویژه وقتی که زبان دارای چندین بخش است و فرمول‌ها بسیار پیجیده‌اند. عموماً حذف سور را با کمک گرفتن از «محکهای جبری» زیر می‌آزمایند.

روش اول

تئوری $T$

دارای حذف سور است اگر و تنها اگر برای هر دو مدلِ

M_{0},M_{1}\models T

و هر زیرساختارِ مشترک از این‌دو مانند

A\subseteq M_{0},M_{1}

هر فرمولِ

\phi (x,{\bar {a}})

که عطفی از فرمول‌های اتمی (فرمول‌های ساخته شده با کمک تساوی و نقیض و ترم‌ها و رابطه‌های زبان) است و پارامترهای

{\bar {a}}

در آن از

A

می‌آیند، داشته باشیم

M_{0}\models \exists x\quad \phi (x,{\bar {a}})\Leftrightarrow M_{1}\models \exists x\quad \phi (x,{\bar {a}}).

روش دوم، راژمانهای رفت و برگشتی

همان‌گونه که در تعریف حذف سور اشاره شد، برای این که یک تئوری حذف سور بپذیرد، باید تایپ‌های کامل عناصر را تایپ‌های بدون سور آن‌ها به دست بدهند. فرض کنید $M_{1}$

و

M_{2}

مدلهایی بسیار اشباع باشند و

{\bar {a}}\in M_{1}

و

{\bar {b}}\in M_{2}

. بامهارتهای اولیهٔ نظریهٔ مدلی می‌توان نشان داد که

qttp^{M_{1}}({\bar {a}})=qftp^{M_{2}}({\bar {b}})

اگر و تنها اگر زیرساختاری از

M_{1}

که

{\bar {a}}

آن را تولید می‌کند با زیرساختاری از

M_{2}

که

{\bar {b}}

آن را تولید می‌کند، ایزومرف باشد. یادآوری می‌کنیم که

q f t p

نشانگر تایپ بدون سور است. نیز

tp^{M_{1}}({\bar {a}})=tp^{M_{2}}({\bar {b}})

هرگاه یک نگاشت مقدماتی جزئی داشته باشیم که

{\bar {a}}

را به

{\bar {b}}

ببرد.
هرگاه یک «راژمان رفت و برگشتی» از ایزومرفیسم‌های میان زیرساختارهای

M_{1}

و

M_{2}

وجود داشته باشد که ایزومرفیسم میان ساختار تولید شده توسط

{\bar {a}}

در

M_{1}

و ساختار تولید شده توسط

{\bar {b}}

در

M_{2}

در میان آن‌ها باشد، آن‌گاه

tp^{M_{1}}({\bar {a}})=tp^{M_{2}}({\bar {b}})

.
به بیان دقیق‌تر، موارد زیر با هم معادلند:

تئوری $T$ دارای حذف سور است،
تایپ‌های کامل در تئوریِ $T$ را تایپ‌های بدون سور کاملاً تعیین می‌کنند،
هرگاه $M_{1}$ و $M_{2}$ دو مدلِ به‌اندازه‌اشباع و هم‌اندازه‌اشباع از $T$ باشند و ${\bar {a}}\in M_{1}$ و ${\bar {b}}\in M_{2}$ ، آنگاه اگر ساختار تولید شده بوسیلهٔ ${\bar {a}}$ در $M_{1}$ با ساختار تولید شده توسط ${\bar {b}}$ در $M_{2}$ ایزومرف باشد، این ایزومرفیسم را می‌توان یک نگاشت مقدماتی میانِ $M_{1}$ و $M_{2}$ گستراند.
هرگاه $M_{1}$ و $M_{2}$ دو مدلِ $\omega$ -اشباع از $T$ باشند و ${\bar {a}}\in M_{1}$ و ${\bar {b}}\in M_{2}$ ، آنگاه اگر ساختار تولید شده بوسیلهٔ ${\bar {a}}$ در $M_{1}$ با ساختار تولید شده توسط ${\bar {b}}$ در $M_{2}$ ایزومرف باشد، برای هر $c\in M_{1}$ بتوان $d\in M_{2}$ را پیدا کرد که ساختار تولید شده بوسیلهٔ ${\bar {a}},c$ در $M_{1}$ با ساختار تولید شده توسط ${\bar {b}},d$ در $M_{2}$ ایزومرف باشد. نیز برای هر $d\in M_{2}$ بتوان $c\in M_{1}$ را چنان یافت که ساختار تولید شده توسط ${\bar {a}},c$ در $M_{1}$ با ساختار تولید شده توسط ${\bar {b}},d$ در $M_{2}$ ایزومرف باشد. توجه کنید که این فراروندِ رفت و برگشتی، نامتناهی است یعنی برای هر $n\in \mathbb {N}$ هرگاه $\langle {\bar {a}},c_{1},\ldots ,c_{n-1}\rangle \simeq \langle {\bar {b}},d_{1},\ldots ,d_{n-1}\rangle$ آن‌گاه برای هر $c_{n}$ در $M_{1}$ عنصری مانند $d_{n}\in M_{2}$ پیدا شود که $\langle {\bar {a}},c_{1},\ldots c_{n-1},c_{n}\rangle \simeq \langle {\bar {b}},d_{1},\ldots d_{n-1},d_{n}\rangle$ ، و نیز برای هر $d_{n}$ در $M_{2}$ عنصری مانند $c_{n}\in M_{1}$ پیدا شود که $\langle {\bar {a}},c_{1},\ldots ,c_{n-1},c_{n}\rangle \simeq \langle {\bar {b}},d_{1},\ldots ,d_{n-1},d_{n}\rangle$ ،
هرگاه $M_{1}$ و $M_{2}$ دو مدل به‌اندازه و هم‌اندازه اشباع از $T$ باشند و $f:\langle {\bar {a}}\rangle \to \langle {\bar {b}}\rangle$ ایزومرفیسمی میان دو ساختار متناهیاً تولید شده از آندو، آنگاه $f$ در یک راژمان رفت و برگشتی واقع شود. یعنی مجموعه‌ای چون $F=\{f_{i}:M_{i}^{1}\to M_{i}^{2}\}$ از ایزومرفیسمهایی میان زیرساختارهایی (نه لزوماً‌همه‌ٔ‌زیرساختارها) از $M_{1}$ و $M_{2}$ داشته باشیم که $f$ را در برداشته باشد و نیز دارای این ویژگی باشد که هرگاه $g\in F$ و $c\in M_{1}$ آنگاه نگاشتی چون $h\in F$ داشته باشیم که $g$ را بگستراند و $c$ در دامنه‌اش باشد. نیز هرگاه $g\in F$ و $d\in M_{2}$ آن‌گاه نگاشتی چون $h\in F$ داشته باشیم که $g$ را بگستراند و $b$ در بُردش باشد.

روش سوم

برای هر $A\models T_{\forall }$ یک مدلِ $M\models T$ پیدا شود که $A$ را دربردارد و برای هر $N\models T$ که $A$ را دربرداشته باشد، $M$ در $N$ بنشیند و نگاشت نشاندنِ $M$ در $N$ روی $A$ همانی باشد.
برای هر مدلِ $M\subseteq N$ از $T$ و هر عنصرِ $n\in N$ ساختار تولید شده به وسیلهٔ $M, n$ را بتوان در یک گسترش مقدماتی از $M$ نشاند به گونه‌ای این نگاشت نشاندن روی $M$ این تابع همانی باشد.

روش چهارم

اگر تئوریِ $T$

دو شرط جبری زیر را برآورد، آن‌گاه سورها را حذف می‌کند:

$T$ دارای مدل اولیهٔ جبری باشد. یعنی برای هر $A\models T_{\forall }$ مدلی مانند $M\models T$ و نشاندنی مانند $f:A\to M$ یافت شوند به گونه‌ای که برای هر مدلِ $N\models T$ و هر نشاندنِ $g:A\to N$ نشاندنی چون $l:M\to N$ پیدا شود که $g=l\circ f$ .
هرگاه $M,N\models T$ و $M\subseteq N$ ، برای هر فرمولِ بدون سورِ $\phi ({\bar {x}},y)$ و هر ${\bar {m}}\in M$ اگر $N\models \exists y\quad \phi ({\bar {m}},y)$ آنگاه $M\models \exists y\quad \phi ({\bar {m}},y)$ .

روش پنجم

موارد زیر با هم معادلند (تعاریف در ادامه آمده‌است).

تئوریِ $T$ دارای حذف سور است.
تئوریِ $T$ مدل‌کامل است و تئوری $T_{\forall }$ (همهٔ نتیجه‌های با سور عمومی از $T$ )دارای ویژگی پیوندی است.

مفاهیم نزدیک به حذف سور

کامل بودن

تئوریِ $T$

را «کامل» می‌خوانند هرگاه هر جمله‌ای یا نقیضِ آن از

T

نتیجه شود. اگر

T

کامل باشد و

M\models T

آن‌گاه

T

با تئوریِ کاملِ

th(M)

هم‌ارز است. یعنی هر ویژگی‌ای که در یکی از مدلهای

T

برقرار باشد، در همهٔ مدل‌های دیگر نیز برقرار خواهد بود. به بیان دیگر، اگر

T

کامل باشد و

M,N\models T

آن‌گاه

M\equiv N

؛ یعنی

M

و

N

هم‌ارز مقدماتی هستند.
هرگاه

T

کامل باشد، می‌توان مدلی بسیار بزرگ از آن را برای کار اندر آن برگزید و و آن را مدل «هیولا» خواند و همهٔ مدل‌ها را زیرمدلی از مدل هیولا دانست. نیز بررسی تایپ‌ها عموماً در تئوری‌های کامل و در مدل هیولا صورت می‌پذیرد.
اگر

T

دارای حذف سور باشد و مدلی داشته باشد که در سایر مدل‌های دیگر، مقدماتی نشانده شود، آنگاه

T

کامل است. کامل بودن بسیاری از تئوریها، مانند میدان‌های بستهٔ حقیقی و میدان‌های بستهٔ جبری، با کمک این نکته ثابت می‌شود.
همان‌گونه که در تعریف گفتیم، تئوریِ

T

دارای حذف سور است اگر و تنها اگر برای هر مدل

M\models T

و هر زیرساختارِ

A\subseteq M

تئوریِ

T\cup Diag(A)

یک تئوری کامل باشد.

مدلْ‌کامل بودن

بسیاری از تئوری‌ها کامل نیستند ولی ویژگی‌ای را نزدیک به کامل‌بودن دارا هستند که آن را «مدل‌کامل» بودن می‌خوانند.
تئوریِ $T$

را مدل‌ْکامل می‌خوانند هرگاه برای هر مدلِ

M\models T

تئوریِ

T\cup Diag(M)

در زبان

L_{M}

یک تئوری کامل باشد. منظور از

Diag(M)

مجموعهٔ همهٔ جمله‌های بدون سورِ درست در

M

است و منظور از

L_{M}

زبانی است که با افزودن ثابت برای عنصرِ

M

به زبانِ تئوریِ

T

به دست آمده باشد. به بیان دیگر، تئوریِ

T

مدل‌کامل است اگروتنهااگر هر مدل از آن بستهٔ وجودی باشد؛ یعنی اگر

M\models T

و

\phi ({\bar {x}},{\bar {y}})

یک فرمول بدون سور باشد و

M\subseteq N\models T

آن گاه برای هر

{\bar {m}}\in M

داریم

N\models \exists {\bar {x}}\quad \phi ({\bar {x}},{\bar {m}})\Leftrightarrow M\models \exists {\bar {x}}\quad \phi ({\bar {x}},{\bar {m}})

. نیز به بیان دیگر، تئوریِ

T

مدل‌کامل است اگروتنهاگر برای هر دو مدلِ

M\subseteq N\models T

داشته باشیم

M\preceq N

؛ یعنی

M

زیرمدلی مقدماتی از

N

باشد. تئوریِ

T

مدل‌کامل است اگروتنهااگر هر فرمولی در آن معادلی با فقط سور وجودی داشته باشد. به بیان دیگر هر فرمول با متغیرِ آزادِ

{\bar {y}}

معادلی به گونهٔ

\exists {\bar {x}}\quad \phi ({\bar {x}},{\bar {y}})

داشته باشد. که در آن

\phi

فرمولی بدون سور است.
از آنجا که «تایپ» مفهومی مقدماتی است (یعنی هر تایپ در یک گسترش مقدماتی برآورده می‌شود) به مدل‌کامل بودن یک تئوری برای بررسی تایپ‌های آن در مدل هیولا نیاز است. اگر

T

حذف سور داشته باشد، مدل‌ْکامل است.

همپای مدلی

برای بررسی راحت‌ترِ ویژگی‌های تئوری‌های ناکامل، می‌توان «همپای مدلی» آن‌ها را در صورت وجود بررسی کرد که مدل‌ْکامل است. تئوریِ $T^{'}$

را «همپای مدلی» تئوری

T

می‌خوانیم هرگاه

T^{'}

مدل‌ْکامل باشد و

T_{\forall }=T'_{\forall }

. منظور از

T_{\forall }

مجموعهٔ همهٔ جمله‌های با سور عمومی است که از

T

نتیجه می‌شوند. به بیان دیگر،

T_{\forall }=T'_{\forall }

یعنی هر مدل از

T

را بتوان به یک مدل از

T^{'}

گستراند و هر مدل از

T^{'}

را به یک مدل از

T

. همپای مدلی یک تئوری لزوماً همیشه موجود نیست، ولی در صورت وجود، یکتاست.
تئوریِ

T

دارای همپای مدلی است، اگروتنهااگر کلاس همهٔ مدل‌های بسته‌ٔوجودیِ آن، کلاسی مقدماتی باشد. در واقع همپای مدلیِ

T

، تئوری‌ِ این کلاس مقدماتی است. مدلِ

M\models T

را «بستهٔ وجودی» می‌خوانند هرگاه برای هر

M\subseteq N\models T

و هر فرمولِ بدون سورِ

\phi ({\bar {x}},{\bar {m}})

که در آن

{\bar {m}}\in M

داشته باشیم

N\models \exists {\bar {x}}\quad \phi ({\bar {x}},{\bar {m}})\Leftrightarrow M\models \exists {\bar {x}}\quad \phi ({\bar {x}},{\bar {m}})

.

مُکمّلِ مدلی

اگر $T^{'}$

همپای مدلیِ

T

باشد و

T

دارای «ویژگی پیوندی» (همان گونه که در زیر آمده‌است) باشد، آن‌گاه

T^{'}

را «مکمل مدلیِ»

T

می‌خوانیم. مکمل‌ِ مدلی یک تئوری به داشتن حذف سور نزدیک است؛ از آن رو که مکملِ مدلیِ یک تئوری با اصل‌بندیِ جهانی (

T=T_{\forall }

) دارای حذف سور است.
نیز

T^{'}

مکمل مدلیِ

T

است. اگروتنهااگر همپای مدلی

T

باشد و برای هر

M\models T

تئوریِ

T'\cup Diag(M)

در زبان

L_{M}

یک تئوری کامل باشد.

ویژگی پیوندی

تئوریِ $T$

دارای «ویژگیِ پیوندی» است. هرگاه هر دو مدل آن را که دارای زیرمدلی مشترک باشند بتوان به هم پیوند زد. به بیان دقیق‌تر هرگاه

M_{0},M_{1},M_{2}

سه مدلِ

T

باشند و

f_{1}:M_{0}\to M_{1}

و

f_{2}:M_{0}\to M_{2}

دو نشاندن باشند، آنگاه یک مدلِ

N

از

T

و دو نشاندنِ

g_{1}:M_{1}\to N

و

g_{2}:M_{2}\to N

موجود باشند که

g_{1}\circ f_{1}=g_{2}\circ f_{2}

.
ویژگی پیوندی با حذف سور رابطهٔ نزدیکی دارد. نخست توجه کنید که «پیوند» در حالت مقدماتی همیشه ممکن است؛ یعنی اگر

M_{0},M_{1},M_{2}

سه ساختار باشند و

f_{i}:M_{0}\to M_{1}

برای

i=1,2

دو «نشاندن مقدماتی» باشند، آنگاه یک ساختارِ

N

به همراه نشاندن‌های مقدماتی

g_{i}:M_{i}\to N

پیدا می‌شوند که

g_{1}\circ f_{1}=g_{2}\circ f_{2}

. از آنجا که در حضور حذف سور، هر زیرمدلی، زیرمدلی مقدماتی است رابطهٔ میان ویژگی پیوندی و حذف سور توجیه شدنی است.
در واقع موارد زیر با هم معادلند:

تئوریِ $T$ دارای حذف سور است.
تئوریِ $T$ مدل‌کامل است و تئوری $T_{\forall }$ (همهٔ نتیجه‌های با سور عمومی از $T$ ) دارای ویژگی پیوندی است.

منابع

↑ Model Theory: An Introduction, Marker, D. url={https://books.google.de/books?id=vTIVswEACAAJ}, 2014, Springer
↑ Model Theory, Hodges, W. ,Encyclopedia of Mathematics and its Applications}, url={https://books.google.de/books?id=Rf6GWut4D30C},1993,Cambridge University Press
↑ A Course in Model Theory, Tent, K. and Ziegler, M. , seriesLecture Notes in Logic, url={https://books.google.de/books?id=D9sClsdErEsC}, 2012, Cambridge University Press
↑ Wilkie, Alex J. "Model completeness results for expansions of the ordered field of real numbers by restricted Pfaffian functions and the exponential function." Journal of the American Mathematical Society 9.4 (1996): 1051-1094.
↑ Van Den Dries, Lou. "Dense pairs of o-minimal structures." Fundamenta Mathematicae 157.1 (1998): 61-78.
↑ Van Den Dries, Lou. "The field of reals with a predicate for the powers of two." Manuscripta Mathematica 54.1 (1985): 187-195.
↑ Pas, Johan. "Uniform p-adic cell decomposition and local zeta functions." J. reine angew. Math 399 (1989): 137-172.
↑ Denef, Jan, and Lou Van den Dries. "P-adic and real subanalytic sets." Annals of Mathematics 128.1 (1988): 79-138.
↑

مدل‌کاملی کششهای میدان ترتیبی اعداد حقیقی با تابعهای پفافی محدود شده و با تابع نمایی، الکس ویکلی، ترجمهٔ م. خانی، http://home.mathematik.uni-freiburg.de/khani/tajomeye-alex-.pdf

[1] Model Theory: An Introduction, Marker, D. url={https://books.google.de/books?id=vTIVswEACAAJ}, 2014, Springer

[2] Model Theory, Hodges, W. ,Encyclopedia of Mathematics and its Applications}, url={https://books.google.de/books?id=Rf6GWut4D30C},1993,Cambridge University Press

[3] A Course in Model Theory, Tent, K. and Ziegler, M. , seriesLecture Notes in Logic, url={https://books.google.de/books?id=D9sClsdErEsC}, 2012, Cambridge University Press

[4] Wilkie, Alex J. "Model completeness results for expansions of the ordered field of real numbers by restricted Pfaffian functions and the exponential function." Journal of the American Mathematical Society 9.4 (1996): 1051-1094.

[5] Van Den Dries, Lou. "Dense pairs of o-minimal structures." Fundamenta Mathematicae 157.1 (1998): 61-78.

[6] Van Den Dries, Lou. "The field of reals with a predicate for the powers of two." Manuscripta Mathematica 54.1 (1985): 187-195.

[7] Pas, Johan. "Uniform p-adic cell decomposition and local zeta functions." J. reine angew. Math 399 (1989): 137-172.

[8] Denef, Jan, and Lou Van den Dries. "P-adic and real subanalytic sets." Annals of Mathematics 128.1 (1988): 79-138.

[9] ↑