حساب القضايا الاستلزامي

في المنطق الرياضي ، يُعدّ حساب القضايا الاستلزامي نسخةً من حساب القضايا الكلاسيكي تستخدم رابطًا واحدًا فقط ، يُسمى الاستلزام أو الشرطي . في الصيغ ، يُشار إلى هذه العملية الثنائية بـ "يستلزم"، "إذا ...، فإن ..."، "→"، "${\displaystyle \rightarrow }$"، إلخ..

الاستلزام وحده ليس كاملاً وظيفياً كعامل منطقي لأنه لا يمكن تكوين جميع دوال الحقيقة الأخرى ذات القيمتين منه.

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

مع ذلك، إذا أضفنا رابطًا صفريًا ⊥ للدلالة على الكذب، فيمكننا تعريف جميع دوال الصدق الأخرى. تُسمى الصيغ التي تُكتب على مجموعة الروابط الناتجة {→, ⊥} بالصيغ f-الاستلزامية . ^{[ 1 ]} إذا كانت P و Q قضيتين، فإن:

• ¬ P يكافئ P → ⊥​
• P ∧ Q يكافئ ( P → ( Q → ⊥)) → ⊥
• P ∨ Q يكافئ ( P → Q ) → Q
• P ↔ Q يكافئ (( P → Q ) → (( Q → P ) → ⊥)) → ⊥

بما أن العوامل المذكورة أعلاه معروفة بأنها كاملة وظيفيًا، فإنه يترتب على ذلك أنه يمكن التعبير عن أي دالة حقيقة من حيث → و ⊥.

تعتبر العبارات التالية بمثابة تحصيل حاصل (غير قابلة للاختزال وصحيحة بديهياً، بحكم التعريف).

• مخطط اكسيوم 1 هو P → ( Q → P ).
• مخطط البديهية 2 هو ( P → ( Q → R )) → (( P → Q ) → ( P → R )).
• المخطط البديهي 3 ( قانون بيرس ) هو (( P → Q ) → P ) → P .
• القاعدة الوحيدة غير الصفرية للاستدلال ( modus ponens ) هي: من P و P → Q استنتج Q.

في كل حالة، يمكن استبدال P و Q و R بأي صيغ تحتوي فقط على "→" كرابط. إذا${\displaystyle \Gamma }$إذا كانت مجموعة من الصيغ و A صيغة، فإن${\displaystyle \Gamma \vdash A}$هذا يعني أن A قابلة للاشتقاق باستخدام البديهيات والقواعد المذكورة أعلاه والصيغ من${\displaystyle \Gamma }$كفرضيات إضافية.

وجد لوكاسيفيتش (1948) نظامًا بديهيًا لحساب الاستلزام يستبدل المخططات 1-3 المذكورة أعلاه بمخطط واحد.

• (( P → Q ) → R ) → (( R → P ) → ( S → P )).

كما جادل بأنه لا يوجد نظام بديهيات أقصر. ^{[ 2 ]}

بما أن جميع بديهيات وقواعد حساب التفاضل والتكامل هي مخططات، فإن الاشتقاق مغلق تحت التعويض :

لو${\displaystyle \Gamma \vdash A,}$ثم${\displaystyle \sigma (\Gamma )\vdash \sigma (A),}$

حيث σ هو أي استبدال (للصيغ التي تستخدم الاستلزام فقط).

كما أن حساب القضايا الاستلزامي يحقق نظرية الاستنتاج :

لو${\displaystyle \Gamma ,A\vdash B}$، ثم${\displaystyle \Gamma \vdash A\to B.}$

كما هو موضح في مقالة نظرية الاستنتاج ، ينطبق هذا على أي امتداد بديهي للنظام يحتوي على مخططات البديهيات 1 و 2 أعلاه و modus ponens.

إن حساب القضايا الاستلزامي كامل دلاليًا بالنسبة للدلالات الثنائية المعتادة لمنطق القضايا الكلاسيكي. أي، إذا كانت Γ مجموعة من الصيغ الاستلزامية، و A صيغة استلزامية مستنتجة من Γ، فإن${\displaystyle \Gamma \vdash A}$.

دليل

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

يشبه البرهان برهان اكتمال منطق القضايا الكامل، ولكنه يستخدم أيضًا الفكرة التالية للتغلب على عدم اكتمال الاستلزام الوظيفي. إذا كانت A و F صيغتين، فإن A → F مكافئة لـ ( ¬A* ) ∨ F ، حيث A* هي نتيجة استبدال جميع أو بعض أو لا شيء من حالات F في A بالخطأ. وبالمثل، فإن ( A → F ) → F مكافئة لـ A* ∨ F. لذا، في ظل شروط معينة، يمكن استخدامهما كبديلين للقول بأن A* خاطئة أو A * صحيحة على التوالي.

نلاحظ أولاً بعض الحقائق الأساسية حول قابلية الاشتقاق:

${\displaystyle A\to B,B\to C\vdash A\to C}$

1

في الواقع، يمكننا استنتاج A → ( B → C ) باستخدام البديهية 1، ثم استنتاج A → C عن طريق القياس المنطقي (مرتين) من البديهية 2.

${\displaystyle A\to B\vdash (B\to C)\to (A\to C)}$

2

وهذا يتبع من ( 1 ) بواسطة نظرية الاستنتاج.

${\displaystyle A\to C,(A\to B)\to C\vdash C}$

3

إذا افترضنا كذلك أن C → B ، فيمكننا استنتاج A → B باستخدام ( 1 )، ثم نستنتج C عن طريق القياس المنطقي. وهذا يُظهر${\displaystyle A\to C,(A\to B)\to C,C\to B\vdash C}$، وتعطي نظرية الاستنتاج${\displaystyle A\to C,(A\to B)\to C\vdash (C\to B)\to C}$نطبق المعادلة 3 للحصول على ( 3 ).

لتكن F صيغة ثابتة اختيارية. لأي صيغة A ، نُعرّف A₀ ⁼ ( A → F ) و A₁ = (( ^A → F ) → F ). لنأخذ في الاعتبار فقط الصيغ في المتغيرات الافتراضية p₁ _, ..., pₙ _. ندّعي أنه لكل صيغة A في هذه المتغيرات ولكل قيمة منطقية e ،

${\displaystyle p_{1}^{e(p_{1})},\dots ,p_{n}^{e(p_{n})}\vdash A^{e(A)}.}$

4

نُثبت ( 4 ) بالاستقراء على A. الحالة الأساسية A = πi بديهية. ليكن A = ( _B → C ) . نميز ثلاث حالات:

1. إذا كان e ( C ) = 1، فإن e ( A ) = 1 أيضًا. لدينا

   ${\displaystyle (C\to F)\to F\vdash ((B\to C)\to F)\to F}$

   بتطبيق ( 2 ) مرتين على البديهية C → ( B → C ). بما أننا استنتجنا ( C → F ) → F بفرضية الاستقراء، يمكننا استنتاج (( B → C ) → F ) → F.

2. e ( B ) = 0. ثم e ( A ) = 1. بتطبيق نظرية الاستنتاج على ( 3 ) نحصل على

   ${\displaystyle B\to F\vdash ((B\to C)\to F)\to F.}$

   بما أننا استنتجنا B → F من خلال فرضية الاستقراء، فيمكننا أن نستنتج (( B → C ) → F ) → F .

3. إذا كانت قيمة e ( B ) تساوي 1 وقيمة e ( C ) تساوي 0، فإن قيمة e ( A ) تساوي 0.

   ${\displaystyle {\begin{aligned}(B\to F)\to F,C\to F,B\to C&\vdash B\to F&&{\text{by (1)}}\\&\vdash F&&{\text{by modus ponens,}}\end{aligned}}}$

   هكذا${\displaystyle (B\to F)\to F,C\to F\vdash (B\to C)\to F}$باستخدام نظرية الاستنتاج. لقد استنتجنا ( B → F ) → F و C → F باستخدام فرضية الاستقراء، وبالتالي يمكننا استنتاج ( B → C ) → F. وهذا يُكمل برهان ( 4 ) .

لنفترض الآن أن F عبارة عن تحصيل حاصل في المتغيرات p1 _، ...، pn _. سنثبت بالاستقراء العكسي على k = n ، ...، 0 أنه لكل تعيين e ،

${\displaystyle p_{1}^{e(p_{1})},\dots ,p_{k}^{e(p_{k})}\vdash F.}$

5

تنتج الحالة الأساسية k = n من حالة خاصة من ( 4 ) باستخدام

${\displaystyle F^{e(F)}=F^{1}=((F\to F)\to F)}$

وحقيقة أن F → F هي نظرية بحسب نظرية الاستنتاج.

بافتراض صحة ( 5 ) لـ k + 1، سنبين صحتها لـ k . بتطبيق نظرية الاستنتاج على فرضية الاستقراء، نحصل على

${\displaystyle {\begin{aligned}p_{1}^{e(p_{1})},\dots ,p_{k}^{e(p_{k})}&\vdash (p_{k+1}\to F)\to F,\\p_{1}^{e(p_{1})},\dots ,p_{k}^{e(p_{k})}&\vdash ((p_{k+1}\to F)\to F)\to F,\end{aligned}}}$

عن طريق وضع e ( p _{k +1} ) = 0 أولاً ووضع e ( p _{k +1} ) = 1 ثانياً. ومن هذا نستنتج ( 5 ) باستخدام modus ponens.

عندما k = 0، نجد أن التكرار المنطقي F قابل للإثبات دون افتراضات. هذا ما كان المطلوب إثباته.

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

يُستخدم نظام بديهيات بيرنايز-تارسكي بشكل متكرر. وعلى وجه الخصوص، تستنتج ورقة لوكاسيفيتش بديهيات بيرنايز-تارسكي من بديهية لوكاسيفيتش الوحيدة كوسيلة لإظهار اكتمالها. وهي تختلف عن مخططات البديهيات المذكورة أعلاه باستبدال مخطط البديهيات 2، ( P → ( Q → R )) → (( P → Q ) → ( P → R ))، بـ

• مخطط اكسيوم 2': ( P → Q )→(( Q → R )→( P → R ))،

وهذا ما يسمى بالقياس المنطقي الافتراضي . وهذا يجعل اشتقاق نظرية الاستنتاج الميتافيزيقية أكثر صعوبة بعض الشيء، ولكنه لا يزال ممكناً.

نُبين أنه من P →( Q → R ) و P → Q يمكن استنتاج P → R. ويمكن استخدام هذه الحقيقة بدلاً من مخطط البديهية 2 للحصول على النظرية الفوقية.

1. P →( Q → R ) معطى
2. P → Q معطى
3. ( P → Q ) → (( Q → R ) → (( P → R )) ax 2'
4. ( س → ص )→( ف → ص ) mp 2,3
5. ( P → ( Q → R )) → ((( Q → R ) → ( P → R )) → ( P → ( P → R ))) ax 2'
6. (( Q → R )→( P → R ))→( P →( P → R )) mp 1,5
7. P →( P → R ) mp 4,6
8. ( P → ( P → R )) → ((( P → R ) → R ) → ( P → R )) ax 2'
9. (( P → R )→ R )→( P → R ) mp 7,8
10. ((( P → R )→ R )→( P → R ))→( P → R ) ax 3
11. P → R mp 9,10 qed

إن إمكانية الإرضاء في حساب القضايا الاستلزامي أمر تافه، لأن كل صيغة قابلة للإرضاء: ما عليك سوى تعيين جميع المتغيرات إلى صحيح.

إن قابلية التكذيب في حساب القضايا الاستدلالي هي NP-كاملة ، ^{[ 3 ]} مما يعني أن الصلاحية (التكرار) هي co-NP-كاملة .

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

مثال على عدم التكرار :

لنفترض أن [( A → B )→(( C → A )→ E )]→([ F →(( C → D )→ E )]→[( A → F )→( D → E )]) خاطئة.

ثم ( أ → ب )→(( ج → أ )→ هـ ) صحيح؛ و →(( ج → د )→ هـ ) صحيح؛ أ → و صحيح؛ د صحيح؛ و هـ خطأ.

بما أن العبارة D صحيحة، فإن العبارة C → D صحيحة أيضاً. لذا فإن صحة العبارة F → (( C → D )→ E ) تعادل صحة العبارة F → E.

وبما أن E خاطئة و F → E صحيحة، فإننا نستنتج أن F خاطئة.

بما أن A → F صحيح، فإن A خاطئ. وبالتالي فإن A → B صحيح و ( C → A ) → E صحيح.

C → A خطأ، لذا فإن C صحيح.

قيمة B لا تهم، لذلك يمكننا اختيارها بشكل تعسفي لتكون صحيحة.

باختصار، التقييم الذي يجعل B و C و D صحيحة و A و E و F خاطئة سيجعل [( A → B ) → (( C → A ) → E )] → ([ F → (( C → D ) → E )] → [( A → F ) → ( D → E )]) خاطئة. لذا فهي ليست تحصيل حاصل.

مثال على التكرار :

لنفترض أن (( A → B )→ C )→(( C → A )→( D → A )) خاطئة.

إذن ( أ → ب ) → ج صحيح؛ ج → أ صحيح؛ د صحيح؛ و أ خطأ.

بما أن العبارة أ خاطئة، فإن العبارة أ → ب صحيحة. إذن العبارة ج صحيحة. وبالتالي، يجب أن تكون العبارة أ صحيحة، وهذا يناقض كونها خاطئة.

وبالتالي، لا يوجد تقييم يجعل (( أ → ب )→ ج )→(( ج → أ )→( د → أ )) خاطئًا. وعليه، فهو تحصيل حاصل.

ماذا سيحدث إذا تمت إضافة مخطط بديهي آخر إلى المخططات المذكورة أعلاه؟ هناك حالتان: (1) أنه تحصيل حاصل؛ أو (2) أنه ليس تحصيل حاصل.

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

إذا لم يكن مخطط البديهيات الجديد تحصيل حاصل، فإن كل صيغة تصبح نظرية (مما يجعل مفهوم النظرية غير ذي جدوى في هذه الحالة). علاوة على ذلك، يوجد حد أعلى لطول برهان كل صيغة، لوجود طريقة مشتركة لإثباتها. على سبيل المثال، لنفترض أن مخطط البديهيات الجديد هو (( B → C ) → C ) → B. عندئذٍ، (( A → ( A → A )) → ( A → A )) → A هو مثال (أحد البديهيات الجديدة) وليس تحصيل حاصل. لكن [(( A → ( A → A )) → ( A → A )) → A ] → A هو تحصيل حاصل، وبالتالي نظرية بسبب البديهيات القديمة (باستخدام نتيجة الاكتمال المذكورة أعلاه). بتطبيق قاعدة القياس المنطقي، نحصل على أن A هي نظرية للنظام الموسع. عندئذٍ ، كل ما علينا فعله لإثبات أي صيغة هو استبدال A بالصيغة المطلوبة في جميع أجزاء برهان A. سيكون لهذا البرهان نفس عدد الخطوات التي يحتوي عليها برهان A.

تعتمد البديهيات المذكورة أعلاه بشكل أساسي على نظرية الاستنتاج للوصول إلى الاكتمال. إليك نظام بديهيات آخر يهدف مباشرةً إلى الاكتمال دون المرور بنظرية الاستنتاج.

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

• aa 1: ꞈ A → A
• aa 2: ( A → B )→ꞈ( A →( C → B ))
• aa 3: A →(( B → C )→ꞈ(( A → B )→ C ))
• aa 4: A →ꞈ( B → A )

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

لنفترض أي صيغة Φ قد تحتوي على A و B و C1 _و ... و _Cn وتنتهي بـ A كنتيجة نهائية. ثم نأخذ

• أأ 5: Φ ₋ →( Φ ₊ →ꞈ Φ )

كنموذج بديهي، حيث _Φ− هي نتيجة استبدال B بـ A في جميع عناصر Φ، و Φ ₊ هي نتيجة استبدال B بـ ( A → A ) في جميع عناصر Φ . هذا نموذج لنماذج البديهيات، إذ يتضمن مستويين من الاستبدال: في الأول، يتم استبدال Φ (مع بعض الاختلافات)؛ وفي الثاني، يمكن استبدال أي من المتغيرات (بما في ذلك A و B ) بصيغ اختيارية من حساب القضايا الاستلزامي. يتيح هذا النموذج إثبات التكرارات المنطقية التي تحتوي على أكثر من متغير واحد، وذلك بالنظر إلى حالة كون B خاطئة (Φ− ₎ وحالة كون B صحيحة (Φ ₊ ).

إذا كانت قيمة المتغير الذي يمثل النتيجة النهائية لصيغة ما صحيحة، فإن الصيغة بأكملها تكون صحيحة بغض النظر عن قيم المتغيرات الأخرى. وبالتالي، إذا _كانت A صحيحة، فإن Φ و Φ⁻ _و Φ⁺ و Φ⁻ _→ ( Φ⁺ → Φ ) كلها صحيحة. لذا، ودون الإخلال بعمومية الحل ، يمكننا افتراض أن A خاطئة. لاحظ أن Φ تُعتبر تحصيل حاصل إذا وفقط إذا كانت كل من _Φ⁻ و Φ⁺ تحصيل حاصل. ولكن بينما تحتوي Φ على n + 2 متغيرًا مختلفًا، فإن Φ⁻ _و Φ⁺ _{تحتويان على} n + 1. لذلك _، اختُزلت مسألة ما إذا كانت الصيغة تحصيل حاصل إلى مسألة ما إذا كانت بعض الصيغ التي تحتوي كل منها على متغير واحد تُعتبر تحصيل حاصل . لاحظ أيضًا أن Φ ₋ →( Φ ₊ → Φ ) هي تحصيل حاصل بغض النظر عما إذا كانت Φ خاطئة أم لا، لأنه إذا كانت Φ خاطئة، فإن Φ ₋ أو Φ ₊ ستكون خاطئة اعتمادًا على ما إذا كانت B خاطئة أم صحيحة.

أمثلة:

اشتقاق قانون بيرس

1. [(( P → P )→ P )→ P ]→([(( P →( P → P ))→ P )→ P ]→[(( P → Q )→ P )→ P ]) aa 5
2. P → P aa 1
3. ( P → P )→(( P → P )→((( P → P )→ P )→ P )) aa 3
4. ( ف → ف )→((( ف → ف )→ ف )→ ف ) mp 2,3
5. (( ف → ف )→ ف )→ ف mp 2,4
6. [(( P →( P → P ))→ P )→ P ]→[(( P → Q )→ P )→ P ] mp 5,1
7. P →( P → P ) aa 4
8. ( P → ( P → P )) → (( P → P ) → (( P → ( P → P )) → P ) → P )) aa 3
9. ( ف → ف )→((( ف →( ف → ف )))→ ف )→ ف ) mp 7,8
10. (( ف →( ف → ف ))→ ف )→ ف mp 2,9
11. (( P → Q )→ P )→ P mp 10,6 qed

اشتقاق البديهية الوحيدة لوكاسيفيتش

1. [(( P → Q )→ P )→(( P → P )→( S → P ))]→([(( P → Q )→( P → P ))→((( P → P )→ P )→( S → P ))]→[(( P → Q )→ R )→(( R → P )→( S → P ))]) aa 5
2. [(( P → P )→ P )→(( P → P )→( S → P ))]→([(( P →( P → P ))→ P )→(( P → P )→( S → P ))]→[(( P → Q )→ P )→(( P → P )→( S → P ))]) aa 5
3. P →( S → P ) aa 4
4. ( P → ( S → P )) → ( P → (( P → P ) → ( S → P ))) aa 2
5. ف →(( ف → ف )→( S → ف )) mp 3,4
6. P → P aa 1
7. ( P → P ) → (( P → (( P → P ) → ( S → P ))) → [(( P → P ) → P ) → (( P → P ) → ( S → P ))]) aa 3
8. ( ف →(( ف → ف )→( S → ف )))→[(( ف → ف )→ ف )→(( ف → ف )→( س → ف )))] mp 6,7
9. (( ف → ف )→ ف )→(( ف → ف )→( س → ف )) mp 5,8
10. [(( P →( P → P ))→ P )→(( P → P )→( S → P )]→[(( P → Q )→ P )→(( P → P )→( S → P ))] mp 9,2
11. P →( P → P ) aa 4
12. ( P → ( P → P )) → (( P → (( P → P ) → ( S → P )))) → [(( P → ( P → P )) → P ) → (( P → P ) → ( S → P ))]) aa 3
13. ( ف →(( ف → ف )→( ق → ف )))→[(( ف →( ف → ف )))→ ف )→(( ف → ف )→( س → ف )))] mp 11,12
14. (( ف →( ف → ف )))→ ف )→(( ف → ف )→( س → ف )) mp 5,13
15. (( ف → س )→ ف )→(( ف → ف )→( س → ف )) mp 14,10
16. [(( ف → س )→( ف → ف )))→((( ف → ف )→ ف )→( س → ف )))]→[(( ف → س )→ ر )→(( ر → ف )→( س → ف )))] mp 15,1
17. ( P → P ) → (( P → ( S → P )) → [(( P → P ) → P ) → ( S → P )]) aa 3
18. ( ف →( ق → ف )))→[(( ف → ف )→ ف )→( ق → ف )] mp 6,17
19. (( ف → ف )→ ف )→( S → ف ) mp 3,18
20. ((( P → P )→ P )→( S → P ))→[(( P → Q )→( P → P ))→((( P → P )→ P )→( S → P ))] aa 4
21. (( ف → س )→( ف → ف )))→((( ف → ف )→ ف )→( ق → ف )) mp 19,20
22. (( P → Q )→ R )→(( R → P )→( S → P )) mp 21,16 qed

يتطلب استخدام جدول الصواب للتحقق من بديهية لوكاسيفيتش الوحيدة النظر في 2⁴ ^حالة ، لاحتوائها على 4 متغيرات مختلفة. في هذا الاستدلال، تمكّنا من حصر النظر في 3 حالات فقط: R خاطئة و Q خاطئة، R خاطئة و Q صحيحة، و R صحيحة. مع ذلك، ولأننا نعمل ضمن النظام المنطقي الرسمي (بدلاً من خارجه، بشكل غير رسمي)، فقد تطلّبت كل حالة جهدًا أكبر بكثير.

• نظرية الاستنتاج
• قائمة الأنظمة المنطقية §  حساب القضايا الاستلزامي
• قانون بيرس
• حساب القضايا
• التكرار (المنطق)
• جدول الحقيقة
• التقييم (المنطقي)

• ميندلسون، إليوت (1997) مقدمة في المنطق الرياضي ، الطبعة الرابعة. لندن: تشابمان وهول.