College of Engineering >
Computer Science >
Computer Science Technical Reports >
Please use this identifier to cite or link to this item:
|Title: ||Adding the Everywhere Operator to Propositional Logic|
|Authors: ||Gries, David|
Schneider, Fred B.
|Keywords: ||computer science|
|Issue Date: ||May-1996|
|Publisher: ||Cornell University|
|Abstract: ||Sound and complete modal propositional logic C is presented, in which "P" 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.|
|Appears in Collections:||Computer Science Technical Reports|
Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.