|Home||Online Resources||Table of Contents|
Journal of Logic and Computation, Volume 8, Issue 1: February 1998.
Adding the everywhere operator to propositional logic
D Gries and FB Schneider
Computer Science, Cornell University, Ithaca, NY 14853, USA. E-mail: email@example.com
Sound and complete modal prepositional logic C is presented, in which [squ]P has the interpretation 'P is true in all states'. This interpretation is already known as the Carnapian extension of S5. The new axiomatization for C provides two insights. First, introducing an inference rule textual substitution allows integration of the prepositional 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 prepositional variables and introduce a substitution inference rule.
Keywords: Propositional logic, calculational logic, everywhere operator.