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: gries@cs.comell.edu

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.

Pages 119-129


This page is run by Oxford University Press, Great Clarendon Street, Oxford OX2 6DP, UK
as part of the OUP Journals World Wide Web service.
Comments and feedback: www-admin@oup.co.uk
URL: http://www.oup.co.uk/logcom/hdb/Volume_08/Issue_01/080119.sgm.abs.html
Last modification: 1 June 1998.
Copyright© Oxford University Press, 1998.