الشكل الطبيعي لسكوليم

في المنطق الرياضي ، تكون صيغة منطق الرتبة الأولى في شكل سكوليم الطبيعي إذا كانت في شكل برينكس الطبيعي مع محددات كمية عالمية من الرتبة الأولى فقط .

يمكن تحويل أي صيغة من الدرجة الأولى إلى الصيغة الطبيعية لسكوليم دون تغيير قابليتها للإرضاء، وذلك من خلال عملية تُسمى "سكوليميزيشن" (أو "سكوليميزيشن "). لا تكون الصيغة الناتجة بالضرورة مكافئة للصيغة الأصلية، ولكنها قابلة للإرضاء معها: أي أنها قابلة للإرضاء إذا وفقط إذا كانت الصيغة الأصلية قابلة للإرضاء. ^{[ 1 ]}

يُعد الاختزال إلى الشكل الطبيعي لسكوليم طريقة لإزالة الكميات الوجودية من عبارات المنطق الرسمي ، وغالبًا ما يتم تنفيذه كخطوة أولى في برنامج إثبات النظريات الآلي .

أبسط أشكال السكولمية هي للمتغيرات المُكمَّمة وجوديًا والتي لا تقع ضمن نطاق المُكمِّم الكلي. ويمكن استبدالها ببساطة عن طريق إنشاء ثوابت جديدة. على سبيل المثال،${\displaystyle \exists xP(x)}$قد يتم تغييرها إلى${\displaystyle P(c)}$، أين${\displaystyle c}$هو ثابت جديد (لا يظهر في أي مكان آخر في الصيغة).

وبشكل أعم، يتم إجراء عملية سكولمية عن طريق استبدال كل متغير كمي وجودي${\displaystyle y}$بمصطلح${\displaystyle f(x_{1},\ldots ,x_{n})}$رموز وظائفها${\displaystyle f}$جديد. متغيرات هذا الحد هي كما يلي. إذا كانت الصيغة في شكلها الطبيعي السابق ، فإن${\displaystyle x_{1},\ldots ,x_{n}}$هي المتغيرات التي يتم قياسها بشكل عالمي والتي تسبق مُحدداتها الكمية مُحددات تلك الخاصة بـ${\displaystyle y}$بشكل عام، هي المتغيرات التي يتم تحديدها كميًا بشكل شامل (نفترض أننا نتخلص من المحددات الوجودية بالترتيب، لذا فإن جميع المحددات الوجودية قبل${\displaystyle \exists y}$تمت إزالتها) وما شابه ذلك${\displaystyle \exists y}$يحدث ذلك في نطاق مُكمِّماتها. الوظيفة${\displaystyle f}$يُطلق على العنصر المُدخل في هذه العملية اسم دالة سكوليم (أو ثابت سكوليم إذا كان من رتبة صفرية ) ويُطلق على الحد اسم حد سكوليم .

على سبيل المثال، الصيغة${\displaystyle \forall x\exists y\forall zP(x,y,z)}$لا يكون في الصيغة الطبيعية لسكوليم لأنه يحتوي على المُكمِّم الوجودي${\displaystyle \exists y}$. سكولميزيشن يحل محل${\displaystyle y}$مع${\displaystyle f(x)}$، أين${\displaystyle f}$هو رمز دالة جديد، ويزيل التحديد الكمي على${\displaystyle y}$الصيغة الناتجة هي${\displaystyle \forall x\forall zP(x,f(x),z)}$مصطلح سكوليم${\displaystyle f(x)}$يتضمن${\displaystyle x}$لكن ليس${\displaystyle z}$لأن المحدد الكمي المراد إزالته${\displaystyle \exists y}$يندرج ضمن نطاق${\displaystyle \forall x}$لكن ليس في ذلك${\displaystyle \forall z}$بما أن هذه الصيغة مكتوبة بصيغة prenex العادية، فإن هذا يعادل القول بأنه في قائمة المحددات الكمية،${\displaystyle x}$يسبق${\displaystyle y}$بينما${\displaystyle z}$لا. الصيغة التي تم الحصول عليها من هذا التحويل تكون قابلة للتحقيق إذا وفقط إذا كانت الصيغة الأصلية قابلة للتحقيق.

تعتمد عملية سكولميز على تطبيق تكافؤ من الدرجة الثانية بالتزامن مع تعريف قابلية الإرضاء من الدرجة الأولى. يوفر هذا التكافؤ طريقةً لـ"نقل" مُكمِّم وجودي قبل مُكمِّم كلي.

${\displaystyle \forall x\exists yR(x,y)\iff \exists f\forall xR(x,f(x))}$

أين

${\displaystyle f(x)}$هي دالة تقوم بربط${\displaystyle x}$ل${\displaystyle y}$.

بشكل بديهي، الجملة "لكل${\displaystyle x}$يوجد${\displaystyle y}$بحيث${\displaystyle R(x,y)}$يتم تحويل " إلى الشكل المكافئ "توجد دالة${\displaystyle f}$رسم خرائط لكل${\displaystyle x}$إلى${\displaystyle y}$بحيث يكون لكل${\displaystyle x}$وهذا يعني أن${\displaystyle R(x,f(x))}$".

هذا التكافؤ مفيد لأن تعريف قابلية الإرضاء من الدرجة الأولى يُكمّم ضمنيًا وجوديًا على الدوال التي تفسر رموز الدوال. على وجه الخصوص، صيغة من الدرجة الأولى${\displaystyle \Phi }$تكون قابلة للتحقيق إذا وُجد نموذج${\displaystyle M}$وتقييم${\displaystyle \mu }$من المتغيرات الحرة في الصيغة التي تُقيّم الصيغة إلى قيمة صحيحة . يحتوي النموذج على تفسير جميع رموز الدوال؛ لذلك، فإن دوال سكوليم مُكمّمة وجوديًا ضمنيًا. في المثال أعلاه،${\displaystyle \forall xR(x,f(x))}$تكون قابلة للتحقيق إذا وفقط إذا كان هناك نموذج${\displaystyle M}$، والذي يتضمن تفسيراً لـ${\displaystyle f}$بحيث${\displaystyle \forall xR(x,f(x))}$يصح هذا لبعض تقييمات متغيراته الحرة (لا يوجد أي منها في هذه الحالة). ويمكن التعبير عن ذلك من الدرجة الثانية على النحو التالي:${\displaystyle \exists f\forall xR(x,f(x))}$وبناءً على التكافؤ المذكور أعلاه، فإن هذا يُعادل قابلية إرضاء${\displaystyle \forall x\exists yR(x,y)}$.

على المستوى الفوقي، إمكانية إرضاء الصيغة من الدرجة الأولى${\displaystyle \Phi }$قد تُكتب مع بعض التجاوزات الطفيفة في استخدام الرموز كما${\displaystyle \exists M\exists \mu (M,\mu \models \Phi )}$، أين${\displaystyle M}$هو نموذج،${\displaystyle \mu }$وهو تقييم للمتغيرات الحرة، و${\displaystyle \models }$هذا يعني أن${\displaystyle \Phi }$صحيح في${\displaystyle M}$تحت${\displaystyle \mu }$بما أن نماذج الرتبة الأولى تتضمن تفسير جميع رموز الدوال، فإن أي دالة سكوليم التي${\displaystyle \Phi }$يتم تحديد مفهوم "يحتوي" ضمنيًا كميًا وجوديًا بواسطة${\displaystyle \exists M}$ونتيجة لذلك، بعد استبدال المحددات الوجودية على المتغيرات بالمحددات الوجودية على الدوال في بداية الصيغة، لا يزال من الممكن التعامل مع الصيغة على أنها صيغة من الدرجة الأولى عن طريق إزالة هذه المحددات الوجودية. هذه هي الخطوة الأخيرة في معالجة${\displaystyle \exists f\forall xR(x,f(x))}$مثل${\displaystyle \forall xR(x,f(x))}$قد تكتمل لأن الدوال تُقاس وجوديًا ضمنيًا بواسطة${\displaystyle \exists M}$في تعريف قابلية الإرضاء من الدرجة الأولى.

يمكن إثبات صحة عملية سكولم في الصيغة النموذجية${\displaystyle F_{1}=\forall x_{1}\dots \forall x_{n}\exists yR(x_{1},\dots ,x_{n},y)}$كما يلي. يتم تحقيق هذه الصيغة بواسطة نموذج${\displaystyle M}$إذا وفقط إذا، لكل قيمة ممكنة لـ${\displaystyle x_{1},\dots ,x_{n}}$في نطاق النموذج، توجد قيمة لـ${\displaystyle y}$في مجال النموذج الذي يصنع${\displaystyle R(x_{1},\dots ,x_{n},y)}$صحيح. بحسب بديهية الاختيار ، توجد دالة${\displaystyle f}$بحيث${\displaystyle y=f(x_{1},\dots ,x_{n})}$ونتيجة لذلك، فإن الصيغة${\displaystyle F_{2}=\forall x_{1}\dots \forall x_{n}R(x_{1},\dots ,x_{n},f(x_{1},\dots ,x_{n}))}$قابلة للإرضاء، لأنها تحتوي على النموذج الذي تم الحصول عليه بإضافة تفسير${\displaystyle f}$ل${\displaystyle M}$وهذا يدل على أن${\displaystyle F_{1}}$لا يمكن تحقيقها إلا إذا${\displaystyle F_{2}}$وهو قابل للتنفيذ أيضاً. على العكس من ذلك، إذا${\displaystyle F_{2}}$إذا كان الشرط قابلاً للتحقيق، فإنه يوجد نموذج${\displaystyle M'}$وهذا يفي بالغرض؛ يتضمن هذا النموذج تفسيراً للدالة${\displaystyle f}$بحيث يكون لكل قيمة من${\displaystyle x_{1},\dots ,x_{n}}$الصيغة${\displaystyle R(x_{1},\dots ,x_{n},f(x_{1},\dots ,x_{n}))}$يثبت. ونتيجة لذلك،${\displaystyle F_{1}}$يتم تحقيق ذلك بواسطة نفس النموذج لأنه يمكن للمرء أن يختار، لكل قيمة من${\displaystyle x_{1},\ldots ,x_{n}}$، القيمة${\displaystyle y=f(x_{1},\dots ,x_{n})}$، أين${\displaystyle f}$يتم تقييمها وفقًا لـ${\displaystyle M'}$.

يُستخدم تحويل سكولم في إثبات النظريات آليًا . على سبيل المثال، في طريقة الجداول التحليلية ، عندما تظهر صيغة يكون مُكمِّمها الرئيسي وجوديًا، يمكن توليد الصيغة الناتجة عن إزالة هذا المُكمِّم باستخدام تحويل سكولم. على سبيل المثال، إذا${\displaystyle \exists x\Phi (x,y_{1},\ldots ,y_{n})}$يحدث ذلك في لوحة، حيث${\displaystyle x,y_{1},\ldots ,y_{n}}$المتغيرات الحرة لـ${\displaystyle \Phi (x,y_{1},\ldots ,y_{n})}$، ثم${\displaystyle \Phi (f(y_{1},\ldots ,y_{n}),y_{1},\ldots ,y_{n})}$يمكن إضافتها إلى نفس فرع الجدول. هذه الإضافة لا تُغير من إمكانية تحقيق الجدول: يمكن توسيع كل نموذج من الصيغة القديمة، بإضافة تفسير مناسب لـ${\displaystyle f}$، إلى نموذج للصيغة الجديدة.

يُعدّ هذا الشكل من عملية سكولمزية تحسينًا على سكولمزية "الكلاسيكية"، إذ لا تُوضع في حدّ سكولمز إلا المتغيرات الحرة في الصيغة. ويُعتبر هذا تحسينًا لأن دلالات الجداول قد تُدرج الصيغة ضمنيًا في نطاق بعض المتغيرات المُكمّمة عالميًا غير الموجودة في الصيغة نفسها؛ وهذه المتغيرات لا تُوضع في حدّ سكولمز، بينما تُوضع فيه وفقًا للتعريف الأصلي لسكولميزية. ومن التحسينات الأخرى التي يُمكن استخدامها تطبيق رمز دالة سكولمز نفسه على الصيغ المتطابقة باستثناء إعادة تسمية المتغيرات. ^{[ 2 ]}

يُستخدم هذا الأسلوب أيضاً في طريقة حل المسائل المنطقية من الدرجة الأولى ، حيث تُمثَّل الصيغ كمجموعات من البنود التي يُفترض أنها مُكمَّمة بشكل شامل. (للاطلاع على مثال، انظر مفارقة شارب الكحول ).

من النتائج المهمة في نظرية النماذج نظرية لوفنهايم-سكوليم ، والتي يمكن إثباتها من خلال تطبيق نظرية سكوليم والإغلاق تحت دوال سكوليم الناتجة. ^{[ 3 ]}

بشكل عام، إذا${\displaystyle T}$هي نظرية ولكل صيغة متغيرات حرة${\displaystyle x_{1},\dots ,x_{n},y}$يوجد رمز دالة من الرتبة n${\displaystyle F}$من المؤكد أن هذه دالة سكوليم لـ${\displaystyle y}$، ثم${\displaystyle T}$تُسمى نظرية سكوليم . ^{[ 4 ]}

كل نظرية سكولم نموذجية كاملة ، أي أن كل بنية فرعية لنموذج ما هي بنية فرعية أولية . وبالنظر إلى نموذج M لنظرية سكولم T ، فإن أصغر بنية فرعية من M تحتوي على مجموعة معينة A تُسمى غلاف سكولم لـ A. وغلاف سكولم لـ A هو نموذج أولي ذري فوق A.

تم تسمية الشكل الطبيعي لسكوليم على اسم عالم الرياضيات النرويجي الراحل ثورالف سكوليم .

• هيربرانديزيشن ، نقيض سكولميزيشن
• منطق الدالة المسندة

• "دالة سكوليم" ، موسوعة الرياضيات ، دار نشر EMS ، 2001 [1994]
• Sklemization على PlanetMath.org
• Skolemization by Hector Zenil, Wolfram Demonstrations Project .
• وايسشتاين، إريك دبليو. "SkolemizedForm" . عالم الرياضيات .