أنظمة الشحن

في مجال تعقيد البرهان ، يُعرف نظام فريجه بأنه نظام برهان افتراضي تكون براهينه عبارة عن متواليات من الصيغ المستمدة باستخدام مجموعة محدودة من قواعد الاستدلال السليمة والكاملة ضمنيًا . ^{[ 1 ]} سُميت أنظمة فريجه (المعروفة غالبًا باسم أنظمة هيلبرت في نظرية البرهان العامة) نسبةً إلى جوتلوب فريجه .

تم تعريف مصطلح "نظام فريج" لأول مرة ^{[ 2 ]} من قبل ستيفن كوك وروبرت ريكهاو، ^{[ 3 ] [ 4 ]} وكان الهدف منه هو استيعاب خصائص أنظمة إثبات القضايا الأكثر شيوعًا. ^{[ 2 ]}

قدم كوك وريكهاو ^{[ 3 ] [ 4 ]} أول ^{[ 2 ]} تعريف رسمي لنظام فريجه، والذي يكافئه التعريف أدناه، استنادًا إلى كرايتشيك ^{[ 1 ] .}

ليكن K مجموعةً منتهيةً كاملةً وظيفيًا من الروابط المنطقية، ولنعتبر الصيغ المنطقية المبنية من المتغيرات p₀ _، p₁ _، p₂ _، ... باستخدام روابط K. قاعدة فريجه هي قاعدة استدلال على الشكل التالي :

${\displaystyle r={\frac {B_{1},\dots ,B_{n}}{B}},}$

حيث B₁ _, ... , Bₙ _, Bₙ هي صيغ. إذا كانت R مجموعة منتهية من قواعد فريجه، فإن F = ( K , R ) تُعرّف نظام اشتقاق على النحو التالي: إذا كانت X مجموعة من الصيغ، و A صيغة، فإن اشتقاق F للصيغة A من البديهيات X _هو سلسلة من الصيغ A₁ _{, ..., Aₘ بحيث يكون Aₘ} = Aₖ ، وكل Aₖ عنصر من X، أو مشتق من إحدى الصيغ Aᵢ، حيث i < k ، _عن طريق استبدال قاعدة من R. برهان F _{للصيغة A} هو اشتقاق F للصيغة A من المجموعة الفارغة من البديهيات ( X = ∅ ). يُسمى F نظام فريجه إذا    

• F صحيح: كل صيغة قابلة للإثبات باستخدام F هي تحصيل حاصل.
• F كاملة ضمنيًا: لكل صيغة A ومجموعة من الصيغ X ، إذا كانت X تستلزم A ، فإن هناك اشتقاق F لـ A من X.

طول البرهان (عدد الأسطر) في A1 _، ...، _Am هو m . حجم البرهان هو العدد الإجمالي للرموز.

يكون نظام الاشتقاق F كما هو مذكور أعلاه كاملاً من حيث الدحض، إذا كان لكل مجموعة غير متسقة من الصيغ X ، يوجد اشتقاق F لتناقض ثابت من X.

• لا يُعد حساب القضايا عند فريجه نظامًا من أنظمة فريجه، لأنه استخدم البديهيات بدلاً من مخططات البديهيات، على الرغم من أنه يمكن تعديله ليصبح نظامًا من أنظمة فريجه. ^{[ 4 ]}
• توجد العديد من الأمثلة على قواعد فريجه السليمة في صفحة حساب القضايا .
• لا يُعدّ الاستدلال نظامًا فريجيًا لأنه يعمل فقط على الجمل ، وليس على الصيغ المبنية بطريقة اعتباطية بواسطة مجموعة كاملة وظيفيًا من الروابط. علاوة على ذلك، فهو ليس كاملًا من الناحية الاستدلالية، أي لا يمكننا استنتاج${\displaystyle A\lor B}$من${\displaystyle A}$ومع ذلك، بإضافة قاعدة الإضعاف :${\displaystyle {\frac {A}{A\lor B}}}$يجعلها مكتملة ضمنيًا . كما أن القرار مكتمل من حيث الدحض.

• تنص نظرية ريكهاو لعام 1979 ^{[ 4 ]} على أن جميع أنظمة فريجه متكافئة من النوع p .
• الاستنتاج الطبيعي وحساب التفاضل والتكامل المتتالي (نظام جنتزن مع القطع) مكافئان أيضًا لأنظمة فريجه.
• توجد براهين فريجه ذات حجم متعدد الحدود لمبدأ الحمام . ^{[ 5 ]}
• تُعتبر أنظمة فريجه أنظمة قوية إلى حد ما. على عكس الاستدلال، على سبيل المثال، لا توجد حدود دنيا فائقة الخطية معروفة لعدد الأسطر في براهين فريجه، وأفضل الحدود الدنيا المعروفة لحجم البراهين هي حدود تربيعية.
• الحد الأدنى لعدد الجولات في لعبة المُثبت والمُنافس اللازمة لإثبات التكرار المنطقي${\displaystyle \phi }$يتناسب مع لوغاريتم الحد الأدنى لعدد الخطوات في برهان فريجه لـ${\displaystyle \phi }$.

• 
  نقاط قوة الإثبات للأنظمة المختلفة.

عرّف كوك وريكهاو أيضًا امتدادًا لنظام فريجه، يُسمى فريجه الموسّع ، ^{[ 4 ]} والذي يأخذ نظام فريجه F ويضيف إليه قاعدة اشتقاق إضافية تسمح باشتقاق صيغة${\displaystyle p\leftrightarrow D}$، أين${\displaystyle \leftrightarrow }$يختصر تعريفه بلغة F المحددة والذرة${\displaystyle p}$لا يظهر في الصيغ المشتقة سابقًا بما في ذلك البديهيات وفي الصيغة${\displaystyle D}$.

يهدف قانون الاشتقاق الجديد إلى إدخال "أسماء" أو اختصارات للصيغ القانونية المختلفة. وهو يسمح بتفسير البراهين في فريجه الموسع كبراهين فريجه تعمل باستخدام الدوائر بدلاً من الصيغ.

تسمح مراسلات كوك بتفسير نظرية فريجه الموسعة على أنها مكافئ غير منتظم لنظرية كوك PV ونظرية بوس${\displaystyle S_{2}^{1}}$صياغة الاستدلال الممكن (في وقت متعدد الحدود).