إثبات رسمي

📅 آخر تحديث: ٢٣ يوليو ٢٠٢٦
✍️ نُشر في: ٢٣ يوليو ٢٠٢٦
الموسوعة الحرة

في المنطق والرياضيات ، يُعرف البرهان الرسمي أو الاستدلال الرسمي بأنه سلسلة منتهية من الجمل (تُعرف بالصيغ السليمة عند ربطها باللغة الرسمية )، كل جملة منها إما بديهية ، أو فرضية، أو نتيجة منطقية للجمل السابقة في السلسلة، وفقًا لقاعدة الاستدلال . ويختلف البرهان الرسمي عن الحجة اللغوية الطبيعية في كونه دقيقًا، لا لبس فيه، وقابلًا للتحقق الآلي. [ 1 ] إذا كانت مجموعة الفرضيات فارغة، تُسمى الجملة الأخيرة في البرهان الرسمي نظرية النظام الرسمي . يُعد مفهوم النظرية فعالًا بشكل عام، ولكن قد لا توجد طريقة موثوقة لإيجاد برهان لجملة معينة أو لتحديد عدم وجود برهان لها. تُعد مفاهيم برهان فيتش ، وحساب المتتاليات ، والاستدلال الطبيعي تعميمات لمفهوم البرهان. [ 2 ] [ 3 ]

تُعدّ النظرية نتيجةً نحويةً لجميع الصيغ الصحيحة التي تسبقها في البرهان. ولكي تُعتبر الصيغة الصحيحة جزءًا من البرهان، يجب أن تكون ناتجةً عن تطبيق قاعدة من قواعد الاستدلال ( لنظام صوري ما) على الصيغ الصحيحة السابقة في تسلسل البرهان.

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

خلفية

اللغة الرسمية

اللغة الرسمية هي مجموعة من المتتاليات المحدودة من الرموز . يمكن تعريف هذه اللغة دون الرجوع إلى أي معانٍ لأي من تعابيرها؛ إذ يمكن أن توجد قبل إسناد أي تفسير لها ، أي قبل أن يكون لها أي معنى. تُعبَّر البراهين الرسمية في بعض اللغات الرسمية.

القواعد الرسمية

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

الأنظمة الرسمية

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

التفسيرات

تفسير النظام الصوري هو إسناد معانٍ للرموز وقيم الصواب لجمل النظام الصوري. يُطلق على دراسة التفسيرات اسم الدلالات الصورية . ويُعدّ إعطاء تفسير مرادفًا لبناء نموذج .

انظر أيضاً

مراجع

  1. ↑ كاسيوس، يانيس (20 فبراير 2009). "الإثبات الرسمي" (ملف PDF) . cs.utoronto.ca . تاريخ الاسترجاع: 12 ديسمبر 2019 .
  2. ↑ قاموس كامبريدج للفلسفة، الاستنتاج
  3. ↑ باروايز، جون؛ إتشيمندي، جون إتشيمندي (1999). اللغة، البرهان والمنطق (الطبعة الأولى ). دار نشر سفن بريدجز ومركز دراسات اللغات والأدب. 
  4. ↑ هاريسون، جون (ديسمبر 2008). "الإثبات الرسمي - النظرية والتطبيق" (ملف PDF) . ams.org . تم الاطلاع عليه بتاريخ 12 ديسمبر 2019 .