© 1998 by Oxford University Press
| ||||||||||||||||||||||||||||||||||||||||||||||||||
Original Articles |
Adding the Everywhere Operator to Propositional Logic
Computer Science, Cornell University Ithaca, NY 14853, USA E-mail: gries{at}cs.cornell.edu
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.
Keywords: Propositional logic; calculational logic; everywhere operator