Аналітико-таблична семантика для формул темпоральної про­позиційної логіки

Семантика темпоральної пропозиційної логіки може бути сфор­мульована в термінах аналітико-табличної семантики. Для цього в се­мантику темпоральної пропозиційної логіки вводяться аналітичні пра­вила для темпоральних модальностей.

Аналітичні правила для темпоральних модальностей визнача­ються за аналогією із алетичними модальностями. При цьому врахо­вуються відношення між моментами часу.

- читається: «Подія А завжди буде в деякий момент часу t', якщо А буде істинним у будь-який наступний момент часу, який є досяжним із t (t Rt', де t^, — будь-який наступний момент часу, досяжний із t)>>.

- читається: «Подія А ніколи не буде в деякий момент часу t, якщо А буде хибним хоча б в один наступний момент часу t', який є досяжним із • (tRt', де t' — деякий наступний момент часу, який ще не зустрічався у попередніх рядках тієї галузки таблиці, де застосовується правило GF, і який є досяжним із t)>>.

- читається: «Подія А завжди була в деякий момент часу t, якщо А було істинним у будь-якому попередньому моменті часу, який є досяжним із t (tRt', де t' - будь-який попередній момент часу, який є досяжним із t)>>.

- читається: «Події А ніколи не було в деякий момент часу t, якщо А було хибним хоча б в одному попередньому моменті часу t', який є досяжним із t (tRt', де t' - деякий попередній момент часу, який ще не зустрічався у попередніх рядках тієї галузки таблиці, де застосо­вується правило HF, і який є досяжним із t)».

- читається: «Подія А буде в деякий момент часу t, якщо А буде істинним хоча б в один наступний момент часу, який є досяжним із t' (tRt', де t' - деякий наступний момент часу, якого ще не було в рядках тієї галузки таблиці, де застосовується правило FT₁ і який є досяжним із t)>>.

- читається: «Події А не було в деякий момент часу t, якщо А буде хибним у будь-який наступний момент часу t?, який є досяжним із t (tRt?, де t? — будь-який момент часу, який є досяжним із t)».

- читається: «Подія А була в деякий момент часу t, якщо А було істинним хоча б в один попередній момент часу t', який є досяжним із t (tRt', де t^, - деякий попередній момент часу, якого ще не було у попередніх рядках тієї галузки таблиці, де застосовується правило PT, і який є досяжним із t)».

- читається: «Події А не було в деякий момент часу t, якщо А було хибним у будь-який попередній момент часу t', який є досяжним із t (tRt', де t' - деякий попередній момент часу, який ще не зустрічався у попередніх рядках тієї галузки таблиці, де застосовується правило PF, і який є досяжним із t)>>.

За допомогою наведених аналітичних правил можна побудувати аналітичні таблиці для будь-яких формул темпоральної пропозиційної логіки з метою з’ясування їхнього семантичного статусу. Наприклад, шляхом побудови аналітичної таблиці з’ясуємо, чи є формула Hp →Pp логічним законом.

6.