منطق زمانی
تاریخ

اگرچه منطق ارسطو تقریباً به‌طور کامل به نظریه قیاس مقوله‌ای مربوط می‌شود، در آثار او عباراتی وجود دارد که اکنون به عنوان پیش‌بینی منطق زمانی تلقی می‌شوند و ممکن است دلالت بر شکل اولیه و تا حدی توسعه‌یافته‌ای از منطق باینری موقتی مرتبه اول داشته باشند. . ارسطو به ویژه به مسئله احتمالات آینده توجه داشت، جایی که او نمی‌توانست بپذیرد که اصل دو ظرفیتی در مورد گزاره‌های مربوط به رویدادهای آینده اعمال می‌شود، یعنی در حال حاضر می‌توانیم دربارهٔ درست یا نادرست بودن گزاره‌ای در مورد رویداد آینده تصمیم بگیریم، مانند «در آنجا فردا یک نبرد دریایی خواهد بود."
چارلز سندرز پیرس در قرن نوزدهم خاطرنشان کرد: برای هزاران سال توسعه کمی وجود داشت:
| 0 | 1 | 2 |
| --- | --- | --- |
| « | Time has usually been considered by logicians to be what is called 'extralogical' matter. I have never shared this opinion. But I have thought that logic had not yet reached the state of development at which the introduction of temporal modifications of its forms would not result in great confusion; and I am much of that way of thinking yet. |  » |
به‌طور شگفت‌انگیزی برای پیرس، اولین سیستم منطق زمانی، تا آنجا که می‌دانیم، در نیمه اول قرن بیستم ساخته شد. اگرچه آرتور پریور به‌طور گسترده‌ای به عنوان بنیانگذار منطق زمانی شناخته می‌شود، اولین رسمی سازی چنین منطقی در سال ۱۹۴۷ توسط منطق دان لهستانی، جرزی لوش ارائه شد. او در کار خود Podstawy Analizy Metodologicznej Kanonów Milla (مبانی تحلیل روش شناختی روش‌های میل) رسمی سازی قوانین میل را ارائه کرد. در رویکرد Łoś تأکید بر عامل زمان قرار گرفت؛ بنابراین، برای رسیدن به هدف خود، باید منطقی را ایجاد می‌کرد که می‌توانست ابزاری برای رسمی کردن کارکردهای زمانی فراهم کند. منطق را می‌توان محصول فرعی هدف اصلی لوش دانست، اگرچه این اولین منطق موضعی بود که بعداً به عنوان چارچوبی برای اختراعات لو در منطق معرفتی استفاده شد. خود منطق دارای نحو بسیار متفاوتی با منطق زمان قبلی است که از عملگرهای مدال استفاده می‌کند. زبان منطق Łoś بیشتر از یک عملگر تحقق خاص برای منطق موقعیتی استفاده می‌کند که عبارت را با زمینه خاصی که در آن ارزش حقیقت در نظر گرفته می‌شود پیوند می‌دهد. در کار لو، این زمینه در نظر گرفته شده فقط زمانی بود، بنابراین عبارات با لحظات یا فواصل زمانی خاصی پیوند خوردند.
در سال‌های بعد، تحقیق دربارهٔ منطق زمانی توسط آرتور پریور آغاز شد. او به مفاهیم فلسفی اراده آزاد و جبر توجه داشت. به گفته همسرش، او برای اولین بار در سال ۱۹۵۳ به رسمیت بخشیدن به منطق زمانی فکر کرد. نتایج تحقیقات او برای اولین بار در کنفرانس ولینگتون در سال 1954 شد. سیستمی که پیش از این ارائه شد، از نظر نحوی مشابه منطق Łoś بود، اگرچه تا سال ۱۹۵۵ او به صراحت به کار Łoś در آخرین بخش از ضمیمه ۱ در منطق رسمی قبلی اشاره کرد.
پیش از این در سال‌های ۱۹۵۵–۱۹۵۶ در دانشگاه آکسفورد دربارهٔ این موضوع سخنرانی کرد و در سال ۱۹۵۷ کتابی به نام «زمان و روش» منتشر کرد که در آن یک منطق مدال گزاره‌ای را با دو رابط زمانی (عملگرهای مدال)، F و P که مربوط به «گاهی در آینده» و «گاهی در گذشته». در این کار اولیه، پریور زمان را خطی می‌دانست. با این حال، در سال ۱۹۵۸، او نامه ای از سائول کریپکه دریافت کرد، که به این موضوع اشاره کرد که این فرض ممکن است بیجا باشد. پریور در تحولی که مشابه آن را در علوم کامپیوتر پیش‌بینی می‌کرد، این موضوع را تحت نظر گرفت و دو نظریه دربارهٔ زمان انشعاب ایجاد کرد که آنها را «اکهامیست» و «پیرسین» نامید.[نیازمند شفاف‌سازی] بین سالهای ۱۹۵۸ و ۱۹۶۵ قبل از آن نیز با چارلز لئونارد هامبلین مکاتبه داشت و تعدادی از تحولات اولیه در این زمینه را می‌توان در این مکاتبات ردیابی کرد، به عنوان مثال مفاهیم هامبلین. پرور بالغ‌ترین اثر خود را در مورد این موضوع، کتاب گذشته، حال و آینده در سال ۱۹۶۷ منتشر کرد. او دو سال بعد درگذشت.
همراه با منطق زمان، پریور چند سیستم منطق موقعیتی را ساخت که ایده‌های اصلی خود را از Łoś به ارث برده‌اند. کار در منطق‌های زمانی موقعیتی توسط نیکلاس رسچر در دهه ۶۰ و ۷۰ ادامه یافت. در آثاری مانند یادداشت بر منطق زمانی (۱۹۶۶)، در مورد منطق قضایای زمانی (۱۹۶۸) ، منطق توپولوژیکی (۱۹۶۸)، منطق زمانی (۱۹۷۱) او در مورد ارتباط بین سیستم‌های Łoś و Prior تحقیق کرد. علاوه بر این او ثابت کرد که عملگرهای زمان قبلی را می‌توان با استفاده از عملگر تحقق در منطق‌های موقعیتی خاص تعریف کرد. رسچر در کار خود همچنین سیستم‌های کلی تری از منطق‌های موقعیتی ایجاد کرد. اگرچه اولین‌ها برای استفاده‌های صرفاً زمانی ساخته شدند، او اصطلاحی از منطق‌های توپولوژیکی را پیشنهاد کرد که شامل یک عملگر تحقق می‌شد، اما بدیهیات زمانی خاصی نداشت - مانند اصل ساعت.
عملگرهای زمانی دودویی Since و Until توسط هانس کمپ در دکترای سال ۱۹۶۸ معرفی شدند. پایان‌نامه، که همچنین حاوی یک نتیجه مهم است که منطق زمانی را به منطق مرتبه اول مرتبط می‌کند - نتیجه ای که اکنون به عنوان قضیه کمپ شناخته می‌شود.
دو رقیب اولیه در راستی‌آزمایی‌های رسمی، منطق زمانی خطی، منطق زمانی خطی توسط امیر پنولی، و منطق درخت محاسباتی، منطق زمانی منشعب شده توسط مردخای بن‌آری، زوهر ماننا و امیر پنولی بودند. یک فرمالیسم تقریباً معادل CTL در همان زمان توسط EM Clarke و EA Emerson پیشنهاد شد. این واقعیت که منطق دوم را می‌توان کارآمدتر از منطق اول تصمیم گرفت، به‌طور کلی بر منطق‌های انشعاب و خطی منعکس نمی‌شود، همان‌طور که گاهی اوقات استدلال شده‌است. در عوض، امرسون و لی نشان می‌دهند که هر منطق خطی را می‌توان به منطق انشعابی که می‌توان با همان پیچیدگی تصمیم‌گیری کرد، گسترش داد.