«حذف سور» (به انگلیسی: Quantifier elimination) یکی از ویژگی های «جبری» مورد بررسی در منطق ریاضی (در نظریهٔ مدلها) است.تئوریِ T {\displaystyle T} دارای حذف سور است (یا سورها را حذف می کند)هرگاه هر فرمولی به پیمانهٔ آن معادلی بدون سور داشته باشد.مصداقِ ملموسی از حذف سور،فرمول تعیین کنندهٔ ریشه داشتن یا نداشتن یک معادلهٔ درجهٔ ۲ در اعداد حقیقی است: ( R , + , . , < , 0 , 1 ) ⊨ ∃ x a x 2 + b x + c = 0 ↔ ( a ≠ 0 ∧ b 2 − 4 a c ≥ 0 ) ∨ ( a = 0 ∧ b ≠ 0 ) ∨ ( a = b = c = 0 ) {\displaystyle (\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 {\displaystyle T} دارای حذف سور باشد، برای بررسی مجموعه های تعریف شدنی در مدل های آن، تنها کافی است مجموعه های تعریف شده با ترکیبات بولیِ فرمول های اتمی را در نظر بگیریم. دوم این که حذف سور، مطالعهٔ جبری مدل ها را ساده می کند. اگر T {\displaystyle T} دارای حذف سور باشد، آن گاه برای هر دومدلِ M , N {\displaystyle M,N} از آن، اگر M {\displaystyle M} زیرساختاری از N {\displaystyle N} باشد، آن گاه M {\displaystyle M} زیرساختاری مقدماتی از N {\displaystyle N} است، یعنی هر جملهٔ مرتبهٔ اول با پارامتر در M {\displaystyle M} اگردر N {\displaystyle N} درست باشد، آن گاه در M {\displaystyle M} نیز درست است. سوم این که، بررسی کامل بودنِ یک تئوری، در صورت حذف سور پذیرفتن آن، آسان تر است. منظور از تئوریِ کامل، تئوری ای است که در آن هر جملهٔ داده شده یا نقیض آن اثبات شدنی است. از این رو اگرروندی تصمیم پذیر برای اثبات حذف سور داشته باشیم، اثبات تصمیم پذیر بودن یک تئوری نیز در حالتی که حذف سور داشته باشد، آسان تر است. چهارمین اهمیت حذف سور،فراهم آوردن توصیف جبری ملموس برای برخی تئوری ها و بدینسان برقرار کردن پیوند میان جبر و نظریهٔ مدل است.برای مثال، بررسی ساختار یا مدل تولید شده توسط یک مجموعهٔ داده شده، یا بررسی بستارِ جبری یک مجموعهٔ داده شده، در تئوری ای که حذف سور داشته باشد، به مراتب آسان تر است.این نکته در مثال های جبری، مانند میدان های بستهٔ حقیقی و میدان های بستهٔ جبریراحت تر به چشم می آید.
تئوریِ T {\displaystyle T} در زبانِ L {\displaystyle L} «دارای حذف سور است»، یا «سورها را حذف می کند» هرگاه برای هر فرمولِ ϕ ( x ¯ ) ∈ L {\displaystyle \phi ({\bar {x}})\in L} فرمولی بدون سور مانند ψ ( x ¯ ) ∈ L {\displaystyle \psi ({\bar {x}})\in L} پیدا شود که T ⊨ ∀ x ¯ ϕ ( x ¯ ) ↔ ψ ( x ¯ ) . {\displaystyle T\models \forall {\bar {x}}\quad \phi ({\bar {x}})\leftrightarrow \psi ({\bar {x}}).} با به روش های مقدماتی منطقی، فرمول بدون سورِ ψ {\displaystyle \psi } را می توان به صورت ⋀ i ⋁ j ψ i j {\displaystyle \bigwedge _{i}\bigvee _{j}\psi _{ij}} یا ⋁ i ⋀ j ψ i j {\displaystyle \bigvee _{i}\bigwedge _{j}\psi _{ij}} در نظر گرفت که در آن هر ψ i j {\displaystyle \psi _{ij}} فرمولی اتمی یا نقیض یک فرمول اتمی است.معادلاً تئوری T {\displaystyle T} دارای حذف سور است، هرگاه «زیرساختارْکامل» باشد. یعنی برای هر مدلِ M ⊨ T {\displaystyle M\models T} و هر زیرساختارِ A ⊆ M {\displaystyle A\subseteq M} تئوریِ D i a g ( A ) ∪ T {\displaystyle Diag(A)\cup T} در زبانِ L A {\displaystyle L_{A}} (زبانی که با افزودن ثابت برای ازای هرعنصرِ A {\displaystyle A} بهزبان تئوریِ T {\displaystyle T} به دست آمده باشد) یک تئوریِ کامل باشد. منظور از D i a g ( A ) {\displaystyle Diag(A)} مجموعهٔ همهٔ جمله های بدون سورِ با پارامتر در A {\displaystyle A} است.از این رو، همان گونه که در مقدمه اشاره شد، اگر T {\displaystyle T} دارای حذف سور باشد و M , N ⊨ T {\displaystyle M,N\models T} و M ⊆ N {\displaystyle M\subseteq N} آن گاه M ⪯ N {\displaystyle M\preceq N} .ولی عکس این گفته برقرار نیست. در واقع این ویژگی،«مدلْ کامل»بودن نام دارد. «زیرساختارْکامل بودن»معادل «حذف سور» است و «مدل ْ کاملْ بودن» با «معادل بودن هر فرمول، با فرمولی فقط دارای سورهای وجودی» معادل است.نیزتئوریِ T {\displaystyle T} حذف سور می پذیرد اگروتنهااگرهر تایپ کاملی در آنبا فرمول های بدون سور آن تایپکاملاً تعیین شود. به بیان دیگر، برای هر a , b {\displaystyle a,b} در مدل هیولا و هر زیرمجموعهٔ A {\displaystyle A} از مدل هیولا، اگر q f t p ( a / A ) = q f t p ( b / A ) {\displaystyle qftp(a/A)=qftp(b/A)} آن گاه t p ( a / A ) = t p ( b / A ) {\displaystyle tp(a/A)=tp(b/A)} ؛ که منظور از q f t p ( a / A ) {\displaystyle qftp(a/A)} مجموعهٔ همهٔ فرمول های بدون سور با پارامتر در A {\displaystyle A} است که a {\displaystyle a} آن ها را برآورده می کند.
داشتن حذف سور، تنها در یک «زبان معقول» حائزِ اهمیت است. این زبان عموماً بهینه ترین زبانی است که ویژگی های جبری یک تئوری را بتواند بیان کند. اگر جز این بخواهد باشد، هر تئوری ای با اضافه کردن محمول برای هر فرمول دارای سور به زبان، دارای حذف سور می شود. به بیان واضح تر اگر برای هر فرمولِ ϕ ( x ¯ , y ¯ ) {\displaystyle \phi ({\bar {x}},{\bar {y}})} محمول p ϕ {\displaystyle p_{\phi }} را به زبان و جملهٔ ∀ x ¯ {\displaystyle \forall {\bar {x}}} را به تئوری بیفزاییم، به یک تئوری دارای حذف سور می رسیم.
ساختارِ به ظاهرسادهٔ ( N , + , . , 0 , 1 , < ) {\displaystyle (\mathbb {N} ,+,.,0,1,<)} سورها را حذف نمی کند.مسئلهٔ حذف سور برای این ساختار،هم ارزِ مسئلهٔ ناکامل بودن اصول پئانو برای حساب است که گودل آن را ثابت کرده است. نیز به بیان دیگر، این مسئله معادلمسئلهٔ وجود یک زیرمجموعهٔبازگشتی شمارش پذیر(آر. ای)از N {\displaystyle \mathbb {N} } است که بازگشتی نباشد. در واقع زیرمجموعه های بازگشتی ِ شمارش پذیرِ N {\displaystyle \mathbb {N} } دقیقاً آنهایند که با فرمولهای ∃ x ¯ p ( y , x ) {\displaystyle \exists {\bar {x}}p(y,x)} تعریف می شوند که در آن p {\displaystyle p} یک چندجمله ای در N {\displaystyle \mathbb {N} } باشد.
تئوریِ T {\displaystyle T} در زبانِ L {\displaystyle L} «دارای حذف سور است»، یا «سورها را حذف می کند» هرگاه برای هر فرمولِ ϕ ( x ¯ ) ∈ L {\displaystyle \phi ({\bar {x}})\in L} فرمولی بدون سور مانند ψ ( x ¯ ) ∈ L {\displaystyle \psi ({\bar {x}})\in L} پیدا شود که T ⊨ ∀ x ¯ ϕ ( x ¯ ) ↔ ψ ( x ¯ ) . {\displaystyle T\models \forall {\bar {x}}\quad \phi ({\bar {x}})\leftrightarrow \psi ({\bar {x}}).} با به روش های مقدماتی منطقی، فرمول بدون سورِ ψ {\displaystyle \psi } را می توان به صورت ⋀ i ⋁ j ψ i j {\displaystyle \bigwedge _{i}\bigvee _{j}\psi _{ij}} یا ⋁ i ⋀ j ψ i j {\displaystyle \bigvee _{i}\bigwedge _{j}\psi _{ij}} در نظر گرفت که در آن هر ψ i j {\displaystyle \psi _{ij}} فرمولی اتمی یا نقیض یک فرمول اتمی است.معادلاً تئوری T {\displaystyle T} دارای حذف سور است، هرگاه «زیرساختارْکامل» باشد. یعنی برای هر مدلِ M ⊨ T {\displaystyle M\models T} و هر زیرساختارِ A ⊆ M {\displaystyle A\subseteq M} تئوریِ D i a g ( A ) ∪ T {\displaystyle Diag(A)\cup T} در زبانِ L A {\displaystyle L_{A}} (زبانی که با افزودن ثابت برای ازای هرعنصرِ A {\displaystyle A} بهزبان تئوریِ T {\displaystyle T} به دست آمده باشد) یک تئوریِ کامل باشد. منظور از D i a g ( A ) {\displaystyle Diag(A)} مجموعهٔ همهٔ جمله های بدون سورِ با پارامتر در A {\displaystyle A} است.از این رو، همان گونه که در مقدمه اشاره شد، اگر T {\displaystyle T} دارای حذف سور باشد و M , N ⊨ T {\displaystyle M,N\models T} و M ⊆ N {\displaystyle M\subseteq N} آن گاه M ⪯ N {\displaystyle M\preceq N} .ولی عکس این گفته برقرار نیست. در واقع این ویژگی،«مدلْ کامل»بودن نام دارد. «زیرساختارْکامل بودن»معادل «حذف سور» است و «مدل ْ کاملْ بودن» با «معادل بودن هر فرمول، با فرمولی فقط دارای سورهای وجودی» معادل است.نیزتئوریِ T {\displaystyle T} حذف سور می پذیرد اگروتنهااگرهر تایپ کاملی در آنبا فرمول های بدون سور آن تایپکاملاً تعیین شود. به بیان دیگر، برای هر a , b {\displaystyle a,b} در مدل هیولا و هر زیرمجموعهٔ A {\displaystyle A} از مدل هیولا، اگر q f t p ( a / A ) = q f t p ( b / A ) {\displaystyle qftp(a/A)=qftp(b/A)} آن گاه t p ( a / A ) = t p ( b / A ) {\displaystyle tp(a/A)=tp(b/A)} ؛ که منظور از q f t p ( a / A ) {\displaystyle qftp(a/A)} مجموعهٔ همهٔ فرمول های بدون سور با پارامتر در A {\displaystyle A} است که a {\displaystyle a} آن ها را برآورده می کند.
داشتن حذف سور، تنها در یک «زبان معقول» حائزِ اهمیت است. این زبان عموماً بهینه ترین زبانی است که ویژگی های جبری یک تئوری را بتواند بیان کند. اگر جز این بخواهد باشد، هر تئوری ای با اضافه کردن محمول برای هر فرمول دارای سور به زبان، دارای حذف سور می شود. به بیان واضح تر اگر برای هر فرمولِ ϕ ( x ¯ , y ¯ ) {\displaystyle \phi ({\bar {x}},{\bar {y}})} محمول p ϕ {\displaystyle p_{\phi }} را به زبان و جملهٔ ∀ x ¯ {\displaystyle \forall {\bar {x}}} را به تئوری بیفزاییم، به یک تئوری دارای حذف سور می رسیم.
ساختارِ به ظاهرسادهٔ ( N , + , . , 0 , 1 , < ) {\displaystyle (\mathbb {N} ,+,.,0,1,<)} سورها را حذف نمی کند.مسئلهٔ حذف سور برای این ساختار،هم ارزِ مسئلهٔ ناکامل بودن اصول پئانو برای حساب است که گودل آن را ثابت کرده است. نیز به بیان دیگر، این مسئله معادلمسئلهٔ وجود یک زیرمجموعهٔبازگشتی شمارش پذیر(آر. ای)از N {\displaystyle \mathbb {N} } است که بازگشتی نباشد. در واقع زیرمجموعه های بازگشتی ِ شمارش پذیرِ N {\displaystyle \mathbb {N} } دقیقاً آنهایند که با فرمولهای ∃ x ¯ p ( y , x ) {\displaystyle \exists {\bar {x}}p(y,x)} تعریف می شوند که در آن p {\displaystyle p} یک چندجمله ای در N {\displaystyle \mathbb {N} } باشد.
wiki: حذف سور