Четает, читает ... спотыкается на первой формуле:
φ ::= p | ¬φ | (φ ∨ φ) Стоять.
(φ ∨ φ) ?
Странно.
Похоже опечатка?
Судя по тексту ниже должно быть
φ ::= p | ¬φ | (φ ∨ ψ)
Зато следующая формула понятная. Час от часу не легче Шалыто А.А., Вельдер С.Э., Лукин М.А., Яминов Б.Р. Верификация автоматных программ : учебное пособие. — Санкт-Петербург : Наука, 2011. — 242 с. — ISBN 978-5-02-038160-5.