منطق الدالة المسندة

المصطلح الذري هو حرف لاتيني كبير، باستثناء الحرفين I و S ، متبوعًا برقم مرفوع يُسمى درجته ، أو بمجموعة من المتغيرات الصغيرة، تُعرف مجتمعةً بقائمة الوسائط . تُشير درجة المصطلح إلى نفس المعلومات التي يُشير إليها عدد المتغيرات التي تلي حرف المسند. يُشير المصطلح الذري من الدرجة 0 إلى متغير منطقي أو قيمة منطقية . درجة الحرف I هي دائمًا 2، ولذلك لا يُشار إليها.

الدوال المسندة "التوافقية" (مصطلح ابتكره كواين)، وهي جميعها أحادية ومميزة لـ PFL، هي Inv و inv و ∃ و + و p . الحد إما أن يكون حدًا ذريًا، أو يُنشأ وفقًا للقاعدة التكرارية التالية. إذا كان τ حدًا، فإن Inv τ و inv τ و ∃ τ و + τ و p τ هي حدود. الدالة التي تحمل رمزًا علويًا n ، حيث n عدد طبيعي أكبر من 1، تدل على n تطبيقًا متتاليًا (تكرارًا) لتلك الدالة.

الصيغة إما مصطلح أو تُعرَّف بالقاعدة التكرارية: إذا كانت α و β صيغتين، فإن αβ و ~(α) صيغتان أيضًا. بالتالي، فإن "~" دالة أحادية أخرى، والربط هو دالة المسند الثنائية الوحيدة. أطلق كواين على هذه الدوال اسم "الدوال الحقيقية". التفسير الطبيعي لـ "~" هو النفي؛ أما الربط فهو أي رابط يشكل، عند دمجه مع النفي، مجموعة كاملة وظيفيًا من الروابط. كانت مجموعة كواين المفضلة الكاملة وظيفيًا هي الاقتران والنفي . لذا تُعتبر المصطلحات المربوطة متصلة . رمز + هو رمز بيكون (1985)؛ وجميع الرموز الأخرى هي رموز كواين (1976؛ 1982). الجزء الحقيقي من PFL مطابق لمخططات المصطلحات البوليانية لكواين (1982).

كما هو معروف جيدًا، يمكن استبدال الدالتين الأليثيتين بدالة ثنائية واحدة بالصيغة والدلالات التالية : إذا كانت α و β صيغتين، فإن (αβ) هي صيغة دلالاتها هي "ليس ( α و/أو β )" ( انظر NAND و NOR ).

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

يرتكز هذا القسم على دوال المسند الأولية وبعض الدوال المُعرَّفة. يمكن صياغة دوال الحقيقة باستخدام أي مجموعة من بديهيات منطق الجمل التي تكون عناصرها الأولية هي النفي وأحد الرمزين ∧ أو ∨. وبالمثل، يمكن اعتبار جميع التكرارات المنطقية لمنطق الجمل بديهيات.

تُذكر أدناه دلالات كواين (1982) لكل دالة مسندة من حيث التجريد (ترميز بناء المجموعة)، متبوعة إما بالبديهية ذات الصلة من كون (1983)، أو بتعريف من كواين (1976).${\displaystyle \{x_{1}\cdots x_{n}:Fx_{1}\cdots x_{n}\}}$يرمز إلى مجموعة n -tuples التي تحقق الصيغة الذرية${\displaystyle Fx_{1}\cdots x_{n}.}$

• الهوية ، I ، تُعرَّف على النحو التالي:

${\displaystyle IFx_{1}x_{2}\cdots x_{n}\leftrightarrow (Fx_{1}x_{1}\cdots x_{n}\leftrightarrow Fx_{2}x_{2}\cdots x_{n}){\text{.}}}$

الهوية انعكاسية ( Ixx )، ومتناظرة ( Ixy → Iyx )، ومتعدية ( ( Ixy ∧ Iyz ) → Ixz )، وتخضع لخاصية الاستبدال:

${\displaystyle (Fx_{1}\cdots x_{n}\land Ix_{1}y)\rightarrow Fyx_{2}\cdots x_{n}.}$

• إضافة الحشو ، + ، تضيف متغيرًا إلى يسار أي قائمة وسائط.

${\displaystyle \ +F^{n}\ {\overset {\underset {\mathrm {def} }{}}{=}}\ \{x_{0}x_{1}\cdots x_{n}:F^{n}x_{1}\cdots x_{n}\}.}$

${\displaystyle +Fx_{1}\cdots x_{n}\leftrightarrow Fx_{2}\cdots x_{n}.}$

• يؤدي الاقتصاص ، ∃ ، إلى حذف المتغير الموجود في أقصى اليسار في أي قائمة وسائط.

${\displaystyle \exists F^{n}\ {\overset {\underset {\mathrm {def} }{}}{=}}\ \{x_{2}\cdots x_{n}:\exists x_{1}F^{n}x_{1}\cdots x_{n}\}.}$

${\displaystyle Fx_{1}\cdots x_{n}\rightarrow \exists Fx_{2}\cdots x_{n}.}$

يُمكّن الاقتصاص من استخدام دالتين معرفتين مفيدتين:

• انعكاس ، S :

${\displaystyle SF^{n}\ {\overset {\underset {\mathrm {def} }{}}{=}}\ \{x_{2}\cdots x_{n}:F^{n}x_{2}x_{2}\cdots x_{n}\}.}$

${\displaystyle SF^{n}\leftrightarrow \exists IF^{n}.}$

يعمم S مفهوم الانعكاسية ليشمل جميع الحدود ذات الدرجة المحدودة الأكبر من 2. ملاحظة: يجب عدم الخلط بين S والمركب الأولي S للمنطق التوافقي.

• الضرب الديكارتي ،${\displaystyle \times }$؛

${\displaystyle F^{m}\times G^{n}\leftrightarrow F^{m}\exists ^{m}G^{n}.}$

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

${\displaystyle F^{m}x_{1}\cdots x_{m}G^{n}x_{1}\cdots x_{n}\leftrightarrow (F^{m}\times G^{n})x_{1}\cdots x_{m}x_{1}\cdots x_{n}.}$

أعد ترتيب قائمة الوسائط المدمجة بحيث يتم نقل زوج من المتغيرات المكررة إلى أقصى اليسار، ثم استدعِ الدالة S لإزالة التكرار. يؤدي تكرار هذه العملية حسب الحاجة إلى قائمة وسائط بطول max( m , n ).

تتيح الدوال الثلاث التالية إعادة ترتيب قوائم الوسائط حسب الرغبة.

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

${\displaystyle \operatorname {Inv} F^{n}\ {\overset {\underset {\mathrm {def} }{}}{=}}\ \{x_{1}\cdots x_{n}:F^{n}x_{n}x_{1}\cdots x_{n-1}\}.}$

${\displaystyle \operatorname {Inv} Fx_{1}\cdots x_{n}\leftrightarrow Fx_{n}x_{1}\cdots x_{n-1}.}$

• الانعكاس الجزئي ، inv ، يقوم بتبديل أول متغيرين في قائمة الوسائط.

${\displaystyle \operatorname {inv} F^{n}\ {\overset {\underset {\mathrm {def} }{}}{=}}\ \{x_{1}\cdots x_{n}:F^{n}x_{2}x_{1}\cdots x_{n}\}.}$

${\displaystyle \operatorname {inv} Fx_{1}\cdots x_{n}\leftrightarrow Fx_{2}x_{1}\cdots x_{n}.}$

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

${\displaystyle \ pF^{n}\ {\overset {\underset {\mathrm {def} }{}}{=}}\ \{x_{1}\cdots x_{n}:F^{n}x_{1}x_{3}\cdots x_{n}x_{2}\}.}$

${\displaystyle pFx_{1}\cdots x_{n}\leftrightarrow \operatorname {Inv} \operatorname {inv} Fx_{1}x_{3}\cdots x_{n}x_{2}.}$

بافتراض وجود قائمة وسائط تتكون من n متغيرًا، فإن الدالة p تتعامل ضمنيًا مع آخر n − 1 متغيرًا كما لو كانت سلسلة دراجة، حيث يمثل كل متغير حلقة في السلسلة. يؤدي تطبيق p مرة واحدة إلى تحريك السلسلة بمقدار حلقة واحدة. يؤدي k تطبيق متتالي للدالة p على F ⁿ إلى نقل المتغير k + 1 إلى موضع الوسيط الثاني في F.

عندما n = 2، فإن Inv و inv يتبادلان x1 و x2 فقط . وعندما n = ₁ ، لا يكون لهما أي تأثير. وبالتالي، فإن _p ليس له أي تأثير عندما n < 3.

يعتبر كون (1983) الانعكاس الرئيسي والانعكاس الثانوي عمليتين أساسيتين. يرمز الرمز p في كون إلى inv ؛ وليس لديه نظير للتبديل ، وبالتالي لا توجد لديه بديهيات له. إذا اعتبرنا p عملية أساسية ، وفقًا لكواين (1976)، فيمكن تعريف inv و inv على أنهما تركيبات غير تافهة من + و ∃ و p المتكرر .

يلخص الجدول التالي كيفية تأثير الدوال على درجات وسائطها.

تعبير	درجة
${\displaystyle p;\operatorname {Inv}$ ;\operatorname {inv}  ;\ \lnot  ;\ I}	لا تغيير
${\displaystyle +F^{n-1};\ \exists F^{n+1};\ SF^{n+1}}$	ن
${\displaystyle \alpha ^{m}\beta ^{n};\ F^{m}\times G^{n}}$	أقصى ( م ، ن )

يجوز استبدال جميع حالات حرف المسند بحرف مسند آخر من نفس الدرجة، دون التأثير على صحة الحكم. والقواعد هي :

• Modus ponens ;
• لتكن α و β صيغتين من صيغ PFL حيث${\displaystyle x_{1}}$لا يظهر. ثم إذا${\displaystyle (\alpha \land Fx_{1}...x_{n})\rightarrow \beta }$إذا كانت نظرية PFL،${\displaystyle (\alpha \land \exists Fx_{2}...x_{n})\rightarrow \beta }$وهي كذلك نظرية PFL.

بدلاً من وضع بديهيات PFL، اقترح كواين (1976) التخمينات التالية كبديهيات مرشحة.

${\displaystyle \exists I}$

n − 1 تكرارات متتالية لـ p تعيد الوضع إلى ما كان عليه قبل ذلك :

${\displaystyle F^{n}\leftrightarrow p^{n-1}F^{n}}$

+ و ∃ يفنيان بعضهما البعض:

${\displaystyle {\begin{cases}F^{n}\rightarrow +\exists F^{n}\\F^{n}\leftrightarrow \exists +F^{n}\end{cases}}}$

يتم توزيع النفي على + و ∃ و p :

${\displaystyle {\begin{cases}+\lnot F^{n}\leftrightarrow \lnot +F^{n}\\\lnot \exists F^{n}\rightarrow \exists \lnot F^{n}\\p\lnot F^{n}\leftrightarrow \lnot pF^{n}\end{cases}}}$

+ و p يتوزعان على العطف:

${\displaystyle {\begin{cases}+(F^{n}G^{m})\leftrightarrow (+F^{n}+G^{m})\\p(F^{n}G^{m})\leftrightarrow (pF^{n}pG^{m})\end{cases}}}$

للهوية دلالة مثيرة للاهتمام:

${\displaystyle IF^{n}\rightarrow p^{n-2}\exists p+F^{n}}$

افترض كواين أيضاً القاعدة التالية: إذا كانت α نظرية PFL، فإن p α و + α و${\displaystyle \lnot \exists \lnot \alpha }$.