Adding the everywhere operator to propositional logic
David Gries · Journal of Logic and Computation · 1998
Sound and complete modal propositional logic C is presented, in which □P has the interpretation ‘P is true in all states’. This interpretation is already known as the Camapian extension of S5. The new axiomatization for C provides two insights. First, introducing an inference rule textual substitution allows integration of the propositional and modal parts of the logic in a way that gives a more practical system for writing formal proofs. Second, the two following approaches to axiomatizing a logic are shown to be not equivalent: (i) give axiom schemes that denote an infinite number of axioms and (ii) write a finite number of axioms in terms of propositional variables and introduce a substitution inference rule.