Geometric logic
ریاضیاتی منطق میں، ہندسی منطق مربوط منطق کی ایک لامحدود عمومی شکل ہے، جو اسکولیم کی وجہ سے فرسٹ آرڈر منطق کی ایک پابندی ہے جو ثبوت-نظریاتی طور پر قابل عمل ہے۔ ہندسی منطق بہت سے ریاضیاتی نظریات کا اظہار کرنے کی صلاحیت رکھتی ہے اور اس کا ٹوپوس تھیوری سے قریبی تعلق ہے۔ تعریفیں فرسٹ آرڈر منطق کا ایک نظریہ ہندسی ہے اگر اسے صرف اس فارم کے محوریوں کا استعمال کرتے ہوئے محوری بنایا جا سکتا ہے جہاں I اور J فارمولوں کے اشاریہ جات کے جداگانہ مجموعے ہیں کہ ہر ایک لامحدود ہو سکتا ہے اور فارمولے φ یا تو ایٹم ہیں یا ایٹموں کے منفی ہیں۔ اگر تمام محوریات محدود ہیں (یعنی، ہر محوری کے لیے، I اور J دونوں محدود ہیں)، تو نظریہ مربوط ہے۔ نظریہ ہر فرسٹ آرڈر تھیوری میں ایک مربوط قدامت پسند توسیع ہوتی ہے۔ اہمیت مندرجہ بالا نظریہ کے آٹھ نتائج کی فہرست بناتی ہے جو اس کی اہمیت کی وضاحت کرتے ہیں (فوٹ نوٹ اور زیادہ تر حوالہ جات کو چھوڑ کر): G3c جیسے ترتیب وار کیلکولس کے تناظر میں، محوریات کے طور پر خصوصی مربوط مضمرات کو ساختی اصولوں (کمزوری، سنکچن اور کٹ) کی قبولیت کو متاثر کیے بغیر براہ راست تخمینہ کے اصولوں میں تبدیل کیا جا سکتا ہے۔ اسی طرح کی اصطلاحات میں، مربوط نظریات "وہ نظریات ہیں جو قدرتی کٹوتی کے اصولوں کے ذریعے ایک خاص سادہ شکل میں ظاہر ہوتے ہیں جس میں صرف جوہری فارمولے ایک اہم کردار ادا کرتے ہیں" ؛ مربوط مضمرات ترتیب بناتے ہیں جو گلیونکو کلاس دیتے ہیں۔ اس صورت میں، نتیجہ، جسے فرسٹ آرڈر بار تھیوریم کے نام سے جانا جاتا ہے، بیان کرتا ہے کہ اگر ہر آئی آئی: 0 ≤ آئی ≤ این ایک مربوط مضمر ہے اور ترتیب I1، ہے۔ ۔ ۔ میں I0 کلاسیکی طور پر ثابت ہے پھر یہ بدیہی طور پر ثابت ہے۔ مربوط/ہندسی نظریات کی بہت سی مثالیں ہیں: تمام الجبرائی نظریات، جیسے گروپ تھیوری اور رنگ تھیوری، تمام بنیادی طور پر الجبرائی نظریات، جیسے زمرہ نظریہ، فیلڈز کا نظریہ، مقامی رنگوں کا نظریہ، جالی نظریہ، پروجیکٹو جیومیٹری، علیحدہ طور پر بند مقامی رنگوں کا نظریہ (عرف "سختی سے ہینسلین مقامی رنگ") اور ٹورسن ابیلین گروپوں کا لامحدود نظریہ۔ مربوط/ہندسی نظریات کو ٹوپوئی (میک لین اور مورڈیک 1992، باب X) کے درمیان ہندسی مورفزم کے ساتھ پل بیک کے ذریعے محفوظ کیا جاتا ہے۔ سی ڈی منطق پروگرامنگ سے ہارن شقوں کو عام کرتا ہے، جہاں ڈی کو ایٹم ہونا ضروری ہے ؛ درحقیقت، وہ اختلاط منطق پروگراموں کی "شقوں" کو عام کرتے ہیں، جہاں ڈی کو ایٹموں کا اختلاط ہونے کی اجازت ہے۔ مربوط نظریات کے لیے موثر نظریہ-ثابت کرنا، (حل کے سلسلے میں) نسبتا آسانی اور وضاحت کے ساتھ، خودکار ہو سکتا ہے۔ جیسا کہ بیزیم اور دیگر نے نوٹ کیا ہے کہ اسکولیمائزیشن (فنکشن کی نئی علامتوں کا تعارف) کی عدم موجودگی کوئی حقیقی مشکل نہیں ہے، اور کلازل فارم میں غیر تبدیلی عام ریاضیاتی دلائل کی ساخت کو بہتر طریقے سے برقرار رکھنے کی اجازت دیتی ہے۔ نوٹز ببلیوگرافی (دو جلدوں، آکسفورڈ لاجک گائیڈز 43 اور 44، تیاری میں تیسرا حجم) مزید پڑھنا جیومیٹری لاجک