This paper defines Ptolemy. The novelty of Ptolemy is the notion of event types and quantification based on event types. We give the syntax, operational semantics and type rules for the langauge, and discuss its meta-theory.