تركيبة جيدة التكوين

في المنطق الرياضي ، ومنطق القضايا ، ومنطق المسندات ، فإن الصيغة السليمة ، والتي يختصرها WFF أو wff ، وغالبًا ما تكون ببساطة صيغة ، هي سلسلة محدودة من الرموز من أبجدية معينة ، يتم إنشاؤها وفقًا لقواعد اللغة الرسمية المحددة . ^{[ 1 ]}

يُنطق الاختصار wff "ووف"، أو أحيانًا "ويف"، أو "ويف"، أو "ويف". ^{[ 12 ]}

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

مقدمة

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

على الرغم من إمكانية استخدام مصطلح "الصيغة" للإشارة إلى العلامات المكتوبة (على سبيل المثال، على ورقة أو سبورة)، إلا أنه يُفهم بدقة أكبر على أنه سلسلة من الرموز المُعبَّر عنها، حيث تُمثل العلامات مثالًا نموذجيًا للصيغة. هذا التمييز بين المفهوم المبهم لـ"الخاصية" والمفهوم المُعرَّف استقرائيًا للصيغة المُصاغة جيدًا له جذور في ورقة فايل البحثية لعام 1910 بعنوان "Über die Definitionen der mathematischen Grundbegriffe". ^{[ 13 ]} وبالتالي، يمكن كتابة الصيغة نفسها أكثر من مرة، وقد تكون الصيغة من حيث المبدأ طويلة جدًا لدرجة أنه لا يمكن كتابتها على الإطلاق في الكون المادي.

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

حساب القضايا

تُعرف صيغ حساب القضايا ، والتي تُسمى أيضًا بالصيغ القضايا ، ^{[ 14 ]} بأنها تعابير مثل $(A\land (B\lor C))$ يبدأ تعريفها باختيار عشوائي لمجموعة V من المتغيرات المنطقية . تتكون الأبجدية من حروف V بالإضافة إلى رموز الروابط المنطقية والأقواس "(" و ")"، والتي يُفترض أنها جميعًا ليست ضمن V. ستكون الصيغ عبارة عن تعابير معينة (أي سلاسل من الرموز) على هذه الأبجدية.

تُعرَّف الصيغ استقرائياً على النحو التالي:

كل متغير افتراضي هو، في حد ذاته، صيغة.
إذا كانت φ صيغة، فإن ¬ φ صيغة أيضًا.
إذا كانت φ و ψ صيغتين، و • أي رابط ثنائي، فإن (φ • ψ) صيغة. هنا، يمكن أن يكون • (على سبيل المثال لا الحصر) أحد العوامل المعتادة ∨، ∧، →، أو ↔.

يمكن أيضًا كتابة هذا التعريف كقواعد نحوية رسمية في شكل باكوس-ناور ، بشرط أن تكون مجموعة المتغيرات محدودة:

< مجموعة ألفا > ::= p | q | r | s | t | u | ... (مجموعة المتغيرات المنطقية المحدودة) < صيغة > ::= < مجموعة ألفا > | ¬ < صيغة > | ( < صيغة > ∧ < صيغة > ) | ( < صيغة > ∨ < صيغة > ) | ( < صيغة > → < صيغة > ) | ( < صيغة > ↔ < صيغة > )

باستخدام هذه القواعد، يكون تسلسل الرموز

((( p → q ) ∧ ( r → s )) ∨ ( ¬ q ∧ ¬ s ))

هي صيغة، لأنها صحيحة نحوياً. تسلسل الرموز

(( p → q ) → ( qq )) p ))

ليست صيغة، لأنها لا تتوافق مع قواعد اللغة.

قد يصعب قراءة الصيغة المعقدة، وذلك بسبب كثرة الأقواس، على سبيل المثال. وللتخفيف من هذه المشكلة، تُفترض قواعد أسبقية (شبيهة بترتيب العمليات الرياضية القياسي ) بين المعاملات، مما يجعل بعضها أكثر إلزامًا من غيرها. على سبيل المثال، بافتراض الأسبقية (من الأكثر إلزامًا إلى الأقل إلزامًا) 1. ¬ 2. → 3. ∧ 4. ∨ ، فإن الصيغة

((( p → q ) ∧ ( r → s )) ∨ ( ¬ q ∧ ¬ s ))

يمكن اختصارها إلى

p → q ∧ r → s ∨ ¬ q ∧ ¬ s

مع ذلك، هذا مجرد اصطلاح يُستخدم لتبسيط التمثيل الكتابي للصيغة. فإذا افترضنا، على سبيل المثال، أن ترتيب العمليات هو ترتيب ترابطي من اليسار إلى اليمين، على النحو التالي: 1. ¬ 2. ∧ 3. ∨ 4. → ، فإن الصيغة نفسها أعلاه (بدون أقواس) ستُعاد كتابتها على النحو التالي:

( p → ( q ∧ r )) → ( s ∨ ( ¬ q ∧ ¬ s ))

منطق المسند

تعريف الصيغة في منطق الرتبة الأولى ${\mathcal {QS}}$ يرتبط هذا الأمر بتوقيع النظرية قيد الدراسة. ويحدد هذا التوقيع الرموز الثابتة، ورموز المسندات، ورموز الدوال في النظرية قيد الدراسة، بالإضافة إلى عدد معاملات رموز الدوال والمسندات.

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

أي متغير هو مصطلح.
أي رمز ثابت من التوقيع هو مصطلح
التعبير من الشكل f ( t ₁ ,..., t _n )، حيث f هو رمز دالة n -ary، و t ₁ ,..., t _n هي حدود، هو مرة أخرى حد.

الخطوة التالية هي تحديد الصيغ الذرية .

إذا كان _t1و t2 حدين ، _فإن_t1= _t2هي صيغة ذرية
إذا كان R رمزًا للمسند n -ary، وكانت t1 _، ...، _tn حدودًا ، فإن R ( t1 _، ...، tn ₎ صيغة ذرية

وأخيرًا، تُعرَّف مجموعة الصيغ بأنها أصغر مجموعة تحتوي على مجموعة الصيغ الذرية بحيث يتحقق ما يلي:

$\neg \phi$ هي صيغة عندما $\phi$ هي صيغة
$(\phi \land \psi )$ و $(\phi \lor \psi )$ هي صيغ عندما $\phi$ و $\psi$ هي صيغ رياضية؛
$\exists x\,\phi$ هي صيغة عندما $x$ متغير و $\phi$ هي صيغة رياضية؛
$\forall x\,\phi$ هي صيغة عندما $x$ متغير و $\phi$ هي صيغة (أو بديلًا، $\forall x\,\phi$ يمكن تعريفها على أنها اختصار لـ $\neg \exists x\,\neg \phi$ ).

إذا لم تتضمن الصيغة أي حالات من $\exists x$ أو $\forall x$ ، لأي متغير $x$ ثم يُطلق عليه اسمصيغة خالية من المحددات الكمية . الصيغة الوجودية هي صيغة تبدأ بتسلسل من التحديد الكمي الوجودي متبوعًا بصيغة خالية من المحددات الكمية.

الصيغ الذرية والمفتوحة

الصيغة الذرية هي صيغة لا تحتوي على روابط منطقية ولا مُكمِّمات ، أو بعبارة أخرى، صيغة لا تحتوي على صيغ فرعية محددة. يعتمد الشكل الدقيق للصيغ الذرية على النظام الصوري قيد الدراسة؛ ففي منطق القضايا ، على سبيل المثال، تكون الصيغ الذرية هي متغيرات القضايا . أما في منطق المسندات ، فتكون الذرات هي رموز المسندات مع وسائطها، حيث يمثل كل وسيط حدًا .

بحسب بعض المصطلحات، تُصاغ الصيغة المفتوحة بدمج الصيغ الذرية باستخدام الروابط المنطقية فقط، دون استخدام أدوات التحديد الكمي. ^{[ 15 ]} ويجب عدم الخلط بين هذه الصيغة والصيغة غير المغلقة.

الصيغ المغلقة

الصيغة المغلقة ، أو الصيغة الأساسية ، هي صيغة لا تحتوي على أي ظهور حر لأي متغير . إذا $كانت$ A صيغةً للغة $من$ الدرجة الأولى حيث توجد المتغيرات $v1$ $،$ ... $،$ $vn$ $بظهور$ حر، $فإن$ A مسبوقة بـ $\forallv1$ $...$ $\forallvn$ $تُشكّل$ إغلاقًا شاملاً لـ A.

الخصائص التي تنطبق على الصيغ

الصيغة أ في اللغة ${\mathcal {Q}}$ تكون صحيحة إذا كانت صحيحة لكل تفسير لـ ${\mathcal {Q}}$ .
الصيغة أ في اللغة ${\mathcal {Q}}$ تكون قابلة للتحقيق إذا كانت صحيحة بالنسبة لتفسير معين لـ ${\mathcal {Q}}$ .
تكون الصيغة A للغة الحساب قابلة للتقرير إذا كانت تمثل مجموعة قابلة للتقرير ، أي إذا كانت هناك طريقة فعالة ، عند إعطاء استبدال للمتغيرات الحرة لـ A ، تقول إما أن الحالة الناتجة من A قابلة للإثبات أو أن نفيها كذلك.

استخدام المصطلحات

في الأعمال السابقة حول المنطق الرياضي (على سبيل المثال بواسطة Church ^{[ 16 ]} )، كانت الصيغ تشير إلى أي سلاسل من الرموز، ومن بين هذه السلاسل، كانت الصيغ جيدة التكوين هي السلاسل التي تتبع قواعد تكوين الصيغ (الصحيحة).

يستخدم العديد من المؤلفين مصطلح "صيغة" ببساطة. ^{[ 17 ]}^{[ 18 ]}^{[ 19 ]}^{[ 20 ]} تميل الاستخدامات الحديثة (خاصة في سياق علوم الحاسوب مع البرامج الرياضية مثل مدققي النماذج ، ومثبتي النظريات الآليين ، ومثبتي النظريات التفاعليين ) إلى الاحتفاظ بمفهوم الصيغة الجبرية فقط، وترك مسألة صحة الصياغة ، أي التمثيل النصي الملموس للصيغ (باستخدام هذا الرمز أو ذاك للروابط والمحددات الكمية، واستخدام اصطلاح الأقواس هذا أو ذاك ، واستخدام الترميز البولندي أو الترميز الوسطي ، وما إلى ذلك) كمشكلة ترميزية بحتة.

تسلل مصطلح "الصيغ السليمة" (WFF) إلى الثقافة الشعبية. ويُعدّ WFF جزءًا من تورية باطنية استُخدمت في اسم اللعبة الأكاديمية " WFF 'N PROOF : The Game of Modern Logic" من ابتكار لايمان ألين، ^{[ 21 ]} الذي طوّره أثناء دراسته في كلية الحقوق بجامعة ييل (وأصبح لاحقًا أستاذًا في جامعة ميشيغان ). صُممت هذه المجموعة من الألعاب لتعليم مبادئ المنطق الرمزي للأطفال ( بالتدوين البولندي ). ^{[ 22 ]} واسمها صدى لكلمة whiffenpoof ، وهي كلمة لا معنى لها كانت تُستخدم كهتاف في جامعة ييل، واشتهرت في أغنية Whiffenpoof وفرقة Whiffenpoofs . ^{[ 23 ]}

انظر أيضاً

ملحوظات

↑ تعتبر الصيغ موضوعًا قياسيًا في المنطق التمهيدي، وتغطيها جميع الكتب التمهيدية، بما في ذلك Enderton (2001) و Gamut (1990) و Kleene (1967).
↑ جينسلر، هاري (11 سبتمبر 2002). مقدمة في المنطق . روتليدج. ص 35. ISBN 978-1-134-58880-0.
↑ هول، كورديليا؛ أودونيل، جون (17 أبريل 2013). الرياضيات المتقطعة باستخدام الحاسوب . سبرينغر ساينس آند بيزنس ميديا. ص 44. ISBN 978-1-4471-3657-6.
↑ أغلر، ديفيد و. (2013). المنطق الرمزي: بناء الجملة، والدلالات، والبرهان . روومان وليتلفيلد. ص 41. ISBN 978-1-4422-1742-3.
↑ سيمبسون، آر إل (17 مارس 2008). أساسيات المنطق الرمزي - الطبعة الثالثة . دار برودفيو للنشر. ص 14. ISBN 978-1-77048-495-5.
↑ لاديروت، كارل (24-10-2022). دليل موجز للمنطق الصوري . دار برودفيو للنشر. ص 59. ISBN 978-1-77048-868-7.
↑ ماورر، ستيفن ب.؛ رالستون، أنتوني (21 يناير 2005). الرياضيات الخوارزمية المنفصلة، الطبعة الثالثة . مطبعة سي آر سي. ص 625. ISBN 978-1-56881-166-6.
↑ مارتن، روبرت م. (6 مايو 2002). قاموس الفيلسوف - الطبعة الثالثة . دار برودفيو للنشر. ص 323. ISBN 978-1-77048-215-9.
↑ ديت، كريستوفر (14-10-2008). قاموس قواعد البيانات العلائقية، الطبعة الموسعة . أبريس. ص 211. ISBN 978-1-4302-1042-9.
↑ ديت، سي جيه (21-12-2015). قاموس قواعد البيانات العلائقية الجديد: المصطلحات والمفاهيم والأمثلة . دار نشر أورايلي ميديا، ص 241. ISBN 978-1-4919-5171-2.
↑ سيمبسون، ر. ل. (10 ديسمبر 1998). أساسيات المنطق الرمزي . دار برودفيو للنشر. ص 12. ISBN 978-1-55111-250-3.
↑
- "نباح" ^{[ 2 ]}^{[ 3 ]}^{[ 4 ]}^{[ 5 ]}
- "wiff" ^{[ 6 ]}^{[ 7 ]}^{[ 8 ]}
- "ويف" ^{[ 9 ]}^{[ 10 ]}
- "نفحة" ^{[ 11 ]}
أيدت جميع المصادر نطق "woof". أما المصادر التي استشهدت بنطق "wiff" و"weff" و"whiff" فقد قدمت هذه النطقات كبدائل لنطق "woof". ويذكر مصدر جينسلر "wood" و"woofer" كمثالين على كيفية نطق حرف العلة في "woof".
↑ دبليو. دين، إس. والش، تاريخ ما قبل الأنظمة الفرعية للحساب من الدرجة الثانية (2016)، ص. 6
↑ المنطق من الدرجة الأولى وإثبات النظريات الآلي، ميلفين فيتينغ، سبرينغر، 1996
↑ دليل تاريخ المنطق، (المجلد 5، المنطق من راسل إلى تشيرش)، منطق تارسكي من تحرير كيث سيمونز، ودي. غاباي، وج. وودز، صفحة 568.
↑ ألونزو تشيرش، [1996] (1944)، مقدمة في المنطق الرياضي، صفحة 49
↑ هيلبرت، ديفيد ؛ أكرمان، فيلهلم (1950) [1937]، مبادئ المنطق الرياضي، نيويورك: تشيلسي
↑ هودجز، ويلفريد (1997)، نظرية نموذجية مختصرة، مطبعة جامعة كامبريدج، رقم ISBN 978-0-521-58713-6
↑ باروايز، جون ، محرر (1982)، دليل المنطق الرياضي، دراسات في المنطق وأسس الرياضيات، أمستردام: نورث هولاند، ISBN 978-0-444-86388-1
↑ كوري، رينيه؛ لاسكار، دانيال (2000)، المنطق الرياضي: دورة مع تمارين، مطبعة جامعة أكسفورد، رقم ISBN 978-0-19-850048-3
↑ إهرنبورغ 2002
↑ من الناحية الفنية، المنطق الافتراضي باستخدام حساب التفاضل والتكامل على طريقة فيتش .
↑ يقر ألين (1965) بالتورية.

مراجع

ألين، لايمان إي. (1965)، "نحو التعلم الذاتي للمنطق الرياضي من خلال ألعاب إثبات WFF 'N"، التعلم الرياضي: تقرير مؤتمر برعاية لجنة أبحاث العمليات الفكرية التابعة لمجلس أبحاث العلوم الاجتماعية ، دراسات جمعية أبحاث نمو الطفل، 30 (1): 29-41
بولوس، جورج ؛ بورغيس، جون؛ جيفري، ريتشارد (2002)، الحوسبة والمنطق (الطبعة الرابعة )، مطبعة جامعة كامبريدج ، رقم ISBN 978-0-521-00758-0
إهرنبرغ، راشيل (ربيع 2002). "إنه منطقي للغاية" . ميشيغان توداي . جامعة ميشيغان. مؤرشف من الأصل بتاريخ 8 فبراير 2009. تم الاطلاع عليه بتاريخ 19 أغسطس 2007 .
إندرتون، هربرت (2001)، مقدمة رياضية في المنطق (الطبعة الثانية )، بوسطن، ماساتشوستس: دار النشر الأكاديمية ، رقم ISBN 978-0-12-238452-3
غاموت، إل تي إف (1990)، المنطق واللغة والمعنى، المجلد 1: مقدمة في المنطق ، مطبعة جامعة شيكاغو، رقم ISBN 0-226-28085-3
هودجز، ويلفريد (2001)، "المنطق الكلاسيكي 1: منطق الرتبة الأولى"، في جوبل، لو (محرر)، دليل بلاكويل للمنطق الفلسفي ، بلاكويل، ISBN 978-0-631-20692-7
هوفستاتر، دوغلاس (1980)، غودل، إيشر، باخ: ضفيرة ذهبية أبدية ، دار بنجوين للنشر ، رقم ISBN 978-0-14-005579-5
كلين، ستيفن كول (2002) [1967]، المنطق الرياضي ، نيويورك: منشورات دوفر ، ISBN 978-0-486-42533-7MR 1950307
راوتنبرغ، وولفغانغ (2010)، مقدمة موجزة في المنطق الرياضي ( الطبعة الثالثة)، نيويورك: سبرينغر ساينس + بيزنس ميديا ، doi : 10.1007/978-1-4419-1221-3 ، ISBN 978-1-4419-1220-6

روابط خارجية

صيغة سليمة لمنطق المسند من الدرجة الأولى - تتضمن اختبارًا قصيرًا بلغة جافا .
معادلة سليمة في بروفن ماث

[1] تعتبر الصيغ موضوعًا قياسيًا في المنطق التمهيدي، وتغطيها جميع الكتب التمهيدية، بما في ذلك Enderton (2001) و Gamut (1990) و Kleene (1967).

[2] جينسلر، هاري (11 سبتمبر 2002). مقدمة في المنطق . روتليدج. ص 35. ISBN 978-1-134-58880-0.

[3] هول، كورديليا؛ أودونيل، جون (17 أبريل 2013). الرياضيات المتقطعة باستخدام الحاسوب . سبرينغر ساينس آند بيزنس ميديا. ص 44. ISBN 978-1-4471-3657-6.

[4] أغلر، ديفيد و. (2013). المنطق الرمزي: بناء الجملة، والدلالات، والبرهان . روومان وليتلفيلد. ص 41. ISBN 978-1-4422-1742-3.

[5] سيمبسون، آر إل (17 مارس 2008). أساسيات المنطق الرمزي - الطبعة الثالثة . دار برودفيو للنشر. ص 14. ISBN 978-1-77048-495-5.

[6] لاديروت، كارل (24-10-2022). دليل موجز للمنطق الصوري . دار برودفيو للنشر. ص 59. ISBN 978-1-77048-868-7.

[7] ماورر، ستيفن ب.؛ رالستون، أنتوني (21 يناير 2005). الرياضيات الخوارزمية المنفصلة، الطبعة الثالثة . مطبعة سي آر سي. ص 625. ISBN 978-1-56881-166-6.

[8] مارتن، روبرت م. (6 مايو 2002). قاموس الفيلسوف - الطبعة الثالثة . دار برودفيو للنشر. ص 323. ISBN 978-1-77048-215-9.

[9] ديت، كريستوفر (14-10-2008). قاموس قواعد البيانات العلائقية، الطبعة الموسعة . أبريس. ص 211. ISBN 978-1-4302-1042-9.

[10] ديت، سي جيه (21-12-2015). قاموس قواعد البيانات العلائقية الجديد: المصطلحات والمفاهيم والأمثلة . دار نشر أورايلي ميديا، ص 241. ISBN 978-1-4919-5171-2.

[11] سيمبسون، ر. ل. (10 ديسمبر 1998). أساسيات المنطق الرمزي . دار برودفيو للنشر. ص 12. ISBN 978-1-55111-250-3.

[12] 
"نباح" ^{[ 2 ]}^{[ 3 ]}^{[ 4 ]}^{[ 5 ]}
"wiff" ^{[ 6 ]}^{[ 7 ]}^{[ 8 ]}
"ويف" ^{[ 9 ]}^{[ 10 ]}
"نفحة" ^{[ 11 ]}
أيدت جميع المصادر نطق "woof". أما المصادر التي استشهدت بنطق "wiff" و"weff" و"whiff" فقد قدمت هذه النطقات كبدائل لنطق "woof". ويذكر مصدر جينسلر "wood" و"woofer" كمثالين على كيفية نطق حرف العلة في "woof".

[mwAiE] "نباح" ^{[ 2 ]}^{[ 3 ]}^{[ 4 ]}^{[ 5 ]}

[mwAjI] "wiff" ^{[ 6 ]}^{[ 7 ]}^{[ 8 ]}

[mwAj8] "ويف" ^{[ 9 ]}^{[ 10 ]}

[mwAkg] "نفحة" ^{[ 11 ]}

[13] دبليو. دين، إس. والش، تاريخ ما قبل الأنظمة الفرعية للحساب من الدرجة الثانية (2016)، ص. 6

[14] المنطق من الدرجة الأولى وإثبات النظريات الآلي، ميلفين فيتينغ، سبرينغر، 1996

[15] دليل تاريخ المنطق، (المجلد 5، المنطق من راسل إلى تشيرش)، منطق تارسكي من تحرير كيث سيمونز، ودي. غاباي، وج. وودز، صفحة 568.

[16] ألونزو تشيرش، [1996] (1944)، مقدمة في المنطق الرياضي، صفحة 49

[17] هيلبرت، ديفيد ؛ أكرمان، فيلهلم (1950) [1937]، مبادئ المنطق الرياضي، نيويورك: تشيلسي

[18] هودجز، ويلفريد (1997)، نظرية نموذجية مختصرة، مطبعة جامعة كامبريدج، رقم ISBN 978-0-521-58713-6

[19] باروايز، جون ، محرر (1982)، دليل المنطق الرياضي، دراسات في المنطق وأسس الرياضيات، أمستردام: نورث هولاند، ISBN 978-0-444-86388-1

[20] كوري، رينيه؛ لاسكار، دانيال (2000)، المنطق الرياضي: دورة مع تمارين، مطبعة جامعة أكسفورد، رقم ISBN 978-0-19-850048-3

[21] إهرنبورغ 2002

[22] من الناحية الفنية، المنطق الافتراضي باستخدام حساب التفاضل والتكامل على طريقة فيتش .

[23] يقر ألين (1965) بالتورية.

[ 1 ]

[ 12 ]

[ 13 ]

[ 14 ]

[ 15 ]

[ 16 ]

[ 17 ]

[ 18 ]

[ 19 ]

[ 20 ]

[ 21 ]

[ 22 ]

[ 23 ]

[ 2 ]

[ 3 ]

[ 4 ]

[ 5 ]

[ 6 ]

[ 7 ]

[ 8 ]

[ 9 ]

[ 10 ]

[ 11 ]