From dy/dx to [ ]P: a matter of notation

Stuart Allen

UITP 1998

(User Interfaces for Theorem Provers Conference in Eindhoven)

Abstract

An analysis is given of the conventional dy/dx notation for derivatives that explains it as a notational abbreviation for expressions using the simpler binding structure standard in modern formalizations. The Nuprl display system was used to implement examples of such notation.

It turns out that the same methods can be used to explain conventional modal logic notations. We construe necessity as a first-order quantifier, in a well known way, then explain standard modal notation as a way simply to display these formulas of a non-modal logic.

We contrast the method with the interpretation of necessity as a sentential operator, and also with higher-order interpretations that have been used to interpret temporal logic in HOL. The methods are then applied to a simple first-order temporal logic. The intention is that the user can work in this notation interactively, not just produce it for printing.

This article, PostScript (9pp, 250K), PDF (180K) appeared in the

Proceedings of the Conference on User Interfaces for Theorem Provers,
Eindhoven, The Netherlands, 1998.

Section Headings: The basic idea: How dy/dx works.
Nuprl Term Structure.
Displaying Terms.
Modal Logic: first-order necessity.
Lifting: second-order necessity.
Temporal Logic: addresses.
The paper concludes with hints about applying the
notational methods to the simple part of Lamport's TLA.
There is a perhaps informative tabular summary of the various modal
semantic forms that are discussed in the text. See Semantics Summary (postscript).
Back to PRL Project Publications.