При всей широте использования классической логики в науке, технике и в обычной жизни очевидны ее ограничения. Классическая логика основывается на самой примитивной модели истины, она не позволяет выразить степень уверенности/неуверенности в истинности высказывания. Формулы логики могут принимать значения только "да" и "нет" на подходящей интерпретации, но не могут определить интервал возможных значений в некоторой области. Формулы обычной логики истинны или ложны независимо от времени, в статическом мире. Вследствие этого, аппарат классической логики оказался недостаточно выразительным во многих областях применения. Поэтому неудивительно, что предпринимались многочисленные попытки расширений классической логики в самых различных направлениях, и некоторые из этих попыток оказались весьма успешными.
Если утверждения естественного языка явно или неявно включают зависимость высказываний от времени или от порядка событий во времени, то формализация их в классической логике высказываний обычно неадекватна. Например, коммутативность операции конъюнкции (перестановочность ее аргументов А /\ В º В /\ А) не выполняется для следующих предложений:
"Джон умер, и его похоронили"
не эквивалентно предложению
"Джона похоронили, и он умер";
"Джейн вышла замуж и родила ребенка"
не эквивалентно предложению
"Джейн родила ребенка и вышла замуж";
"Сообщение послано в канал, и на него пришло подтверждение"
не эквивалентно предложению
"На сообщение пришло подтверждение, и оно послано в канал".
Анализ этих утверждений в рамках обычной логики высказываний невозможен. Для адекватного формального выражения подобных утверждений нужна логика, позволяющая отразить соотношения моментов времени наступления событий, в естественном языке определяемые такими словами, как "случилось после", "случается иногда", "случается всегда". Это требует формализации высказываний, истинность которых меняется во времени.
Необходимость оперировать высказываниями, истинность которых меняется со временем, возникает часто. Например, высказывание: "Путин - президент России" истинно только в определенный период времени. Высказывание "Светит солнце", ложное сегодня, может стать истинным завтра. Утверждение "Я голоден" станет ложным после того, как я поем. Многие утверждения, в которых вводятся причинно-следственные отношения, также связаны со временем:
"Если я видел ее раньше, то я узнаю ее при встрече ";
"Раз Персил - всегда Персил";
"Мы не друзья, пока ты не извинишься".
Утверждение естественного языка:
"Вчера он сказал, что придет завтра, значит, он сказал, что придет сегодня", несомненно, истинно. Но в обычной логике высказываний формальное доказательство истинности этого утверждения невозможно[1].
Большую долю утверждений, нуждающихся в формализации логической теорией с учетом времени и проверки их, составляют свойства технических систем, обладающих динамикой, то есть поведением во времени, изменяющим некоторые параметры систем. Например:
С1: Посланный запрос когда-нибудь в будущем будет обработан;
С2: Лифт никогда не пройдет мимо этажа, вызов от которого поступил, но еще не обслужен.
Элементарные (атомарные) утверждения в этих высказываниях могут быть истинны в один момент времени и ложны в другой. Мы не можем адекватно представить утверждение С1 с помощью такой формулы логики высказываний:
Послан(R) Обработан(R) (то есть если запрос R послан, то он обработан).
Действительно, в классической логике утверждения обычно понимаются как истинные либо ложные независимо от времени, а утверждение C1 явно различает разные моменты времени. Оно утверждает, что если в некоторый момент времени t запрос R послан, то в какой-то будущий момент времени t ' > t он будет обработан.
Попытаемся выразить эти свойства с помощью логики предикатов первого порядка, вводя в употребление такие выражения, как "событие р наступило в момент t". Утверждение С1 при этом будет выглядеть так:
Утверждение С2 в логике предикатов выглядит так (здесь ЛифтN(t)) - утверждение: Лифт в момент t находится на этаже n):
Такая формализация трудно читается, и, как известно, доказательства в логике предикатов проводить довольно сложно. Этот путь формализации зависимых от времени утверждений пока не дал существенных результатов для практики верификации технических систем.
Попытка построения формальной модели, неявно учитывающей время в высказываниях, была предпринята философом и логиком Гансом Райхенбахом ([1]) для изучения глагольных времен английского языка. В теории Райхенбаха время глагола в предложении характеризуется соотношением моментов наступления событий, о которых говорится и которые подразумеваются в предложении. Используя соотношения во времени двух моментов: момента S, в который сделано высказывание (Speech time), и момента Е наступления события, о котором говорится в высказывании (Event time), можно образовать только три простых времени глагола - настоящее, прошедшее и будущее с соотношениями соответственно E=S, E<S и S<E. Для того чтобы покрыть большое число различных глагольных времен, Рейхенбах ввел третий момент - момент R точки референции (Reference time), то есть момента, на который ссылается высказывание. В Past Perfect, когда мы говорим, например, "I shall have seen John" (буквально "Я буду иметь Джона увиденным"), это высказывание отсылает нас не к тому моменту, когда я увидел Джона, но к моменту, по отношению к которому (with reference to) мое видение Джона уже произошло, то есть соотношение между этими моментами времени есть S<E<R.
Формальная модель Райхенбаха позволяет прояснить различия многих времен глаголов английского языка. Например, в предложении "I saw John" соотношение между этими
моментами R=E<S; а в предложении "I have seen John" это соотношение E<R=S (рис. 1).
Однако возможность использования этого формализма для верификации дискретных систем сомнительна. Прогресс в области верификации был достигнут на пути введения специальных модальностей в обычную логику высказываний.
В приведенных выше примерах высказываний время не присутствует явно. И нам действительно часто неважно, при каких конкретных значениях времени наступали те или иные события, важно только выразить порядок событий, отношения между моментами времени, в которых эти события наступали (вспомним знаменитый тезис Л. Лэмпорта: Время есть способ упорядочения событий). Характеристики временных свойств систем используют категории вида "никогда не будет верно, что...", или "в будущем обязательно случится, что..." и тому подобные, характеризующие истинность суждения с учетом отношений между моментами наступления различных событий во времени. Можно расширить классическую логику, разрешив использовать такие категории перед утверждениями логики, например, выражение ¥Получено(т) можно понимать так: Когда-нибудь в будущем сообщение m обязательно будет получено. Такие категории называются модальностями, их можно поместить перед высказываниями, чтобы они как-то характеризовали содержание этих высказываний.
Модальность в логике (от латинского modus - способ, наклонение) вводится дополнительным оператором, предваряющим высказывание. Модальный оператор характеризует высказывание, являющееся его операндом. В общем случае модальный оператор не обязательно связан со временем. Например, пусть q - некоторое высказывание. Можно выразить неполную уверенность в истинности утверждения q, сказав: "Возможно, что q наступит". Для формализации этого введем модальный оператор М. Тогда Мq имеет смысл "возможно, что q наступит", или "может быть, наступит q".
Формальные теории устанавливают соотношения между формулами. Например, введем модальный оператор L, имеющий смысл "необходимо, что...". Тогда можно следующим образом определить отношение между модальностями М и L: Lq ºØ MØq, что согласуется с интуитивно истинным утверждением:
"q обязательно наступит, это то же самое, что неверно, что q, возможно, не наступит вовсе".
Классическая логика, расширенная какими-нибудь операторами модальности, называется модальной логикой. Такое расширение можно определить по-разному, вводя разного типа модальности и даже разную их семантику (формальное определение смысла модальностей). Возможность использования различной семантики проистекает из того, что в естественном языке в разных его применениях трактовки одних и тех же модальных слов часто различны, и даже в одной области применения они обычно смутны, расплывчаты, неоднозначны. Поэтому существует большое число различных модальных логик, каждая из которых удобна в конкретной области применения.
Модальности, которыми можно расширить классическую логику, могут быть связаны и с характеристикой момента времени, в котором утверждается истинность высказывания, зависящего от времени. Логики, расширенные такими модальностями, называются темпоральными, или временными логиками. Мы будем использовать термин темпоральные логики.
Определение 1 (темпоральные логики). Темпоральные логики - это логики, в которых истинностное значение логических формул зависит от момента времени, в котором вычисляются значения этих формул.
Темпоральные логики издавна использовались в философии для изучения таких схем рассуждений, которые включали ссылки на время. Основная идея темпоральной логики состоит в том, чтобы фиксировать только относительный порядок событий - фактически, текущее, будущее и прошедшее время. Конечно, в некоторых приложениях, например в области верификации систем реального времени, явные значения времени и численные ограничения на время должны учитываться, и там следует вводить более сложные формализмы.
В одной из предшественниц современных темпоральных логик - Tense Logic, разработанной английским логиком Артуром Прайором в середине прошлого века [2], были впервые введены две модальности: F (от Future): "когда-нибудь в будущем будет истинно..." и P (от Past): "когда-то в прошлом было истинно...".
На рис. 2 показано, при каких значениях времени истинны утверждения Fq и Pq, если заданы отрезки времени, в которых истинно утверждение q. Обозначим t|=Ф утверждение:
"В момент времени t истинно утверждение Ф". Тогда (см. рис. 2):
- утверждение q истинно в момент времени t (t|=q), если утверждение q истинно в момент t (что является тождественной истиной, тавтологией);
- утверждение Fq истинно в момент времени t (t|=Fq), если для какого-то момента времени t' в будущем (при некотором t'>t) q станет истинным (заметьте, что будущее здесь включает настоящее);
- утверждение Рq истинно в момент времени t (t|=Pq), если для какого-то момента времени t' в прошлом (при некотором t'> t < t) утверждение q было истинным.
В Tense Logic введены и два дуальных темпоральных оператора: G (от слова Globally) и H (от слова History) с очевидными соотношениями: Gq ºØ F Ø q, Hq ºØ P Ø q. Справедливость этих соотношений очевидна. Например, первого: "Утверждать, что в будущем утверждение q будет всегда истинно, это то же самое, что утверждать, что неверно, что когда-нибудь в будущем утверждение q станет ложным". Эти операторы можно определить и независимо от F и P (см. рис. 2):
Рис. 2. Темпоральные операторы Tense Logic |
- утверждение Gq истинно в момент времени t (t|=Gq), если для любого момента времени t' в будущем (при всех t'>t) утверждение q истинно (заметьте, что будущее здесь также включает настоящее);
- утверждение Hq истинно в момент времени t (t|=Hq), если для любого момента времени t' в прошлом утверждение q истинно.
Уже с помощью двух темпоральных операторов F и G можно выразить сложные свойства, зависящие от времени. Например:
Утверждение q будет истинным:
всегда в будущем: Gq
хотя бы раз в будущем: Fq
никогда в будущем: Ø Fq
бесконечно много раз в будущем: GFq
с какого-то момента постоянно: FGq.
Рассмотрим, как с помощью этих операторов формально записать некоторые утверждения.
События е1 и е2 никогда не произойдут одновременно (взаимное исключение): G[Ø(е1 /\ e2) ]
Посланное сообщение m когда-нибудь в будущем будет получено:
G[ Посланоm F Полученот ]
Джейн вышла замуж и родила ребенка:
Р(Джейн_выходит_замуж /\ FДжейн_рожаеm_ребенка)
Джейн родила ребенка и вышла замуж:
Р(Джейн_рожает_ребенка /\ FДжейн_выходum_замуж)
Пока ключ зажигания не вставлен, машина не поедет:
G(ØP Зажигание Старт).
В темпоральную логику можно ввести еще два оператора: NextTime (X) и Until (U). Оператор Next time: утверждение Xq истинно в момент времени t, если q истинно в следующий момент t + 1:
Джон убил, и ему стало страшно:
Р(Джон_убивает /\ XG Джону_страшно)
Если я видел ее раньше, я ее узнаю при встрече:
РУвидел G(Всmреmuл ^ ХУзнал)
Джон умер и его похоронили:
Р(Джон_умирает /\ XGДжона_хоронят)
Оператор Until (до тех пор, пока не наступит нечто) требует двух аргументов - утверждений. Формально он записывается довольно сложно:
Утверждение pUq истинно в момент времени t, если q истинно в некоторый будущий момент времени t'> t, а во всем промежутке [t, t') от момента t до t' истинно p. Пример развертки во времени, показывающей, когда будет истинно утверждение pUq при различных истинностных значениях p и q, показан на рис. 3.
С оператором Until многие сложные утверждения легко представимы в формальной записи, например:
Мы не друзья, пока ты не извинишься:
(ØМы_друзья) U Ты_извиняешься
Лифт никогда не пройдет мимо этажа, вызов от которого поступил, но еще не обслужен:
G [ Вызов(n) (ØЛифт(n))U Обслуживается(n) ].
Через оператор U легко выражается оператор F:
Fq = true U q,
а следовательно, и оператор G:
G = ØFØq = Ø (true U Ø q).
В этой логике для операторов X и U существуют их аналоги в прошлом: X^(-1) (в предыдущий момент времени, 'вчера') и S (since, 'с тех пор, как').
Tense Logic позволяет формализовать философские мысли о времени. Например, обозначим атомарное утверждение "нечто есть" символом q. Тогда следующее глубокомысленное абсолютно истинное заключение (тавтологию):
"Будет, что нечто было, если и только если оно или есть сейчас, или будет, или уже было"
можно формализовать так:
FPq º q \/ Fq \/ Pq.
Философскую мысль о времени:
"Любое 'вчера' было когда-то 'завтра', любое 'завтра' когда-нибудь станет 'вчера'" формально можно записать так:
(PX^(-1)q PXq) /\ (FXq FX^(-1)q).
Временная логика помогает точно и однозначно выразить временные соотношения между событиями, о которых повествуют (часто неоднозначные) фразы естественного языка. Обозначим:
Д(х): х - мой друг, П(х): х - президент.
Используя эти обозначения, можно формально записать несколько совершенно различных интерпретаций предложения "Мой друг NN будет президентом":
1 Д(NN) & FXП(NN):
сейчас NN — мой друг, а в будущем он станет президентом;
2 FX(Д(NN) & П(NN)):
в будущем NN станет моим другом, и в это время он уже будет президентом;
3 F(Д(NN) & FXП(NN))
в будущем NN станет моим другом, а затем он станет президентом.