البوابة الدوارة (رمز)

في المنطق الرياضي وعلوم الحاسوب، يرمز الرمز ⊢ (${\displaystyle \vdash }$أُطلق على هذا المصطلح اسم "البوابة الدوارة " لتشابهه مع البوابة الدوارة التقليدية . ويُشار إليه أيضاً باسم "تي" وغالباً ما يُقرأ بمعنى "يُعطي" أو "يثبت" أو "يُرضي" أو "يستلزم".

تمثل البوابة الدوارة علاقة ثنائية . ولها تفسيرات مختلفة في سياقات مختلفة:

• في مجال نظرية المعرفة ، يحلل بير مارتن-لوف (1996)${\displaystyle \vdash }$يرمز إلى ذلك على النحو التالي: "...[إن] الجمع بين خط الحكم [  |  ] وخط المحتوى [—]، أصبح يُطلق عليه علامة التأكيد." ^{[ 1 ]} تدوين فريجه لحكم على محتوى ما A

${\displaystyle \vdash A}$

ويمكن قراءتها بعد ذلك

أعلم أن أ صحيح . ^{[ 2 ]}

وبالمثل، تأكيد مشروط

${\displaystyle P\vdash Q}$

يمكن قراءتها على النحو التالي:

من النقطة P ، أعرف أن Q

• في علم ما وراء اللغة ، وهو دراسة اللغات الصورية ، يُمثل رمز البوابة الدوارة نتيجة نحوية (أو "قابلية الاشتقاق"). بمعنى آخر، يُظهر هذا الرمز إمكانية اشتقاق سلسلة نصية من أخرى في خطوة واحدة، وفقًا لقواعد التحويل (أي النحو ) لنظام صوري مُحدد . ^{[ 3 ]} وعلى هذا النحو، فإن التعبير

${\displaystyle P\vdash Q}$

هذا يعني أن Q يمكن اشتقاقها من P في النظام.

تماشياً مع استخدامها للاستدلال على الاشتقاق، فإن الرمز "⊢" متبوعاً بتعبير دون أي شيء يسبقه يدل على نظرية ، أي أن التعبير يمكن اشتقاقه من القواعد باستخدام مجموعة فارغة من البديهيات . وعلى هذا النحو، فإن التعبير

${\displaystyle \vdash Q}$

هذا يعني أن Q هي نظرية في النظام.

• في نظرية البرهان ، يُستخدم رمز البوابة الدوارة للدلالة على "إمكانية الإثبات" أو "إمكانية الاشتقاق". على سبيل المثال، إذا كانت T نظرية رسمية و S جملة معينة في لغة النظرية، فإن

${\displaystyle T\vdash S}$

يعني ذلك أن S قابلة للإثبات من T. ^{[ 4 ]} وقد تم توضيح هذا الاستخدام في مقالة حساب القضايا . ينبغي مقارنة النتيجة النحوية للإثبات بالنتيجة الدلالية، التي يُرمز لها برمز البوابة المزدوجة .${\displaystyle \models }$يقول أحدهم أن${\displaystyle S}$هو نتيجة دلالية لـ${\displaystyle T}$، أو${\displaystyle T\models S}$، عندما تكون جميع التقييمات الممكنة التي${\displaystyle T}$صحيح،${\displaystyle S}$وهذا صحيح أيضاً. بالنسبة لمنطق القضايا، يمكن إثبات أن النتيجة الدلالية${\displaystyle \models }$وقابلية الاشتقاق${\displaystyle \vdash }$متكافئة فيما بينها. أي أن منطق القضايا سليم (${\displaystyle \vdash }$يشير إلى${\displaystyle \models }$) وأكمل (${\displaystyle \models }$يشير إلى${\displaystyle \vdash }$) ^{[ 5 ]}

• في حساب المتتابعات ، يُستخدم رمز البوابة الدوارة للدلالة على المتتابعة . المتتابعة${\displaystyle A_{1},\,\dots ,A_{m}\,\vdash \,B_{1},\,\dots ,B_{n}}$يؤكد ذلك أنه إذا كانت جميع المقدمات${\displaystyle A_{1},\,\dots ,A_{m}}$إذا كانت هذه النتائج صحيحة، فإن واحدة على الأقل من النتائج المترتبة على ذلك ستكون صحيحة.${\displaystyle B_{1},\,\dots ,B_{n}}$لا بد أن يكون ذلك صحيحاً.
• في حساب التفاضل والتكامل اللامدا المكتوب ، تُستخدم البوابة الدوارة لفصل افتراضات الكتابة عن حكم الكتابة. ^{[ 6 ] [ 7 ]}
• في نظرية الفئات ، البوابة الدوارة المعكوسة (${\displaystyle \dashv }$), كما في${\displaystyle F\dashv G}$يُستخدم الرمز للإشارة إلى أن الدالة F هي دالة مرافقة يسارية للدالة G. ^{[ 8 ]} وفي حالات نادرة، يُستخدم الرمز للإشارة إلى بوابة دوارة (${\displaystyle \vdash }$), كما في${\displaystyle G\vdash F}$يُستخدم للإشارة إلى أن الدالة G هي دالة مرافقة ^يمنى للدالة F. [ ^{9 ]}
• في لغة APL، يُطلق على الرمز اسم "الرابط الأيمن" ويمثل دالة التطابق اليمنى المزدوجة حيث يكون كل من X ⊢ Y و ⊢ Y هو Y. أما الرمز المعكوس "⊣" فيُطلق عليه اسم "الرابط الأيسر" ويمثل دالة التطابق اليسرى المماثلة حيث يكون X ⊣ Y هو X و ⊣ Y هو Y. ^{[ 10 ] [ 11 ]}
• في علم التوافيق ،${\displaystyle \lambda \vdash n}$يعني ذلك أن λ هو تجزئة للعدد الصحيح n . ^{[ 12 ]}
• في سلسلة آلات حاسبة HP-41C / CV / CX و HP-42S من شركة هيوليت-باكارد ، يُطلق على الرمز (عند النقطة 127 في مجموعة أحرف FOCAL ) اسم "حرف الإلحاق"، ويُستخدم للإشارة إلى أنه سيتم إلحاق الأحرف التالية بسجل الأحرف الأبجدية بدلاً من استبدال محتوياته الحالية. كما يدعم هذا الرمز (عند النقطة 148) نسخةً معدلةً من مجموعة أحرف HP Roman-8 المستخدمة في آلات حاسبة HP الأخرى.
• في آلات حاسبة Casio fx-92 Collège 2D و fx-92+ Spéciale Collège، ^{[ 13 ]} يمثل الرمز عامل باقي القسمة ؛ عند إدخال${\displaystyle 5\vdash 2}$سينتج عنه إجابة من${\displaystyle Q=2;R=1}$، حيث Q هو ناتج القسمة و R هو الباقي .
• في نظرية النماذج ،${\displaystyle \varphi \vdash \psi }$وسائل${\displaystyle \varphi }$يستلزم${\displaystyle \psi }$كل طراز من${\displaystyle \varphi }$هو نموذج لـ${\displaystyle \psi }$.

في TeX ، رمز البوابة الدوارة${\displaystyle \vdash }$يتم الحصول عليها من الأمر \vdash .

في نظام يونيكود ، يُطلق على رمز البوابة الدوارة ( ⊢ ) اسم "المسار الأيمن" ويقع عند نقطة الترميز U+22A2. ^{[ 14 ]} (نقطة الترميز U+22A6 تسمى علامة التأكيد ( ⊦ ).)

• U+22A2 ⊢ RIGHT TACK ( & RightTee;, & vdash; )
  • = بوابة دوارة
  • = يثبت، يستلزم، ينتج
  • = قابل للاختزال
• U+22A3 ⊣ LEFT TACK ( & dashv;, & LeftTee; )
  • = بوابة دوارة عكسية
  • = ليس نظرية، لا ينتج عنه
• U+22AC ⊬ لا يثبت ( & nvdash; )
  • ≡ U+22A2 ⊢ RIGHT TACK U+0338 ̸ COMBING LONG SOLIDUS OVERLAY

على الآلة الكاتبة ، يمكن تكوين البوابة الدوارة من خط عمودي (|) وشرطة ( –).

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

• ꜔ (U+A714) حرف مُعدِّل شريط النغمة الأيسر الأوسط
• ├ (U+251C) رسومات صندوقية ضوء رأسي ويمين
• ㅏ (U+314F) حرف الهانغول A
• Ͱ (U+0370) الحرف اليوناني الكبير هيتا
• ͱ (U+0371) الحرف اليوناني الصغير هيتا
• Ⱶ (U+2C75) حرف لاتيني كبير نصف H
• ⱶ (U+2C76) حرف لاتيني صغير نصف H
• ⎬ (U+23AC) قطعة وسطى من القوس المعقوف الأيمن

• بوابة دوارة مزدوجة ⊨
• قائمة الرموز المنطقية
• قائمة الرموز الرياضية

• فريج ، جوتلوب (1879). Begriffsschrift: Eine der arithmetischen nachgebildete Formelsprache desrainen Denkens . هالي.
• إيفرسون، كينيث (1987). قاموس لغة APL .
• مارتن-لوف، بير (1996). "حول معاني الثوابت المنطقية ومبررات القوانين المنطقية" (ملف PDF) . المجلة الإسكندنافية للمنطق الفلسفي . 1 (1): 11-60 .(ملاحظات محاضرة عن دورة قصيرة في جامعة ديجلي ستودي دي سيينا، أبريل 1983.)
• شميدت، ديفيد (1994). بنية لغات البرمجة المكتوبة . مطبعة معهد ماساتشوستس للتكنولوجيا . ISBN 0-262-19349-3.
• ترولسترا، أ.س .؛ شفيتشتنبرغ، هـ. (2000). نظرية البرهان الأساسية (  الطبعة الثانية). مطبعة جامعة كامبريدج . ISBN 978-0-521-77911-1.