انتقل إلى المحتوى
Topos Uranos
العربية

تناظرات الروابط

ملخص

يبرهن هذا الدرس على أن ترتيب الوسيطين لا يغيّر ما يُستنتج من النفي المشترك، ومن الفصل، ومن العطف، ومن الاستلزام المزدوج، ومن الفصل الحصري. فبالاختصارات المعتمدة في الدورة، ليست هذه التناظرات بديهية: فالنفي المشترك هو الرابط الأولي، ومسلّمات لوكاشيفيتش لا تتحدث إلا عن النفي والاستلزام، وقاعدة إبدال النفي المزدوج لا تفعل إلا أن تضيف نفيين متتاليين أو تحذفهما. ولذلك يرسي الدرس أولًا ثلاث أدوات. الأولى تقول إن التكافؤ الاستنتاجي يسلك سلوك المساواة. والثانية، التوطئة الأساسية، تترجم النفي المشترك إلى لغة المسلّمات: (φ↓ψ)(\varphi \downarrow \psi) تكافئ ¬(¬φ→ψ)\neg(\neg\varphi \rightarrow \psi)، بفضل قاعدة إبدال النفي المزدوج والنفي المزدوج. والثالثة، إبدال المتكافئات، التي لا تجعلها قاعدة إبدال النفي المزدوج زائدة، تتيح إبدال صيغة بأي صيغة أخرى تكافئها (لا إبدال θ\theta بـ¬¬θ\neg\neg\theta فحسب) تحت النفي، وفي طرفي الاستلزام، وفي طرفي النفي المشترك. وبها يُبرهن، بوصفها تكافؤات، على الصور البديلة للفصل والعطف، التي تتخذها كتب أخرى تعريفات، وعلى التناظرات الخمسة، في الاتجاهين وبالترتيب الذي تفرضه التعريفات: النفي المشترك أولًا، ومنه، على التوالي، البقية.

أهداف التعلم

  1. فكّ الاختصارات المعتمدة للحكم على ما إذا كانت عبارتان تدلّان على الصيغة نفسها أو على صيغتين مختلفتين يتطلب تكافؤهما استنتاجًا.
  2. البرهان على التوطئة الأساسية (φ↓ψ)⊣⊢¬(¬φ→ψ)(\varphi \downarrow \psi) \dashv\vdash \neg(\neg\varphi \rightarrow \psi) بقاعدة إبدال النفي المزدوج والنفي المزدوج، مع تحديد مواضع النفي المزدوج التي تخفيها الاختصارات.
  3. تطبيق إبدال المتكافئات لنقل تكافؤ إلى داخل نفي أو استلزام أو نفي مشترك، وتمييزه من قاعدة إبدال النفي المزدوج، التي لا تفعل إلا أن تبادل بين θ\theta و¬¬θ\neg\neg\theta، واستعمال التكافؤ الاستنتاجي بوصفه مساواة في تعاقبات من التكافؤات.
  4. البرهان على الصور البديلة للفصل والعطف وعلى التناظرات الخمسة في الاتجاهين، بربط نتائج سبق البرهان عليها.
  5. تعميم إبدال المتكافئات على أي صيغة بواسطة الاستقراء على تعقيد الصيغ.

ما يُستعمل وما يجب البرهان عليه

حدّد الدرس الخاص بـالأنظمة الاستنتاجية الصورية نظام لوكاشيفيتش: المسلّمات A1 وA2 وA3 وقاعدة الوضع. وأثبت فضلًا عن ذلك الانعكاسية (انعكاس: إذا كان φ∈Γ\varphi \in \Gamma، فإن Γ⊢φ\Gamma \vdash \varphi)، والرتابة (رتابة)، وقاعدة القطع (قطع: إذا كان Γ⊢φi\Gamma \vdash \varphi_{i} لكل ii وكان Γ∪{φ1,…,φn}⊢ψ\Gamma \cup \{\varphi_{1}, \ldots, \varphi_{n}\} \vdash \psi، فإن Γ⊢ψ\Gamma \vdash \psi)، ومبرهنة الاستنتاج (استنتاج) وعكسها (عكس الاستنتاج)، والتكافؤ الاستنتاجي، φ⊣⊢ψ\varphi \dashv\vdash \psi، الذي يعني أن {φ}⊢ψ\{\varphi\} \vdash \psi وأن {ψ}⊢φ\{\psi\} \vdash \varphi؛ وبيّن، بعلامة تحفظها المسلّمات وقاعدة الوضع، أن هذا النظام لا يستنتج بعض الصيغ المتعلقة بالنفي المشترك. وأضاف الدرس الخاص بـأربع تقنيات للاستنتاج القياس الشرطي ({(φ→ψ),(ψ→χ)}⊢(φ→χ)\{(\varphi \rightarrow \psi), (\psi \rightarrow \chi)\} \vdash (\varphi \rightarrow \chi))، وتبادل المقدمات (تبادل)، والنفي المزدوج (φ⊣⊢¬¬φ\varphi \dashv\vdash \neg\neg\varphi، مع مبرهنتيه ⊢(¬¬φ→φ)\vdash (\neg\neg\varphi \rightarrow \varphi) و⊢(φ→¬¬φ)\vdash (\varphi \rightarrow \neg\neg\varphi))، وعكس النقيض بأشكاله الثلاثة:

(φ→ψ)⊣⊢(¬ψ→¬φ),(¬φ→ψ)⊣⊢(¬ψ→φ),(φ→¬ψ)⊣⊢(ψ→¬φ)(\varphi \rightarrow \psi) \dashv\vdash (\neg\psi \rightarrow \neg\varphi), \qquad (\neg\varphi \rightarrow \psi) \dashv\vdash (\neg\psi \rightarrow \varphi), \qquad (\varphi \rightarrow \neg\psi) \dashv\vdash (\psi \rightarrow \neg\varphi)

وبعد البرهان على النفي المزدوج، أكمل الدرس نفسه نظام الدورة بقاعدة أولية ثانية، هي إبدال النفي المزدوج: إذا نتجت χ′\chi' من χ\chi بإبدال ورود واحد لصيغة جزئية θ\theta بـ¬¬θ\neg\neg\theta، أو بإبدال ورود واحد لصيغة جزئية ¬¬θ\neg\neg\theta بـθ\theta، فإنه يُستدل من χ\chi على χ′\chi'. ويُبرَّر السطر الذي يُحصَّل هكذا من السطر ii بـإبدال النفي المزدوج(i)(i). ومنذ تلك النقطة يشير ⊢\vdash إلى نظام الدورة (A1 إلى A3 وقاعدة الوضع وإبدال النفي المزدوج)، الذي تظل تصح فيه الانعكاسية والرتابة وقاعدة القطع ومبرهنة الاستنتاج وعكسها. والقاعدة تعمل على سلسلة اللغة الأساسية، بحيث تبلغ أيضًا الورودات التي يخفيها اختصار، وفي أي من وسيطي نفي مشترك؛ ومن نتائجها المباشرة

(φ↓ψ)⊣⊢(¬¬φ↓ψ),(φ↓ψ)⊣⊢(φ↓¬¬ψ)(\varphi \downarrow \psi) \dashv\vdash (\neg\neg\varphi \downarrow \psi), \qquad (\varphi \downarrow \psi) \dashv\vdash (\varphi \downarrow \neg\neg\psi)

وعمومًا، χ⊣⊢χ′\chi \dashv\vdash \chi' كلما نتجت χ′\chi' من χ\chi بإبدال النفي المزدوج. ويُبرَّر سطر تكافؤ من هذا الشكل بـ«إبدال النفي المزدوج»، بلا رقم سطر، كما يستشهد سطر «نفي مزدوج» أو «عكس النقيض» بتكافؤ سبق البرهان عليه. وكما هناك، يمكن كتابة مبرهنة سبق البرهان عليها سطرًا في استنتاج، لأن استنتاجها الخاص يمكن إدراجه في ذلك الموضع؛ وبتوطئة «من النتيجة إلى القاعدة» في ذلك الدرس، تُطبَّق كل تقنية أيضًا قاعدةً تحت أي مجموعة Γ\Gamma من المقدمات، ويُستشهد بها مع أرقام الأسطر التي تُطبَّق عليها، مثل «عكس النقيض(i)(i)» أو «قياس شرطي(i,j)(i, j)». وفي الاستنتاجات حول الاستنتاجات، تدلّ «مقدمة» على فرضية من فرضيات القاعدة التي يُبرهن عليها.

الاختصارات المعتمدة، التي حُدّدت في الدرس الخاص بـلغة منطق القضايا، هي التعريفات الوحيدة للروابط:

¬φ:=(φ↓φ),(φ∨ψ):=¬(φ↓ψ),(φ∧ψ):=¬(¬φ∨¬ψ)\neg\varphi := (\varphi \downarrow \varphi), \qquad (\varphi \vee \psi) := \neg(\varphi \downarrow \psi), \qquad (\varphi \wedge \psi) := \neg(\neg\varphi \vee \neg\psi)
(φ→ψ):=(¬φ∨ψ),(φ↔ψ):=((φ→ψ)∧(ψ→φ)),(φ⊻ψ):=¬(φ↔ψ)(\varphi \rightarrow \psi) := (\neg\varphi \vee \psi), \qquad (\varphi \leftrightarrow \psi) := ((\varphi \rightarrow \psi) \wedge (\psi \rightarrow \varphi)), \qquad (\varphi \veebar \psi) := \neg(\varphi \leftrightarrow \psi)

السطر المبرَّر بـ«تعريف» لا يستنتج شيئًا: إنه يكتب الصيغة نفسها باسم آخر، والتعليق يقول أي اختصار يُفكّ أو يُطوى («تعريف →\rightarrow»، «تعريف ∨\vee»). ويحسن أن نتذكر الظاهرة التي لوحظت في الدرس الخاص بـصورنة اللغة الطبيعية: الصيغة الواحدة تقبل عدة أسماء، بحيث يكون العطف أيضًا، بوصفه سلسلة، فصلًا. فمثلًا، بفكّ الاستلزام مع ¬φ\neg\varphi بدلًا من φ\varphi، نحصل على

(¬φ→ψ)=(¬¬φ∨ψ)=¬(¬¬φ↓ψ)(\neg\varphi \rightarrow \psi) = (\neg\neg\varphi \vee \psi) = \neg(\neg\neg\varphi \downarrow \psi)

والنفي المزدوج الذي يظهر أمام φ\varphi، والذي يخفيه الاختصار، هو السبب الذي من أجله ستتدخل قاعدة إبدال النفي المزدوج في كل ما يلي.

التكافؤ الاستنتاجي بوصفه مساواة

براهين هذا الدرس كلها تقريبًا تعاقباتٌ من التكافؤات: φ1⊣⊢φ2\varphi_{1} \dashv\vdash \varphi_{2}، φ2⊣⊢φ3\varphi_{2} \dashv\vdash \varphi_{3}، وهكذا دواليك. ولكي يُستخلص من تعاقب أن φ1⊣⊢φn\varphi_{1} \dashv\vdash \varphi_{n}، يجب أن يسلك التكافؤ الاستنتاجي سلوك المساواة، وهذا ما أثبتته القضية الخاصة بخواص التكافؤ الاستنتاجي في الدرس الخاص بـالأنظمة الاستنتاجية الصورية: فالعلاقة انعكاسية (φ⊣⊢φ\varphi \dashv\vdash \varphi)، ومتناظرة (إذا كان φ⊣⊢ψ\varphi \dashv\vdash \psi، فإن ψ⊣⊢φ\psi \dashv\vdash \varphi)، ومتعدية (إذا كان φ⊣⊢ψ\varphi \dashv\vdash \psi وψ⊣⊢χ\psi \dashv\vdash \chi، فإن φ⊣⊢χ\varphi \dashv\vdash \chi)، والصيغتان المتكافئتان استنتاجيًا قابلتان للتبادل بوصفهما نتيجتين (إذا كان Γ⊢φ\Gamma \vdash \varphi وφ⊣⊢φ′\varphi \dashv\vdash \varphi'، فإن Γ⊢φ′\Gamma \vdash \varphi'، لكل مجموعة Γ\Gamma من الصيغ). ويحسن أن نتذكر كيف بُرهن على الخاصتين الأخيرتين، لأن الدرس كله يرتكز عليهما: من {φ}⊢φ′\{\varphi\} \vdash \varphi' ننتقل، بالرتابة، إلى Γ∪{φ}⊢φ′\Gamma \cup \{\varphi\} \vdash \varphi'، ومن هذه ومن Γ⊢φ\Gamma \vdash \varphi، بقاعدة القطع، إلى Γ⊢φ′\Gamma \vdash \varphi'؛ والتعدي ينتج من تطبيق ذلك مع Γ={φ}\Gamma = \{\varphi\} في اتجاه ومع Γ={χ}\Gamma = \{\chi\} في الاتجاه الآخر.

ومن الآن فصاعدًا، تُبرَّر الخطوة التي تجمع تعاقبًا من التكافؤات في تكافؤ واحد بـ«قطع»، وهي أداة تلك القضية. على أن كل حلقة φi⊣⊢φi+1\varphi_{i} \dashv\vdash \varphi_{i+1} تحتوي على الاستنتاجين، استنتاج الذهاب واستنتاج الإياب؛ ومن ثم فإن تعاقبًا من التكافؤات يبرهن في آن واحد على اتجاهي نتيجته كليهما، ولا يبقى شيء «تمرينًا».