نظام هيلبرت

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

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

يُعرَّف نظام هيلبرت بأنه نظام استنتاجي يُولِّد نظريات من بديهيات وقواعد استدلال، [ 3 ] [ 4 ] [ 5 ] لا سيما إذا كانت قاعدة الاستدلال الوحيدة المفترضة هي قاعدة القياس المنطقي (modus ponens) . [ 6 ] [ 7 ] كل نظام هيلبرت هو نظام بديهي ، وهو مصطلح يستخدمه العديد من المؤلفين كمصطلح عام غير محدد للإشارة إلى أنظمة هيلبرت الخاصة بهم، [ 8 ] [ 9 ] [ 10 ] دون ذكر أي مصطلحات أكثر تحديدًا. في هذا السياق، تُقارن "أنظمة هيلبرت" بأنظمة الاستنتاج الطبيعي ، [ 3 ] التي لا تستخدم بديهيات، بل قواعد استدلال فقط.

بينما تُعرّف جميع المصادر التي تُشير إلى نظام إثبات منطقي "بديهي" هذا النظام ببساطة على أنه نظام إثبات منطقي ذو بديهيات، فإن المصادر التي تستخدم صيغًا مختلفة من مصطلح "نظام هيلبرت" تُعرّفه أحيانًا بطرق مختلفة، لن نتناولها في هذه المقالة. على سبيل المثال، يُعرّف ترويلسترا "نظام هيلبرت" بأنه نظام ذو بديهيات و→هـ{\displaystyle {\rightarrow }E}و∀أنا{\displaystyle {\forall }I}باعتبارها قواعد الاستدلال الوحيدة. [ 11 ] تُسمى مجموعة محددة من البديهيات أحيانًا "نظام هيلبرت"، [ 12 ] أو "حساب هيلبرت". [ 13 ] يُستخدم مصطلح "هيلبرت" أحيانًا للإشارة إلى نوع النظام البديهي الذي تُعطى بديهياته في شكل تخطيطي ، [ 2 ] كما في قسم "  الشكل التخطيطي" من المسألة 2 أدناه، ولكن تستخدم مصادر أخرى مصطلح "هيلبرت" ليشمل كلاً من الأنظمة ذات البديهيات التخطيطية والأنظمة ذات قاعدة الاستبدال، [ 14 ] كما هو الحال في هذه المقالة. يعود استخدام مصطلح "هيلبرت" والمصطلحات المشابهة لوصف أنظمة البرهان البديهية في المنطق إلى تأثير كتاب " مبادئ المنطق الرياضي" لهيلبرت وأكرمان ( 1928). [ 2 ]

تتخذ معظم أنظمة هيلبرت نهجًا مميزًا في كيفية موازنتها بين البديهيات المنطقية وقواعد الاستدلال . [ 1 ] [ 6 ] [ 15 ] [ 11 ] تتميز أنظمة هيلبرت باختيار عدد كبير من مخططات البديهيات المنطقية ومجموعة صغيرة من قواعد الاستدلال . أما أنظمة الاستدلال الطبيعي فتتخذ نهجًا معاكسًا، إذ تتضمن العديد من قواعد الاستدلال ولكن عددًا قليلًا جدًا من مخططات البديهيات أو لا تتضمنها على الإطلاق. [ 3 ] تحتوي أنظمة هيلبرت الأكثر شيوعًا على قاعدة استدلال واحدة فقط - وهي قاعدة القياس المنطقي ( modus ponens) لمنطق القضايا - أو قاعدتين - مع التعميم - للتعامل مع منطق المسندات أيضًا - بالإضافة إلى العديد من مخططات البديهيات اللانهائية. تتطلب أنظمة هيلبرت لمنطق الموجه الحقيقي ، والتي تُسمى أحيانًا أنظمة هيلبرت-لويس ، قاعدة الإلزام أيضًا . تستخدم بعض الأنظمة قائمة محدودة من الصيغ الملموسة كمسلمات بدلاً من مجموعة لا نهائية من الصيغ عبر مخططات المسلمات، وفي هذه الحالة تكون قاعدة الاستبدال الموحدة مطلوبة. [ 14 ]    

من السمات المميزة للعديد من صيغ أنظمة هيلبرت أن السياق لا يتغير في أي من قواعد الاستدلال الخاصة بها، بينما يحتوي كل من الاستدلال الطبيعي وحساب المتتاليات على بعض القواعد التي تغير السياق. [ 16 ] وبالتالي، إذا كان المرء مهتمًا فقط بإمكانية اشتقاق التكرارات المنطقية ، دون النظر إلى الأحكام الافتراضية، فيمكنه صياغة نظام هيلبرت بحيث تحتوي قواعد الاستدلال الخاصة به على أحكام ذات شكل بسيط نسبيًا. لا يمكن فعل الشيء نفسه مع نظامي الاستدلال الآخرين: نظرًا لتغير السياق في بعض قواعد الاستدلال الخاصة بهما، لا يمكن صياغتهما بحيث يمكن تجنب الأحكام الافتراضية - حتى لو أردنا استخدامهما فقط لإثبات إمكانية اشتقاق التكرارات المنطقية. 

الاستنتاجات الرسمية

تمثيل بياني لنظام الاستنتاج
تمثيل بياني لنظام الاستنتاج

في نظام هيلبرت، يُعرَّف الاستنتاج الرسمي (أو البرهان ) بأنه سلسلة منتهية من الصيغ، حيث تمثل كل صيغة إما بديهية أو تُستنتج من صيغ سابقة وفقًا لقاعدة استدلال. [ 17 ] تهدف هذه الاستنتاجات الرسمية إلى محاكاة البراهين المكتوبة باللغة الطبيعية، على الرغم من أنها أكثر تفصيلًا. [ 18 ]

يفترضΓ{\displaystyle \Gamma }هي مجموعة من الصيغ، تُعتبر بمثابة فرضيات . على سبيل المثال،Γ{\displaystyle \Gamma }قد تكون مجموعة من البديهيات لنظرية الزمر أو نظرية المجموعات . الترميزΓ⊢ϕ{\displaystyle \Gamma \vdash \phi }يعني ذلك وجود استنتاج ينتهي بـϕ{\displaystyle \phi }باستخدام البديهيات المنطقية وعناصرها فقط كمسلماتΓ{\displaystyle \Gamma }[ 19 ] وهكذا، بشكل غير رسمي ،Γ⊢ϕ{\displaystyle \Gamma \vdash \phi }هذا يعني أنϕ{\displaystyle \phi }يمكن إثبات ذلك بافتراض أن جميع الصيغ فيΓ{\displaystyle \Gamma }.

تتميز أنظمة هيلبرت باستخدام العديد من مخططات البديهيات المنطقية . مخطط البديهيات هو مجموعة لانهائية من البديهيات التي يتم الحصول عليها عن طريق استبدال جميع الصيغ ذات شكل معين في نمط محدد. [ 20 ] لا تقتصر مجموعة البديهيات المنطقية على تلك البديهيات المولدة من هذا النمط فحسب، بل تشمل أيضًا أي تعميم لإحدى تلك البديهيات. [ 21 ] يتم الحصول على تعميم الصيغة عن طريق إضافة صفر أو أكثر من المحددات الكمية الشاملة إلى بداية الصيغة؛ على سبيل المثال∀y(∀xPxy→Pتy){\displaystyle \forall y(\forall xPxy\to Pty)}هو تعميم لـ∀xPxy→Pتy{\displaystyle \forall xPxy\to Pty}.

المنطق الافتراضي

فيما يلي بعض أنظمة هيلبرت التي استُخدمت في منطق القضايا . أحدها، وهو الشكل  التخطيطي لـ P2 ، يُعتبر أيضًا نظام فريجه .

كتاب فريجه المختصر

استُخدمت البراهين البديهية في الرياضيات منذ كتاب "أصول الهندسة" لإقليدس ، وهو كتاب مدرسي يوناني قديم شهير ، حوالي عام 300 قبل الميلاد. لكن أول نظام برهان رسمي كامل معروف ، والذي يُصنَّف بالتالي كنظام هيلبرت، يعود إلى كتاب " Begriffsschrift " لغوتلوب فريجه عام 1879. [ 9 ] [ 22 ] استخدم نظام فريجه الاستلزام والنفي فقط كأدوات ربط، [ 23 ] وكان يتألف من ست بديهيات، [ 22 ] وهي: [ 24 ] [ 25 ]

  • الاقتراح الأول:أ⊃(ب⊃أ){\displaystyle a\supset (b\supset a)}
  • الاقتراح الثاني:(ج⊃(ب⊃أ))⊃((ج⊃ب)⊃(ج⊃أ)){\displaystyle (c\supset (b\supset a))\supset ((c\supset b)\supset (c\supset a))}
  • الاقتراح رقم 8:(د⊃(ب⊃أ))⊃(ب⊃(د⊃أ)){\displaystyle (d\supset (b\supset a))\supset (b\supset (d\supset a))}
  • الاقتراح رقم 28:(ب⊃أ)⊃(¬أ⊃¬ب){\displaystyle (b\supset a)\supset (\neg a\supset \neg b)}
  • الاقتراح رقم 31:¬¬أ⊃أ{\displaystyle \neg \neg a\supset a}
  • الاقتراح رقم 41:أ⊃¬¬أ{\displaystyle a\supset \neg \neg a}

استخدم فريجه هذه القواعد إلى جانب قاعدة القياس المنطقي وقاعدة الاستبدال (التي تم استخدامها ولكن لم يتم تحديدها بدقة) للوصول إلى صياغة بديهية كاملة ومتسقة لمنطق القضايا الكلاسيكي القائم على وظائف الصدق. [ 24 ]

صفحة 2 من كتاب لوكاسيفيتش

أظهر يان لوكاسيفيتش أنه في نظام فريجه، "البديهية الثالثة زائدة عن الحاجة لأنها يمكن اشتقاقها من البديهيتين السابقتين، ويمكن استبدال البديهيات الثلاث الأخيرة بجملة واحدةججشمالصشمالqجqص{\displaystyle CCNpNqCqp}[ 25 ] وهو ما يعني ، عند نقله من تدوين لوكاسيفيتش البولندي إلى التدوين الحديث ذي الصيغة الوسطية .(¬ص→¬q)→(q→ص){\displaystyle (\neg p\rightarrow \neg q)\rightarrow (q\rightarrow p)}وبالتالي، يُنسب إلى لوكاسيفيتش [ 22 ] هذا النظام المكون من ثلاثة بديهيات:

  • ص→(q→ص){\displaystyle p\to (q\to p)}
  • (ص→(q→ر))→((ص→q)→(ص→ر)){\displaystyle (p\to (q\to r))\to ((p\to q)\to (p\to r))}
  • (¬ص→¬q)→(q→ص){\displaystyle (\neg p\to \neg q)\to (q\to p)}

تمامًا مثل نظام فريجه، يستخدم هذا النظام قاعدة الاستبدال، ويستخدم قاعدة الاستدلال المنطقي (modus ponens) كقاعدة للاستدلال. [ 22 ] وقدّم ألونسو تشيرش النظام نفسه (مع قاعدة استبدال صريحة) ، [ 26 ] وأشار إليه باسم النظام P2 ، [ 26 ] [ 27 ] وساهم في نشره. [ 27 ]

الشكل التخطيطي لـ P 2

يمكن تجنب استخدام قاعدة الاستبدال من خلال تقديم البديهيات في شكل تخطيطي، واستخدامها لتوليد مجموعة لانهائية من البديهيات. وبالتالي، باستخدام الأحرف اليونانية لتمثيل المخططات (متغيرات ما وراء المنطق التي يمكن أن تمثل أي صيغ سليمة )، تُعطى البديهيات على النحو التالي: [ 9 ] [ 27 ]

  • φ→(ψ→φ){\displaystyle \varphi \to (\psi \to \varphi )}
  • (φ→(ψ→χ))→((φ→ψ)→(φ→χ)){\displaystyle (\varphi \to (\psi \to \chi ))\to ((\varphi \to \psi )\to (\varphi \to \chi ))}
  • (¬φ→¬ψ)→(ψ→φ){\displaystyle (\neg \varphi \to \neg \psi )\to (\psi \to \varphi )}

يُنسب الشكل التخطيطي لـ P2 إلى جون فون نيومان ، [ 22 ] ويُستخدم في قاعدة بيانات البراهين الرسمية "set.mm" في Metamath . [ 27 ] في الواقع، تُنسب فكرة استخدام مخططات البديهيات لاستبدال قاعدة الاستبدال إلى فون نيومان. [ 28 ] كما نُسب الشكل التخطيطي لـ P2 إلى هيلبرت ، وسُمّيح{\displaystyle {\mathcal {H}}}في هذا السياق. [ 29 ]

تُسمى أنظمة المنطق الافتراضي التي تكون قواعد استدلالها تخطيطية أيضًا بأنظمة فريجه ؛ وكما أشار المؤلفون الذين عرّفوا مصطلح "نظام فريجه" في الأصل [ 30 ] ، فإن هذا يستثني في الواقع نظام فريجه نفسه، المذكور أعلاه، لأنه كان يحتوي على بديهيات بدلاً من مخططات بديهية. [ 28 ]

مثال على البرهان في الصفحة 2

كمثال على ذلك، برهان علىأ→أ{\displaystyle A\to A}يُعطى الجزء الثاني أدناه. أولاً، تُعطى البديهيات أسماءً:

(أ1)(ص→(q→ص)){\displaystyle (p\to (q\to p))}
(A2)((ص→(q→ر))→((ص→q)→(ص→ر))){\displaystyle ((p\to (q\to r))\to ((p\to q)\to (p\to r)))}
(A3)((¬ص→¬q)→(q→ص)){\displaystyle ((\neg p\to \neg q)\to (q\to p))}

والدليل على ذلك هو كالتالي:

  1. أ→((ب→أ)→أ){\displaystyle A\to ((B\to A)\to A)}   (مثال على (A1))
  2. (أ→((ب→أ)→أ))→((أ→(ب→أ))→(أ→أ)){\displaystyle (A\to ((B\to A)\to A))\to ((A\to (B\to A))\to (A\to A))}   (مثال على (A2))
  3. (أ→(ب→أ))→(أ→أ){\displaystyle (A\to (B\to A))\to (A\to A)}   (من (1) و (2) عن طريق الاستدلال المنطقي )
  4. أ→(ب→أ){\displaystyle A\to (B\to A)}   (مثال على (A1))
  5. أ→أ{\displaystyle A\to A}   (من (4) و (3) عن طريق الاستدلال المنطقي)

منطق المسند (نظام مثال)

يوجد عدد لا محدود من البديهيات لمنطق المسندات، إذ يتيح أي منطق حرية اختيار البديهيات والقواعد التي تميزه. نصف هنا نظام هيلبرت بتسعة بديهيات وقاعدة واحدة فقط هي قاعدة القياس المنطقي (modus ponens)، والذي نسميه بديهية القاعدة الواحدة، وهو يصف منطق المعادلات الكلاسيكي. نتعامل مع لغة بسيطة لهذا المنطق، حيث تستخدم الصيغ الروابط المنطقية فقط.¬{\displaystyle \lnot }و→{\displaystyle \to }والمحدد الكمي فقط∀{\displaystyle \forall }سنوضح لاحقًا كيف يمكن توسيع النظام ليشمل روابط منطقية إضافية، مثل∧{\displaystyle \land }و∨{\displaystyle \lor }، دون توسيع فئة الصيغ القابلة للاستنتاج.

تسمح المخططات المنطقية الأربعة الأولى (بالإضافة إلى قاعدة الاستدلال المنطقي) بالتلاعب بالروابط المنطقية.

P1.ϕ→ϕ{\displaystyle \phi \to \phi }
P2.ϕ→(ψ→ϕ){\displaystyle \phi \to \left(\psi \to \phi \right)}
P3.(ϕ→(ψ→ξ))→((ϕ→ψ)→(ϕ→ξ)){\displaystyle \left(\phi \to \left(\psi \rightarrow \xi \right)\right)\to \left(\left(\phi \to \psi \right)\to \left(\phi \to \xi \right)\right)}
ص4.(¬ϕ→¬ψ)→(ψ→ϕ){\displaystyle \left(\lnot \phi \to \lnot \psi \right)\to \left(\psi \to \phi \right)}

البديهية P1 زائدة عن الحاجة، إذ أنها تتبع من P3 وP2 وقاعدة الاستدلال (انظر البرهان ). تصف هذه البديهيات منطق القضايا الكلاسيكي ؛ وبدون البديهية P4 نحصل على منطق الاستلزام الإيجابي . يتحقق المنطق الأدنى إما بإضافة البديهية P4m بدلاً منها، أو بتعريف¬ϕ{\displaystyle \lnot \phi }مثلϕ→⊥{\displaystyle \phi \to \bot }.

P4m.(ϕ→ψ)→((ϕ→¬ψ)→¬ϕ){\displaystyle \left(\phi \to \psi \right)\to \left(\left(\phi \to \lnot \psi \right)\to \lnot \phi \right)}

يتحقق المنطق الحدسي بإضافة البديهيتين P4i وP5i إلى المنطق الاستلزامي الإيجابي، أو بإضافة البديهية P5i إلى المنطق الأدنى. كلتا البديهيتين P4i وP5i هما نظريتان من نظريات المنطق الافتراضي الكلاسيكي.

P4i.(ϕ→¬ϕ)→¬ϕ{\displaystyle \left(\phi \to \lnot \phi \right)\to \lnot \phi }
P5i.¬ϕ→(ϕ→ψ){\displaystyle \lnot \phi \to \left(\phi \to \psi \right)}

لاحظ أن هذه مخططات بديهية، تمثل عددًا لا نهائيًا من الحالات المحددة للبديهيات. على سبيل المثال، قد يمثل P1 حالة بديهية معينة.ص→ص{\displaystyle p\to p}أو قد يمثل(ص→q)→(ص→q){\displaystyle \left(p\to q\right)\to \left(p\to q\right)}: الϕ{\displaystyle \phi }هو مكان يمكن وضع أي صيغة فيه. يُطلق على المتغير الذي يتراوح بين الصيغ اسم "المتغير التخطيطي".

باستخدام قاعدة ثانية للاستبدال الموحد ، يمكننا تحويل كل مخطط من مخططات البديهيات هذه إلى بديهية واحدة، باستبدال كل متغير مخطط بمتغير افتراضي غير مذكور في أي بديهية، لنحصل على ما نسميه البديهية الاستبدالية. كلا الصياغتين الرسميتين تحتويان على متغيرات، ولكن بينما تحتوي البديهية ذات القاعدة الواحدة على متغيرات مخططة خارجة عن لغة المنطق، تستخدم البديهية الاستبدالية متغيرات افتراضية تؤدي نفس الوظيفة من خلال التعبير عن فكرة متغير يمتد على الصيغ باستخدام قاعدة تستخدم الاستبدال.

الولايات المتحدة. دعϕ(ص){\displaystyle \phi (p)}أن تكون صيغة تحتوي على حالة واحدة أو أكثر من متغير الاقتراحص{\displaystyle p}ودعψ{\displaystyle \psi }لنفترض صيغة أخرى. ثم منϕ(ص){\displaystyle \phi (p)}، استدلالϕ(ψ){\displaystyle \phi (\psi )}.

توفر المخططات المنطقية الثلاثة التالية طرقًا لإضافة ومعالجة وإزالة المحددات الكمية الشاملة.

س5.∀x(ϕ)→ϕ[x:=ت]{\displaystyle \forall x\left(\phi \right)\to \phi [x:=t]}حيث يمكن استبدال t بـ x فيϕ{\displaystyle \,\!\phi }
س6.∀x(ϕ→ψ)→(∀x(ϕ)→∀x(ψ)){\displaystyle \forall x\left(\phi \to \psi \right)\to \left(\forall x\left(\phi \right)\to \forall x\left(\psi \right)\right)}
س7.ϕ→∀x(ϕ){\displaystyle \phi \to \forall x\left(\phi \right)}حيث x ليس حراً فيϕ{\displaystyle \phi }.

تُوسّع هذه القواعد الثلاث الإضافية النظامَ الافتراضي ليشمل منطقَ المسند الكلاسيكي . وبالمثل، تُوسّع هذه القواعد الثلاث نظامَ منطق القضايا الحدسي (مع القواعد P1-3 وP4i وP5i) ليشمل منطق المسند الحدسي .

غالباً ما يتم إعطاء التحديد الكمي الشامل بديهية بديلة باستخدام قاعدة تعميم إضافية، وفي هذه الحالة تكون القاعدتان Q6 و Q7 زائدتين عن الحاجة.

  • التعميم : إذاΓ⊢ϕ{\displaystyle \Gamma \vdash \phi }ولا يظهر x بشكل حر في أي صيغة من صيغΓ{\displaystyle \Gamma }ثمΓ⊢∀xϕ{\displaystyle \Gamma \vdash \forall x\phi }.

تتطلب مخططات البديهيات النهائية العمل مع الصيغ التي تتضمن رمز المساواة.

I8.x=x{\displaystyle x=x}لكل متغير x .
I9.(x=y)→(ϕ[z:=x]→ϕ[z:=y]){\displaystyle \left(x=y\right)\to \left(\phi [z:=x]\to \phi [z:=y]\right)}

التوسعات المحافظة

من الشائع تضمين بديهيات عاملي الاستلزام والنفي فقط في نظام هيلبرت لتحقيق الاكتمال الوظيفي . وبناءً على هذه البديهيات، يُمكن صياغة امتدادات محافظة لنظرية الاستنتاج تسمح باستخدام روابط منطقية إضافية. تُسمى هذه الامتدادات محافظة لأنه إذا أُعيدت كتابة صيغة φ تتضمن روابط جديدة كصيغة مكافئة منطقيًا θ تتضمن فقط النفي والاستلزام والتكميم الكلي، فإن φ قابلة للاستنتاج في النظام الموسع إذا وفقط إذا كانت θ قابلة للاستنتاج في النظام الأصلي. وعند اكتمال التوسيع، يُصبح نظام هيلبرت أقرب إلى نظام الاستنتاج الطبيعي .

التحديد الكمي الوجودي

  • مقدمة
∀x(ϕ→∃y(ϕ[x:=y])){\displaystyle \forall x(\phi \to \exists y(\phi [x:=y]))}
  • الاستبعاد
∀x(ϕ→ψ)→(∃x(ϕ)→ψ){\displaystyle \forall x(\phi \to \psi )\to (\exists x(\phi )\to \psi )}أينx{\displaystyle x}ليس متغيرًا حرًا لـψ{\displaystyle \psi }.

الاقتران والانفصال

  • إدخال حروف العطف وحذفها
مقدمة:α→(β→α∧β){\displaystyle \alpha \to (\beta \to \alpha \land \beta )}
الإقصاء المتبقي:α∧β→α{\displaystyle \alpha \wedge \beta \to \alpha }
حق الاستبعاد:α∧β→β{\displaystyle \alpha \wedge \beta \to \beta }
  • إدخال وإلغاء الفصل
مقدمة من اليسار:α→α∨β{\displaystyle \alpha \to \alpha \vee \beta }
مقدمة على اليمين:β→α∨β{\displaystyle \beta \to \alpha \vee \beta }
الاستبعاد:(α→γ)→((β→γ)→α∨β→γ){\displaystyle (\alpha \to \gamma )\to ((\beta \to \gamma )\to \alpha \vee \beta \to \gamma )}

انظر أيضاً

ملحوظات

  1. 1 2 ماتي وروزا 1997:129
  2. 1 2 3 سميث، بيتر (21-02-2013). مقدمة في نظريات غودل . مطبعة جامعة كامبريدج. ص  10. ISBN 978-1-107-02284-3.
  3. 1 2 3 ريستال، جريج (11-09-2002). مقدمة في المنطق البنيوي الفرعي . روتليدج. ص 73-74 . ISBN  978-1-135-11131-1.
  4. ↑ غايفمان، حاييم (2002). "نظام استنتاجي من نوع هيلبرت للمنطق الجملي، والكمال، والتراص" (ملف PDF) . جامعة كولومبيا . تاريخ الاسترجاع: 19 أغسطس 2024 .
  5. ↑ بنثام، يوهان فان؛ غوبتا، أميتابها؛ باريك، روهيت (2011-04-02). البرهان، والحساب، والفاعلية: المنطق على مفترق الطرق . سبرينغر ساينس آند بيزنس ميديا. ص 41. ISBN  978-94-007-0080-2.
  6. 1 2 بيكون، أندرو (29-09-2023). مقدمة فلسفية في منطق الرتبة العليا . تايلور وفرانسيس. ص 424. ISBN  978-1-000-92575-3.
  7. ^ إيجك ، جان فان (26/02/1991). المنطق في الذكاء الاصطناعي: ورشة العمل الأوروبية JELIA '90، أمستردام، هولندا، 10-14 سبتمبر 1990. الإجراءات . سبرينغر العلوم والإعلام التجاري. ص. 113. ردمك  978-3-540-53686-4.
  8. ↑ هاك، سوزان (27 يوليو 1978). فلسفة المنطق . مطبعة جامعة كامبريدج. ص 19. ISBN  978-0-521-29329-7.
  9. 1 2 3 بوستوك، ديفيد (1997). المنطق الوسيط . أكسفورد : نيويورك: مطبعة كلارندون؛ مطبعة جامعة أكسفورد. الصفحات 4-5 ، 8-13 ، 18-19 ، 22، 27، 29، 191، 194. ISBN   978-0-19-875141-0.
  10. ↑ لوكاس، الابن (10-10-2018). رسالة في الزمان والمكان . روتليدج. ص 152. ISBN  978-0-429-68517-0.
  11. 1 2 ترولسترا، أ.س.؛ شفيتشتنبرغ، هـ. (2000). نظرية البرهان الأساسية . سلسلة كامبريدج في علوم الحاسوب النظرية ( الطبعة الثانية). كامبريدج: مطبعة جامعة كامبريدج. ص 51. doi : 10.1017/cbo9781139168717 . ISBN   978-0-521-77911-1.
  12. ↑ "مقدمة في المنطق - الفصل 4" . intrologic.stanford.edu . تاريخ الاسترجاع: 16 أغسطس 2024 .
  13. ↑ بوس، إس آر (998-07-09). دليل نظرية البرهان . إلسيفير. ص 552-553 . ISBN  978-0-08-053318-6.
  14. 1 2 أونو، هيرواكيرا (2019-08-02). نظرية البرهان والجبر في المنطق . سبرينغر. ص 5. ISBN  978-981-13-7997-0.
  15. ^ إيجك ، جان فان (26/02/1991). المنطق في الذكاء الاصطناعي: ورشة العمل الأوروبية JELIA '90، أمستردام، هولندا، 10-14 سبتمبر 1990. الإجراءات . سبرينغر العلوم والإعلام التجاري. ص. 113. ردمك  978-3-540-53686-4.
  16. ↑ غاباي، دوف م.؛ غوينتنر، فرانز (14 مارس 2013). دليل المنطق الفلسفي . سبرينغر ساينس آند بيزنس ميديا. ص 201. ISBN  978-94-017-0458-8.
  17. ↑ كوت، توشار ب. "أنظمة هيلبرت" (ملف PDF) . جامعة ستوني بروك . تم الاطلاع عليه بتاريخ 21 نوفمبر 2025 .
  18. ↑ ستوني بروك. "الفصل الثامن: أنظمة هيلبرت" (ملف PDF) . جامعة ستوني بروك . تم الاطلاع عليه بتاريخ 21 نوفمبر 2025 .
  19. ↑ كوت، توشار ب. "أنظمة هيلبرت" (ملف PDF) . جامعة ستوني بروك . تم الاطلاع عليه بتاريخ 21 نوفمبر 2025 .
  20. ↑ غورتزل، بن. "الاستدلال في منطق الرتبة الأولى" (ملف PDF) . Goertzel.org . تم الاطلاع عليه بتاريخ 21 نوفمبر 2025 .
  21. ↑ كوت، توشار ب. "أنظمة هيلبرت" (ملف PDF) . جامعة ستوني بروك . تم الاطلاع عليه بتاريخ 21 نوفمبر 2025 .
  22. 1 2 3 4 5 سموليان، ريموند م. (23-07-2014). دليل المبتدئين في المنطق الرياضي . شركة كورير. ص 102-103 . ISBN  978-0-486-49237-7.
  23. ↑ فرانكس، كورتيس (2023)، "المنطق الافتراضي" ، في زالتا، إدوارد ن.؛ نودلمان، أوري (محرران)، موسوعة ستانفورد للفلسفة ( طبعة خريف 2023)، مختبر أبحاث الميتافيزيقا، جامعة ستانفورد ، تاريخ الاسترجاع 22-03-2024 
  24. 1 2 مندلسون، ريتشارد ل. (10 يناير 2005). فلسفة غوتلوب فريجه . مطبعة جامعة كامبريدج. ص 185. ISBN  978-1-139-44403-3.
  25. 1 2 لوكاسيفيتش، يناير (1970). جان لوكاسيفيتش: أعمال مختارة . شمال هولندا. ص. 136. 
  26. 1 2 تشيرش، ألونسو (1996). مقدمة في المنطق الرياضي . مطبعة جامعة برينستون. ص 119. ISBN  978-0-691-02906-1.
  27. 1 2 3 4 "مستكشف البراهين - الصفحة الرئيسية - ميتا ماث" . us.metamath.org . تم الاطلاع عليه بتاريخ 2024-07-02 .
  28. 1 2 كوك، ستيفن أ.؛ ريكهاو، روبرت أ. (1979). "الكفاءة النسبية لأنظمة إثبات القضايا" . مجلة المنطق الرمزي . 44 (1): 39. doi : 10.2307/2273702 . ISSN 0022-4812 . JSTOR 2273702 .  
  29. ↑ واليكي، ميخال (2017). مقدمة في المنطق الرياضي ( طبعة موسعة). نيوجيرسي: وورلد ساينتيفيك. ص 126. ISBN   978-981-4719-95-7.
  30. ↑ بودلاك، بافيل؛ بوس، صموئيل ر. (1995). "كيفية الكذب دون أن تُدان (بسهولة) وأطوال البراهين في حساب القضايا" . في باتشولسكي، ليزيك؛ تيورين، جيرزي (محرران). منطق علوم الحاسوب . سلسلة محاضرات في علوم الحاسوب. المجلد 933. برلين، هايدلبرغ: سبرينغر. ص 152. doi : 10.1007/BFb0022253 . ISBN   978-3-540-49404-1.

مراجع

  • كاري، هاسكل ب.؛ روبرت فيس (1958). المنطق التوافقي المجلد الأول. المجلد  1. أمستردام: نورث هولاند.
  • مونك، ج. دونالد (1976). المنطق الرياضي . نصوص الدراسات العليا في الرياضيات. برلين، نيويورك: سبرينغر-فيرلاغ . ISBN 978-0-387-90170-1.
  • روزا، إيمري؛ ماتي، أندراس (1997). Bevezetés لوجيكابا حديثة (باللغة الهنغارية). بودابست: أوزوريس كيادو.
  • تارسكي، ألفريد (1990). Bizonyítás és igazság (باللغة المجرية). بودابست: الجندول.إنها ترجمة مجرية لأوراق مختارة من تأليف ألفريد تارسكي حول النظرية الدلالية للحقيقة .
  • ديفيد هيلبرت (1927) "أسس الرياضيات"، ترجمة ستيفان باور-مينغلربيرغ وداغفين فوليسدال (ص 464-479  ) . في:
    • فان هيجينورت، جان (1967). من فريجه إلى غودل: كتاب مرجعي في المنطق الرياضي، 1879-1931 ( الطبعة الثالثة، 1976  ). كامبريدج، ماساتشوستس: مطبعة جامعة هارفارد . ISBN 0-674-32449-8.
    • يقدم هيلبرت في محاضرته لعام 1927، المستندة إلى محاضرة "الأسس" السابقة لعام 1925 (الصفحات  367 - 392)، بديهياته الـ 17 - بديهيات الاستلزام #1-4، وبديهيات حول & و V #5-10، وبديهيات النفي #11-12، وبديهية إبسيلون المنطقية #13، وبديهيات المساواة #14-15، وبديهيات العدد #16-17 - إلى جانب العناصر الضرورية الأخرى لنظرية "الإثبات" الشكلية الخاصة به - مثل بديهيات الاستقراء، وبديهيات الاستدعاء الذاتي، وما إلى ذلك؛ كما يقدم دفاعًا قويًا ضد الحدسية لـ LEJ Brouwer. انظر أيضًا تعليقات ودحض هيرمان ويل (1927) (ص  480 – 484)، وملحق بول بيرناي (1927) لمحاضرة هيلبرت (ص  485 – 489) ورد لويتزن إجبرتوس جان بروير (1927) (ص  490 – 495)
  • كلين، ستيفن كول (1952). مقدمة في ما وراء الرياضيات (الطبعة العاشرة مع تصحيحات 1971  ). أمستردام، نيويورك: شركة نورث هولاند للنشر. ISBN 0-7204-2103-9.{{cite book}}عدم توافق رقم ISBN / التاريخ ( مساعدة )
    • انظر على وجه الخصوص الفصل الرابع النظام الرسمي (الصفحات  69-85 ) حيث يقدم كلين الفصول الفرعية §16 الرموز الرسمية، §17 قواعد التكوين، §18 المتغيرات الحرة والمقيدة (بما في ذلك الاستبدال)، §19 قواعد التحويل (مثل modus ponens) - ومن هذه يقدم 21 "مسلمة" - 18 بديهية و3 علاقات "النتيجة المباشرة" مقسمة على النحو التالي: مسلمات حساب القضايا #1-8، مسلمات إضافية لحساب المسند #9-12، ومسلمات إضافية لنظرية الأعداد #13-21.