2015-02-24
2247
Временные логики – это модальные логики. Они строятся добавлением к логике высказываний новых знаков, отражающих свойства времени. Термин «временная логика» широко употребляется как покрывающий все подходы к представлению временной информации в рамках логической системы.
Рассуждение Георга фон Вригта: «Возьмем, например, процесс выпадения дождя. Этот процесс продолжается некоторое время, а затем прекращается. Но предположим, что это происходит не внезапно, а постепенно. Пусть 
иллюстрирует, что на определенном отрезке времени вначале определенно идет дождь (А), потом определенно не идет дождь (
), а между этими временными точками находится переходная область, когда может капать небольшое количество капель – слишком мало для того, чтобы заставить нас сказать, что идет дождь, но слишком много для того, чтобы мы могли воздержаться от утверждения, что дождь определенно закончился. В этой области высказывание А ни истинно, ни ложно»[6].
Логический язык временной логики содержит, в дополнение к обычным истинностным операторам четыре модальных оператора со следующими предполагаемыми смыслами:
|
|
|
P «Когда-то было верно что…»
F «Когда-то будет верно что…»
H «Всегда было верно что…»
G «Всегда будет верно что»
P и F известны как слабые временные операторы, в то время, как H и G известны как сильные временные операторы. Эти две пары обычно рассматриваются как взаимоопределяемые с помощью эквивалентностей:
На основе этих предполагаемых смыслов, Приор использовал операторы для построения формул, выражающих различные философские положения относительно времени, которые при желании можно взять за аксиомы формальной системы. Несколько примеров:
«Что будет всегда, будет в некоторый момент»
«Если из p всегда будет следовать q, то, если p всегда будет верно, то также всегда будет верно q»
«Если р будет верно, то будет также верно – до этого – что р будет верно»
«Если никогда не будет верно р, то всегда будет верно, что р никогда не будет верно»
Особо важна система минимальной временной логики Kt, которая порождается четырьмя аксиомами:
«Про то, что истинно, всегда было верно, что оно будет истинно»
«Про то, что истинно, всегда будет верно, что оно было истинно»
«То, что всегда следовало из того, что всегда было верно, само всегда было верно»
«То, что всегда будет следовать из того, что всегда будет верно, само всегда будет верно»
вместе с двумя правилами временного вывода:
RH: Из доказательства р выводится доказательство Hр
RG: Из доказательства p выводится доказательство Gp,
и, естественно, всеми правилами обычной пропозициональной логики. Теоремы Kt выражают, по сути, те свойства временных операторов, что не зависят от каких-либо конкретных предположений относительно временного порядка.
|
|
|
Временная логика получается добавлением временных операторов к существующей логике. Очевидной важностью обладает временная логика предикатов, в которой временные операторы добавляются к классическому исчислению предикатов первого порядка. Это позволяет нам выразить важные различия, касающиеся логики времени и существования. К примеру, утверждение «Философ будет королем» можно интерпретировать несколькими различными способами, например:
«Некто, являющийся философом, будет в будущем королем»
«Существует некто, кто в будущем будет одновременно философом и королем»
«Будет существовать некто, являющийся философом, и кто будет в будущем королем»
«Будет существовать некто, являющийся одновременно философом и королем»
Вскоре после своего появления, базовый синтаксис «PFGH» временной логики был расширен различными способами. Несколькими важными примерами являются следующие:
· Бинарные временные операторы S и U («sinсe», «until», «с тех пор», «до тех пор»). Предполагаемыми смыслами являются:
Spq «q было верно с того момента, когда p было верно»
Upq «q будет верно до того момента, когда p будет верно»
· Метрическая временная логика. Выражение Fnp для обозначения «Спустя интервал n будет верно p». Отдельного понятия Pnp не нужно, так как запись F(-n)p выражает «Интервал n назад было верно p». Случай n=0 дает настоящее время.
· Оператор О («следующий раз»). Этот оператор предполагает, что время состоит из дискретного ряда атомарных моментов. Формула Ор предполагает обозначить, что р истинно в ближайший следующий момент (или шаг) времени.
