Sciweavers

LOGCOM
1998

Adding the Everywhere Operator to Propositional Logic

14 years 3 days ago
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.
David Gries, Fred B. Schneider
Added 22 Dec 2010
Updated 22 Dec 2010
Type Journal
Year 1998
Where LOGCOM
Authors David Gries, Fred B. Schneider
Comments (0)