Adding the Everywhere Operator to Propositional Logic

Sound and complete modal propositional logic C is presented, in which 2P has the interpretation “ P is true in all states”. The interpretation is already known as the Carnapian extension of S5. A new axiomatization for C provides two insights. First, introducing an inference rule textual substitution allows seamless integration of the propositional and modal parts of the logic, giving 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.

• Type: Journal
• Year: 1998
• Where: LOGCOM
• Authors: David Gries, Fred B. Schneider
• Keywords: Inference Rule, LOGCOM 1998, Modal Propositional Logic, Propositional