Введение
Система представления и рассуждения о времени.
В логике, временная логика – это любая система правил и символики для представления и рассуждения о высказываниях, квалифицированных во времени (например, "Я всегда голоден", "Я в конечном итоге проголодаюсь" или "Я буду голоден, пока не поем"). Иногда этот термин также используется для обозначения логики времен, модальной логической системы временной логики, предложенной Артуром Приором в конце 1950-х годов, с важным вкладом Ганса Кампа. Она была далее развита учеными в области компьютерных наук, в частности Амиром Пнуэли, и логиками. Временная логика нашла важное применение в формальной верификации, где она используется для формулирования требований к аппаратному или программному обеспечению. Например, можно утверждать, что каждый раз при поступлении запроса доступ к ресурсу в конечном итоге предоставляется, но никогда не предоставляется одновременно двум запрашивающим. Подобное утверждение удобно выразить средствами временной логики.
In logic, temporal logic is any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time (for example, "I am always hungry", "I will eventually be hungry", or "I will be hungry until I eat something"). It is sometimes also used to refer to tense logic, a modal logic based system of temporal logic introduced by Arthur Prior in the late 1950s, with important contributions by Hans Kamp. It has been further developed by computer scientists, notably Amir Pnueli, and logicians. Temporal logic has found an important application in formal verification, where it is used to state requirements of hardware or software systems. For instance, one may wish to say that whenever a request is made, access to a resource is eventually granted, but it is never granted to two requestors simultaneously. Such a statement can conveniently be expressed in a temporal logic.
Мотивация
Рассмотрим утверждение "Я голоден". Хотя его смысл остаётся постоянным во времени, истинность этого утверждения может меняться. Иногда оно истинно, а иногда ложно, но никогда одновременно и истинно, и ложно. В темпоральной логике утверждение может иметь значение истинности, которое изменяется во времени, в отличие от атемпоральной логики, которая применяется только к утверждениям, чья истинность постоянна во времени. Такое рассмотрение истинности во времени отличает темпоральную логику от вычислительной логики глаголов. Темпоральная логика всегда способна рассуждать о временной шкале. Так называемые "линейные" темпоральные логики ограничены этим типом рассуждений. Однако логики "разветвлённого времени" могут рассуждать о множестве временных шкал. Это позволяет, в частности, описывать среды, которые могут действовать непредсказуемо. Продолжая пример, в логике разветвлённого времени мы можем утверждать, что "существует возможность, что я останусь голодным навсегда", и что "существует возможность, что в конечном итоге я перестану быть голодным". Если мы не знаем, буду ли я когда-либо накормлен, оба эти утверждения могут быть истинными.
Логика позиции Лоша
Логика Лоша была опубликована в 1947 году в виде его магистерской диссертации «Podstawy Analizy Metodologicznej Kanonów Milla» (Основы методологического анализа методов Милля). Его философские и формальные концепции можно рассматривать как продолжение идей Львовско-Варшавской школы логики, поскольку его научным руководителем был Ежи Слюпецкий, ученик Яна Лукашевича. Диссертация не была переведена на английский язык до 1977 года, хотя Генрик Хиж представил в 1951 году краткий, но содержательный обзор в журнале «Journal of Symbolic Logic». В этом обзоре были изложены ключевые концепции работы Лоша, что позволило популяризировать его результаты в логическом сообществе. Главной целью данной работы было представление канонов Милля в рамках формальной логики. Для достижения этой цели автор исследовал роль временных функций в структуре концепции Милля. На основе этого он разработал свою аксиоматическую систему логики, которая могла служить основой для канонов Милля с учетом их временных аспектов.
Перевод на предикативную логику
Берджесс дает перевод Мередита из утверждений языка TL в утверждения логики первого порядка с одной свободной переменной 0 (представляющей текущий момент времени). Этот перевод определяется рекурсивно следующим образом: где – это предложение, у которого все индексы переменных увеличены на 1, а – одноместный предикат, определенный как .
where is the sentence with all variable indices incremented by 1 and is a one place predicate defined by .